GNU bug report logs - #57181
[PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Maximilian Heisinger <mail <at> maxheisinger.at>
Subject: bug#57181: closed (Re: [PATCH v2 4/4] gnu: Add cryptominisat.)
Date: Sat, 26 Nov 2022 13:16:02 +0000

[Message part 1 (text/plain, inline)]

Your bug report

#57181: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 57181 <at> debbugs.gnu.org.

-- 
57181: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=57181
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: 57181-done <at> debbugs.gnu.org
Cc: mail <at> maxheisinger.at
Subject: Re: [PATCH v2 4/4] gnu: Add cryptominisat.
Date: Sat, 26 Nov 2022 14:15:35 +0100

Am Samstag, dem 15.10.2022 um 16:47 +0200 schrieb Liliana Marie
Prikler:
> * gnu/packages/maths.scm (cryptominisat): New variable.
> 
> Co-authored-by: Maximilian Heisinger <mail <at> maxheisinger.at>
Aaaand it's pushed.

[Message part 3 (message/rfc822, inline)]

From: Maximilian Heisinger <mail <at> maxheisinger.at>
To: "guix-patches <at> gnu.org" <guix-patches <at> gnu.org>
Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat
Date: Sat, 13 Aug 2022 17:34:49 +0200 (CEST)

[Message part 4 (text/plain, inline)]

From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail <at> maxheisinger.at>
Date: Sat, 13 Aug 2022 17:23:59 +0200
Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat

* gnu/packages/maths.scm (cryptominisat5): Add package.
* gnu/packages/maths.scm (kissat): Add package.
---
 gnu/packages/maths.scm | 64 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index c79058ab42..4a58b9eb3f 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7311,6 +7311,70 @@ (define-public minisat
        "http://minisat.se/MiniSat.html")
       (license license:expat))))

+(define-public cryptominisat5
+  (package
+    (name "cryptominisat5")
+    (version "5.8.0")
+    (source
+     (origin
+      (method git-fetch)
+      (uri (git-reference
+        (url "https://github.com/msoos/cryptominisat")
+        (commit version)))
+      (file-name (git-file-name name version))
+      (sha256
+       (base32
+        "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"))))
+    (build-system cmake-build-system)
+    (arguments `(#:tests? #false))
+    (inputs (list zlib boost))
+    (synopsis "Advanced incremental SAT solver")
+    (description
+     "Provides CryptoMiniSat, an advanced incremental SAT solver.  The system
+has 3 interfaces: command-line, C++ library and python.  The command-line
+interface takes a cnf as an input in the DIMACS format with the extension of
+XOR clauses.  The C++ and python interface mimics this and also allows for
+incremental use: assumptions and multiple solve calls.  A C compatible wrapper
+is also provided.")
+    (home-page "https://github.com/msoos/cryptominisat")
+    (license license:expat)))
+
+(define-public kissat
+  (package
+    (name "kissat")
+    (version "3.0.0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/arminbiere/kissat")
+             (commit (string-append "rel-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:tests? #f
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs #:allow-other-keys)
+             (invoke "./configure")))
+         (replace 'install
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (install-file
+              "build/kissat"
+              (string-append (assoc-ref outputs "out") "/bin")))))))
+    (home-page "https://github.com/arminbiere/kissat")
+    (synopsis "Bare-metal SAT solver after the KISS principle principle
+written in C")
+    (description
+     "Kissat is a \"keep it simple and clean bare metal SAT solver\" written
+in C.  It is a port of CaDiCaL back to C with improved data structures, better
+scheduling of inprocessing and optimized algorithms and implementation.")
+    (license license:gpl3+)))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
--
2.37.1

[signature.asc (application/pgp-signature, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.