diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index adc7beb655..2b21ce3db2 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8925,6 +8925,97 @@ (define-public kissat
  optimized algorithms and implementation.")
      (license license:expat)))
  
+(define-public cadical
+  (package
+    (name "cadical")
+    (version "1.9.4")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/arminbiere/cadical")
+             (commit (string-append "rel-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1sd3r1czgm6h36fa5if2npnjpfnxjnzlnc2srkbwi2ywvsysyavi"))))
+    (build-system gnu-build-system)
+    (inputs (list xz gzip lzip bzip2 p7zip))
+    (arguments
+     (list
+      #:test-target "test"
+      #:phases #~(modify-phases %standard-phases
+                   (add-after 'unpack 'patch-source
+                     (lambda* (#:key inputs outputs source #:allow-other-keys)
+                       (substitute* "src/file.cpp"
+                         (("(bzip2|gzip|lzma|xz) -c" all cmd)
+                          (string-append (search-input-file inputs
+                                                            (string-append
+                                                             "bin/" cmd))
+                                         " -c"))
+                         (("7z ([ax])" all mode)
+                          (string-append (search-input-file inputs "bin/7z")
+                                         " " mode))
+                         ;; Since we hard-coded the paths, we no longer need to find
+                         ;; them.
+                         (("char \\*found = find\\_program \\(prg\\)")
+                          "const char* found = \"<configured-at-build-time>\"")
+                         (("delete\\[\\] found;")
+                          ""))
+                       (substitute* "scripts/make-build-header.sh"
+                         ;; The identifier in Guix is the source, as the input may be
+                         ;; replaced while building.
+                         (("`../scripts/get-git-id.sh`")
+                          source)
+                         ;; Remove non-determinism by removing the date from the
+                         ;; binary.
+                         (("\\$DATE")
+                          "<no non-deterministic timestamp in the binary>"))
+                       ;; Convert the static library to a shared one.
+                       (substitute* "makefile.in"
+                         (("libcadical\\.a")
+                          "libcadical.so")
+                         (("\\$\\(COMPILE\\) -o")
+                          (string-append "$(COMPILE) -Wl,-rpath="
+                                         (assoc-ref outputs "out") "/lib -o"))
+                         (("ar rc")
+                          "$(COMPILE) -shared -o"))
+                       (substitute* "test/api/run.sh"
+                         (("libcadical\\.a")
+                          "libcadical.so"))
+                       (substitute* "configure"
+                         (("-static")
+                          "-shared")
+                         ;; Tests are not written with a shared libcadical.so in
+                         ;; mind, so the LD_LIBRARY_PATH has to be set to the
+                         ;; libcadical.so in the build directory while running
+                         ;; tests. The rpath points to the installed directory and is
+                         ;; only available after installation.
+                         (("\\\\\\$\\(MAKE\\)")
+                          (string-append "export LD_LIBRARY_PATH="
+                                         (getcwd) "/build/ ; \\\\\\$(MAKE)"))
+                         (("CXXFLAGS=\"\\$CXXFLAGS\\$options\"")
+                          "CXXFLAGS=\"$CXXFLAGS$options -fPIC\""))))
+                   (replace 'configure
+                     (lambda* (#:key configure-flags #:allow-other-keys)
+                       ;; The configure script does not support standard GNU options.
+                       (apply invoke "./configure" configure-flags)))
+                   (replace 'install
+                     (lambda* (#:key inputs outputs #:allow-other-keys)
+                       (let ((out (assoc-ref outputs "out")))
+                         (install-file "build/cadical"
+                                       (string-append out "/bin"))
+                         (install-file "build/libcadical.so"
+                                       (string-append out "/lib"))
+                         (install-file "src/cadical.hpp"
+                                       (string-append out "/include"))))))))
+    (home-page "https://github.com/arminbiere/cadical")
+    (synopsis "CaDiCaL Simplified Satisfiability (SAT) Solver")
+    (description
+     "CaDiCaL is a hackable CDCL SAT solver written in C++. It offers an incremental
+API and a library for solving SAT problems given in CNF in the standard DIMACS
+format.")
+    (license license:expat)))
+
  (define-public aiger
    (package
      (name "aiger")
