From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@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