diff mbox series

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

Message ID 132482353.134362.1660560630571@ox93.mailbox.org
State New
Headers show
Series [bug#57181] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat | expand

Checks

Context Check Description
cbaines/comparison success View comparision
cbaines/git-branch success View Git branch
cbaines/applying patch success View Laminar job
cbaines/issue success View issue

Commit Message

Maximilian Heisinger Aug. 15, 2022, 10:50 a.m. UTC 
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
diff mbox series

Patch

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