[bug#57181] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat
Commit Message
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
Comments
Hi,
I've pushed kissat with some heavy edits. In particular, I
- fixed the commit message,
- hard-coded the compression binaries (and made them regular inputs),
- fixed the actual test failure,
- used G-Expressions rather than quasiquoting.
See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee.
Am Montag, dem 15.08.2022 um 12:50 +0200 schrieb Maximilian Heisinger:
> 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.
I know about the existence of Minisat, but the problem here is rather
that cryptominisat seems to pull in lots of stuff that we'd rather have
packaged separately instead of vendored (e.g. googletest). Could you
try unvendoring those things and place the remaining parts in the right
location without a recursive checkout?
> The library interfaces mimic this and also
> +allow IPASIR-esque incremental use, including assumptions.
"Incremental solving" sounds easier to understand.
> + (inputs (list zlib boost))
> + (native-inputs (list python python-lit))
If you have a Python interface, you probably also need python in
inputs, no?
Cheers
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(+)
@@ -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