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

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

[Maximilian Heisinger]

[-- Attachment #1: Type: text/plain, Size: 3219 bytes --]

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

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

[bug#57181] [PATCH v2 1/4] gnu: Add aiger.

[Liliana Marie Prikler]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3324 bytes --]

* gnu/packages/maths.scm (aiger): New variable.
---
 gnu/packages/maths.scm | 54 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ffd2a89d2f..1e9d7b8be8 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,6 +55,7 @@
 ;;; Copyright © 2022 Philip McGrath <philip@philipmcgrath.com>
 ;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
 ;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
+;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler@gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -7375,6 +7376,59 @@ (define-public kissat
 optimized algorithms and implementation.")
     (license license:expat)))
 
+(define-public aiger
+  (package
+    (name "aiger")
+    (version "1.9.9")
+    (source (origin
+             (method url-fetch)
+             (uri (string-append "http://fmv.jku.at/aiger/aiger-"
+                                 version ".tar.gz"))
+             (sha256
+               (base32
+                "1ish0dw0nf9gyghxsdhpy1jjiy5wp54c993swp85xp7m6vdx6l0y"))))
+    (outputs (list "out" "static"))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:tests? #f                  ; no check target
+           #:phases
+           #~(modify-phases %standard-phases
+               (add-after 'unpack 'patch-source
+                 (lambda* (#:key inputs #:allow-other-keys)
+                   (substitute* "aiger.c"
+                     (("\"(gzip|gunzip)" all cmd)
+                      (string-append
+                       "\""
+                       (search-input-file inputs (string-append "bin/" cmd)))))))
+               (add-after 'unpack 'patch-build-files
+                 (lambda* (#:key outputs #:allow-other-keys)
+                   (substitute* "makefile.in"
+                     (("test -d .*") "true")
+                     (("/usr/local") (assoc-ref outputs "out")))))
+               (replace 'configure
+                 (lambda* (#:key configure-flags #:allow-other-keys)
+                   (apply invoke "./configure.sh" configure-flags)))
+               (add-after 'install 'install-static
+                 (lambda* (#:key outputs #:allow-other-keys)
+                   (apply invoke #$(ar-for-target) "rcs" "libaiger.a"
+                          (find-files "." "\\.o$"))
+                   (let* ((static (assoc-ref outputs "static"))
+                          (lib (string-append static "/lib"))
+                          (incl (string-append static "/include/aiger")))
+                     (mkdir-p lib)
+                     (mkdir-p incl)
+                     (install-file "libaiger.a" lib)
+                     (for-each (lambda (f) (install-file f incl))
+                               (find-files "." "\\.h$"))))))))
+    (inputs (list gzip))
+    (home-page "http://fmv.jku.at/aiger")
+    (synopsis "Utilities for And-Inverter Graphs")
+    (description "AIGER is a format, library and set of utilities for
+@acronym{AIG, And-Inverter Graphs}s.  The focus is on conversion utilities and a
+generic reader and writer API.")
+    (license (list license:expat
+                   license:bsd-3))))    ; blif2aig
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.38.0

[bug#57181] [PATCH v2 2/4] gnu: Add lingeling.

[Liliana Marie Prikler]

* gnu/packages/maths.scm (lingeling): New variable.
---
 gnu/packages/maths.scm | 82 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1e9d7b8be8..5c8a0fe2ef 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7429,6 +7429,88 @@ (define-public aiger
     (license (list license:expat
                    license:bsd-3))))    ; blif2aig
 
+(define-public lingeling
+  (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
+        (revision "1"))
+    (package
+     (name "lingeling")
+     (version (git-version "sc2022" revision commit))
+     (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/arminbiere/lingeling")
+                    (commit commit)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c"))))
+     (build-system gnu-build-system)
+     (arguments
+      (list #:test-target "test"
+            #:modules `((ice-9 match)
+                        ,@%gnu-build-system-modules)
+            #:configure-flags #~(list "--aiger=.")
+            #:phases
+            #~(modify-phases %standard-phases
+                (add-after 'unpack 'unpack-aiger
+                  (lambda* (#:key inputs #:allow-other-keys)
+                    (invoke #$(ar-for-target) "x"
+                            (search-input-file inputs "lib/libaiger.a")
+                            "aiger.o")
+                    (copy-file
+                     (search-input-file inputs "include/aiger/aiger.h")
+                     "aiger.h")))
+                (add-after 'unpack 'hard-code-commit
+                  (lambda _
+                    (substitute* "mkconfig.sh"
+                      (("`\\./getgitid`") #$commit))))
+                (add-after 'unpack 'patch-source
+                  (lambda* (#:key inputs #:allow-other-keys)
+                    (substitute* (list "treengeling.c" "lgldimacs.c")
+                      (("\"(gunzip|xz|bzcat|7z)" all cmd)
+                       (string-append
+                        "\""
+                        (search-input-file inputs (string-append "bin/" cmd)))))))
+                (replace 'configure
+                  (lambda* (#:key configure-flags #:allow-other-keys)
+                    (apply invoke "./configure.sh" configure-flags)))
+                (replace 'install
+                  (lambda* (#:key outputs #:allow-other-keys)
+                    (let ((bin (string-append (assoc-ref outputs "out")
+                                              "/bin")))
+                      (mkdir-p bin)
+                      (for-each
+                       (lambda (file)
+                         (install-file file bin))
+                       '("blimc" "ilingeling" "lglddtrace" "lglmbt"
+                         "lgluntrace" "lingeling" "plingeling"
+                         "treengeling")))))
+                (add-after 'install 'wrap-path
+                  (lambda* (#:key outputs #:allow-other-keys)
+                    (with-directory-excursion (string-append
+                                               (assoc-ref outputs "out")
+                                               "/bin")
+                      (for-each
+                       (lambda (file)
+                         (wrap-program
+                          file
+                          '("PATH" suffix
+                            #$(map (lambda (input)
+                                     (file-append (this-package-input input) "/bin"))
+                                   '("gzip" "bzip2" "xz" "p7zip")))))
+                       ;; These programs use sprintf on buffers with magic
+                       ;; values to construct commands (yes, eww), so we
+                       ;; can't easily substitute* them.
+                       '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
+     (inputs (list `(,aiger "static") gzip bzip2 xz p7zip))
+     (home-page "http://fmv.jku.at/lingeling")
+     (synopsis "SAT solver")
+     (description "This package provides a range of SAT solvers, including
+the sequential @command{lingeling} and its parallel variants
+@command{plingeling} and @command{treengeling}.  A bounded model checker is
+also included.")
+     (license license:expat))))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.38.0

[bug#57181] [PATCH v2 3/4] gnu: Add louvain-community.

[Liliana Marie Prikler]

* gnu/packages/maths.scm (louvain-community): New variable.
---
 gnu/packages/maths.scm | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5c8a0fe2ef..58faa6674b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7511,6 +7511,37 @@ (define-public lingeling
 also included.")
      (license license:expat))))
 
+(define-public louvain-community
+  (let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
+        (revision "1"))
+    (package
+      (name "louvain-community")
+      (version (git-version "1.0.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                       (url "https://github.com/meelgroup/louvain-community")
+                       (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "1ss00hkdvr9bdkd355hxf8zd7xycb3nm8qpy7s75gjjf6yng0bfj"))))
+      (build-system cmake-build-system)
+      (arguments
+       (list #:tests? #f                ; tests appear to require missing files
+             #:phases
+             #~(modify-phases %standard-phases
+                 (add-after 'unpack 'encode-git-hash
+                   (lambda _
+                     (substitute* "CMakeLists.txt"
+                       (("GIT-hash-notfound") #$commit)))))))
+      (native-inputs (list python))
+      (home-page "https://github.com/meelgroup/louvain-communities")
+      (synopsis "Multi-criteria community detection")
+      (description "This package provides a C++ implementation of the Louvain
+community detection algorithm.")
+      (license license:lgpl3+))))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.38.0

[bug#57181] [PATCH v2 4/4] gnu: Add cryptominisat.

[Liliana Marie Prikler]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3381 bytes --]

* gnu/packages/maths.scm (cryptominisat): New variable.

Co-authored-by: Maximilian Heisinger <mail@maxheisinger.at>
---
 gnu/packages/maths.scm | 51 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 58faa6674b..9db28239fd 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -56,6 +56,7 @@
 ;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
 ;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
 ;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler@gmail.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail@maxheisinger.at>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -159,6 +160,7 @@ (define-module (gnu packages maths)
   #:use-module (gnu packages serialization)
   #:use-module (gnu packages shells)
   #:use-module (gnu packages sphinx)
+  #:use-module (gnu packages sqlite)
   #:use-module (gnu packages swig)
   #:use-module (gnu packages tcl)
   #:use-module (gnu packages texinfo)
@@ -7542,6 +7544,55 @@ (define-public louvain-community
 community detection algorithm.")
       (license license:lgpl3+))))
 
+(define-public cryptominisat
+  (package
+    (name "cryptominisat")
+    (version "5.11.4")
+    (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
+        "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc"))))
+    (build-system cmake-build-system)
+    (arguments
+     (list
+      #:build-type "Release"
+      #:test-target "test"
+      #:configure-flags #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON")
+      #:phases
+      #~(modify-phases %standard-phases
+          (add-after 'unpack 'patch-source
+            (lambda* (#:key inputs #:allow-other-keys)
+              (substitute* "CMakeLists.txt"
+                (("add_subdirectory\\(utils/lingeling-ala\\)") ""))
+              ;; Transitively included in vendored gtest.h. Fixed in
+              ;; upstream:
+              ;; https://github.com/msoos/cryptominisat/pull/686
+              (substitute* "tests/assump_test.cpp"
+                (("#include <vector>")
+                 "#include <vector>\n#include <algorithm>"))
+              (substitute* "tests/CMakeLists.txt"
+                (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)")
+                 "find_package(GTest REQUIRED)")
+                (("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)")
+                 "")))))))
+    (inputs (list boost louvain-community python python-numpy sqlite zlib))
+    (native-inputs (list googletest lingeling python python-wrapper 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 incremental solving, including assumptions.")
+    (home-page "https://github.com/msoos/cryptominisat")
+    (license license:expat)))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.38.0

bug#57181: [PATCH v2 4/4] gnu: Add cryptominisat.

[Liliana Marie Prikler]

Am Samstag, dem 15.10.2022 um 16:47 +0200 schrieb Liliana Marie
Prikler:
> * gnu/packages/maths.scm (cryptominisat): New variable.
> 
> Co-authored-by: Maximilian Heisinger <mail@maxheisinger.at>
Aaaand it's pushed.

[bug#57181] [PATCH v2 4/4] gnu: Add cryptominisat.

[Maximilian Heisinger]

[-- Attachment #1: Type: text/plain, Size: 725 bytes --]

> Liliana Marie Prikler <liliana.prikler@gmail.com> hat am 26.11.2022 14:15 CET geschrieben:
>
> Aaaand it's pushed.

Thank you so much! Sorry for not working on the patch in the meantime, I started doing this while at a conference and was completely wrapped up in other issues and some deadlines after coming back...

This is a beautiful patch series and I am looking forward to being able to coming up with such constructs myself. Integrating libraries like this is really interesting and opens up quite a few possibilities for research, especially with preserving old releases and making them comparable.

Thanks again, and I'm looking forward to future submissions! They will be bottom-up next time :)

Best regards,
Max

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

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

[Liliana Marie Prikler]

Hi,

Am Samstag, dem 13.08.2022 um 17:23 +0200 schrieb Maximilian Heisinger:
> * gnu/packages/maths.scm (cryptominisat5): Add package.
> * gnu/packages/maths.scm (kissat): Add package.
Split into two patches, one for cryptominisat and one for kissat.
> ---
>  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))
Always state why tests are disabled.
> +    (inputs (list zlib boost))
> +    (synopsis "Advanced incremental SAT solver")
"Incremental SAT solver" is probably enough.
> +    (description
> +     "Provides CryptoMiniSat, an advanced incremental SAT solver. 
> The system
> +has 3 interfaces: command-line, C++ library and python.
I'd shorten this to "CryptoMiniSat is an incremental SAT solver with
three 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
Use @abbrev for CNF (also capitalize).
> +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.")
Doesn't that technically make it a fourth interface?
> +    (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
Specify why.
> +       #:phases
> +       (modify-phases %standard-phases
> +         (replace 'configure
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (invoke "./configure")))
You probably want to (apply invoke "./configure" configure-flags).
> +         (replace 'install
> +           (lambda* (#:key inputs outputs #:allow-other-keys)
> +             (install-file
> +              "build/kissat"
> +              (string-append (assoc-ref outputs "out") "/bin")))))))
Is this the only thing to install?
> +    (home-page "https://github.com/arminbiere/kissat")
> +    (synopsis "Bare-metal SAT solver after the KISS principle
> principle
> +written in C")
"Bare-metal SAT solver" probably suffices.
> +    (description
> +     "Kissat is a \"keep it simple and clean bare metal SAT solver\"
> written
"bare metal SAT solver" again probably suffices.  If you want to be
generous with advertising terms, clean may be added, but I don't think
it adds useful information.
> +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+)))
> +
Cheers

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

[Liliana Marie Prikler]

Hi,

Don't forget to CC the mailing list.

Am Sonntag, dem 14.08.2022 um 21:27 +0200 schrieb Maximilian Heisinger:

> gnu: maths: Add modern SAT solver cryptominisat5
Should simply be "gnu: Add cryptominisat5.

> +       (uri (git-reference
> +             (url "https://github.com/msoos/cryptominisat")
> +             (commit version)
> +             (recursive? #t)))
Recursive checkout doesn't really sound "mini".
> 

> +    (description
> +     "Incremental SAT solver with four interfaces: command-line, C++
> library,
> +C interface, and Python.
I forgot this, but the description should consist of full sentences. 
Also, while I (jokingly) referred to the C interface as a separate
interface, you should probably phrase this a little differently.

> gnu: maths: Add modern SAT solver kissat
As above.

> +             ;; One test fails in the guix build container: "main".
> The cause
> +             ;; is not clear yet and this test is not enabled in the
> tissat
> +             ;; test step.  Kissat (called by tissat) just does not
> finish.
> +             ;; Could be an issue with kissat.
This could probably be shortened to something like "XXX: main test
fails in build container".

> +             ;; Kissat has no `make install` step, so files are
> installed
> +             ;; manually.  This installs the (static) library, the
> header and
> +             ;; the executable.
Don't comment the obvious, but more importantly, could we try to make
this a shared library?

> Kissat is a bare-metal and clean SAT-solver written in C.
I wouldn't use "and" as a joiner here.  Both "clean, bare-metal SAT
solver" and "bare-metal SAT solver" sound a little cleaner 🙂️

Cheers

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

[Maximilian Heisinger]

[-- 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 --]

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

[Liliana Marie Prikler]

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

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

[mail]

[-- Attachment #1: Type: text/plain, Size: 2156 bytes --]

Hi,

> - 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.

Thank you very much!  This really is clearer, better, and gives me more
pointers to research about Guix.

> 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?

Yes, that would be better... Then we have two choices now I think:

 1. Try to unvendor everything and add minisat as transformed package
    with different sources + lingeling as a new package.  This would
    also still require to download the external test files as additional
    source repositories.
 2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
    offers that is meant to build a simpler binary, but also deactivates
    more complex tests.  We still build a complex binary (i.e. Boost
    program options for options parsing) by not setting it, but instead
    substitute the query for the option in the  ~test/CMakeLists.txt~
    file.  Additionally, we substitute some other issues away.

The second option loses some scripts and the more comprehensive tests.
I would argue though, that these would be better suited for developing
the solver and less for such a package management situation.  What is
your opinion about this trade-off?

> "Incremental solving" sounds easier to understand.

Changed it.

> If you have a Python interface, you probably also need python in
> inputs, no?

True - it is better to directly expose it.  I also took another look at
the solver's capabilities and output in more detail and added
python-numpy (required dependency for the py API) and sqlite (optional
dependency used for collecting statistics).

Thank you again for your patience and effort!  You find my updated patch
attached.

Best regards (now even written from an Emacs mail client),
Max


[-- Attachment #2: 0001-gnu-Add-cryptominisat5.patch --]
[-- Type: text/x-patch, Size: 3575 bytes --]

From 5541a0aeb7660eacd5dbec8ef88db42af7b3b7b5 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@maxheisinger.at>
Date: Tue, 16 Aug 2022 20:59:06 +0200
Subject: [PATCH] gnu: Add cryptominisat5

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

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 72d5e9a83a..a01f386831 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,6 +55,7 @@
 ;;; Copyright © 2022 Philip McGrath <philip@philipmcgrath.com>
 ;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
 ;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail@maxheisinger.at>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -159,6 +160,7 @@ (define-module (gnu packages maths)
   #:use-module (gnu packages shells)
   #:use-module (gnu packages sphinx)
   #:use-module (gnu packages swig)
+  #:use-module (gnu packages sqlite)
   #:use-module (gnu packages tcl)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages tex)
@@ -7317,6 +7319,54 @@ (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
+     (list #:build-type "Release"
+           #:test-target "test"
+           #:configure-flags
+           #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON")
+           #:phases
+           #~(modify-phases %standard-phases
+               (add-after 'unpack 'patch-source
+                 (lambda* (#:key inputs #:allow-other-keys)
+                   (substitute* "CMakeLists.txt"
+                     (("add_subdirectory\\(utils/lingeling-ala\\)") ""))
+                   ;; Transitively included in vendored gtest.h. Fixed in
+                   ;; upstream:
+                   ;; https://github.com/msoos/cryptominisat/pull/686
+                   (substitute* "tests/assump_test.cpp"
+                     (("#include <vector>")
+                      "#include <vector>\n#include <algorithm>"))
+                   (substitute* "tests/CMakeLists.txt"
+                     (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)")
+                      "find_package(GTest REQUIRED)")
+                     (("if\\(NOT ONLY_SIMPLE\\)") "if(FALSE)")))))))
+    (inputs (list zlib boost sqlite python python-numpy))
+    (native-inputs (list python-lit googletest))
+    (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 incremental solving, including assumptions.")
+    (home-page "https://github.com/msoos/cryptominisat")
+    (license license:expat)))
+
 (define-public kissat
   (package
     (name "kissat")
-- 
2.37.2

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

[Liliana Marie Prikler]

Hi,

Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb
mail@maxheisinger.at:
> [...] [W]e have two choices now I think:
> 
>  1. Try to unvendor everything and add minisat as transformed package
>     with different sources + lingeling as a new package.  This would
>     also still require to download the external test files as
>     additional source repositories.
>  2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
>     offers that is meant to build a simpler binary, but also
>     deactivates more complex tests.  We still build a complex binary
>     (i.e. Boost program options for options parsing) by not setting
>     it, but instead substitute the query for the option in the
>     ~test/CMakeLists.txt~ file.  Additionally, we substitute some
>     other issues away.
> 
> The second option loses some scripts and the more comprehensive
> tests.  I would argue though, that these would be better suited for
> developing the solver and less for such a package management
> situation.  What is your opinion about this trade-off?
Only running simple tests is preferable to running no tests at all.  If
you think that unvendoring everything is an unreasonable amount of
work, that's a viable solution.  However, we do strive to offer
complete packages, so feel free to do 1. :)

If you need some pointers as for the test files, ppsspp includes both
another package's source (not so great, needs better unvendoring) and
test files, and there's probably some other packages you could consult
as well.

> > "Incremental solving" sounds easier to understand.
> 
> Changed it.
LGTM.

> > If you have a Python interface, you probably also need python in
> > inputs, no?
> 
> True - it is better to directly expose it.  I also took another look
> at the solver's capabilities and output in more detail and added
> python-numpy (required dependency for the py API) and sqlite
> (optional dependency used for collecting statistics).
Note that python is now missing from native-inputs, but python-lit is
in there.  I suppose you need python both as input (for linking) and
native-input (to run whatever python-lit is supposed to do).


Cheers