>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
signature.asc
Description: PGP signature
--- End Message ---