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

[Maximilian Heisinger <mail@maxheisinger.at>]

[-- Attachment #1.1: Type: text/plain, Size: 744 bytes --]

Hi,

sorry, doing the correct CC now.

> Recursive checkout doesn't really sound "mini".

Oh, there's some history behind the mini...  CryptoMiniSat adds some stuff commonly needed in cryptography to MiniSat, which is a common base for many other SAT solvers.  Kissat is "clean" mainly because it is a new solver that completely breaks with the old MiniSat codebase (and it cleans up some stuff, that was done in CaDiCaL, which I also intend to add later, as some features are still missing from Kissat).  And MiniSat itself was a nice and minimal implementation containing (back then) the state-of-the-art optimizations.

> could we try to make this a shared library?

Done.

Also updated the text and the commit messages :)

Best regards,
Max

[-- Attachment #1.2: 0002-PATCH-gnu-Add-modern-SAT-solver-kissat.patch --]
[-- Type: text/x-patch, Size: 3126 bytes --]

From 2a1a5176241c2062b1d4b1f379ca6fb945fb701f Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@maxheisinger.at>
Date: Sun, 14 Aug 2022 21:09:59 +0200
Subject: [PATCH 2/2] PATCH] gnu: Add modern SAT solver kissat

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

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index f69c6ce6de..580751e516 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7345,6 +7345,61 @@ (define-public cryptominisat5
     (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)
+    (native-inputs (list xz gzip lzip bzip2))
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key configure-flags #:allow-other-keys)
+             ;; The configure script of kissat is custom and does not support
+             ;; standard GNU options like CONFIG_SHELL.  We therefore overwrite
+             ;; the default.
+             (apply invoke "./configure" "-shared" configure-flags)))
+         (add-before 'check 'patch-test
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             ;; "main" test fails in build container.  The list below includes
+             ;; all tests but the failing one.
+             (substitute* "build/makefile"
+               (("./tissat")
+                 "./tissat error utilities endianness ceil format references \\
+\treluctant random queue allocate array stack arena heap vector rank sort bump \\
+\toptions config init add file parse collect kitten solve coverage usage \\
+\tterminate"))))
+         (replace 'install
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (install-file
+              "build/kissat"
+              (string-append (assoc-ref outputs "out") "/bin"))
+             (install-file
+              "build/libkissat.so"
+              (string-append (assoc-ref outputs "out") "/lib"))
+             (install-file
+              "src/kissat.h"
+              (string-append (assoc-ref outputs "out") "/include/kissat")))))))
+    (home-page "https://github.com/arminbiere/kissat")
+    (synopsis "Bare-metal SAT solver")
+    (description
+     "Kissat is a 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:expat)))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.37.1


[-- Attachment #1.3: 0001-PATCH-gnu-Add-modern-SAT-solver-cryptominisat5.patch --]
[-- Type: text/x-patch, Size: 2056 bytes --]

From c212c453002f0cd7e547c98f51672f28387def05 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@maxheisinger.at>
Date: Sun, 14 Aug 2022 15:40:02 +0200
Subject: [PATCH 1/2] [PATCH] gnu: Add modern SAT solver cryptominisat5

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

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index c79058ab42..f69c6ce6de 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7311,6 +7311,40 @@ (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)
+             ;; Recursive checkout is required to enable testing.
+             (recursive? #t)))
+      (file-name (git-file-name name version))
+      (sha256
+       (base32
+        "1dz4b4mjmbm2j758l3y520x918mh5b1ia73xx6byw0h97kwyx8zw"))))
+    (build-system cmake-build-system)
+    (arguments
+     (list #:build-type "Release"
+           #:test-target "test"
+           #:configure-flags
+           #~(list "-DENABLE_TESTING=ON")))
+    (inputs (list zlib boost))
+    (native-inputs (list python python-lit))
+    (synopsis "Incremental SAT solver")
+    (description
+     "CryptoMiniSat is an incremental SAT solver with both command line and
+library (C++, C, Python) interfaces.  The command-line interface takes a
+@acronym{CNF, Conjunctive Normal Form} as an input in the DIMACS format with
+the extension of XOR clauses.  The library interfaces mimic this and also
+allow IPASIR-esque incremental use, including assumptions.")
+    (home-page "https://github.com/msoos/cryptominisat")
+    (license license:expat)))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.37.1


[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 475 bytes --]