From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id aBYkFzDY92Jp4QAAbAwnHQ (envelope-from ) for ; Sat, 13 Aug 2022 18:58:24 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id 4FwVFzDY92J1TwAA9RJhRA (envelope-from ) for ; Sat, 13 Aug 2022 18:58:24 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id D5CFB3C9DB for ; Sat, 13 Aug 2022 18:58:23 +0200 (CEST) Received: from localhost ([::1]:54456 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oMuSs-0006Ww-P9 for larch@yhetil.org; Sat, 13 Aug 2022 12:58:22 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:36102) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oMuRd-0005mY-CS for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:05 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:45229) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oMuRb-0001O3-Ur for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:05 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oMuRb-0006M9-Qm for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:03 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Maximilian Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 13 Aug 2022 16:57:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 57181 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 57181@debbugs.gnu.org X-Debbugs-Original-To: "guix-patches@gnu.org" Received: via spool by submit@debbugs.gnu.org id=B.166040981024389 (code B ref -1); Sat, 13 Aug 2022 16:57:03 +0000 Received: (at submit) by debbugs.gnu.org; 13 Aug 2022 16:56:50 +0000 Received: from localhost ([127.0.0.1]:34975 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMuRL-0006LE-1y for submit@debbugs.gnu.org; Sat, 13 Aug 2022 12:56:50 -0400 Received: from lists.gnu.org ([209.51.188.17]:44812) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMtAP-0004Gq-0h for submit@debbugs.gnu.org; Sat, 13 Aug 2022 11:35:16 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:52886) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oMtAD-0001AW-Co for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:04 -0400 Received: from mout-p-202.mailbox.org ([80.241.56.172]:56256) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_CHACHA20_POLY1305:256) (Exim 4.90_1) (envelope-from ) id 1oMtA8-0006Nf-MM for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:01 -0400 Received: from smtp2.mailbox.org (smtp2.mailbox.org [10.196.197.2]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-384) server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by mout-p-202.mailbox.org (Postfix) with ESMTPS id 4M4l3F5VTBz9sTh for ; Sat, 13 Aug 2022 17:34:49 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1660404889; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type; bh=ugBfwExP9pqFp7Fzh18MxqZ3yTZmZOQ14UZnKuDRyXU=; b=JZVb1JsP8hkcK0KrIFuooT02Cx5orqlCPg5JHFaaLFCEMhAnmCokkN24ZvgPN1WjzRp+qA gydxKgHjFetpUdXZc+N3x+VgnPl6h/Tz6QchuIRWLL/U6CvWhO+IWbmO8WM6hSoxy3NGuX g7R+2dKePPlU7xsq0yapyUn6EwoossFtns8rWE2xHHxT4f+5Jq5SI11agUNfxPVeAmc9W2 /3DuTXnTa2COzymvU7pJbKKULHXzLPI/z9fcgPyeXIuzJM6HGmakzu2mcLW003eLUkBBfM 14SJQwQB6RPb/GYX3HJFSJP2t0Yezljf3X9bE7hGHsEohBPyooqFsMw8Qau3zg== Date: Sat, 13 Aug 2022 17:34:49 +0200 (CEST) From: Maximilian Heisinger Message-ID: <923508243.78855.1660404889221@ox93.mailbox.org> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="----=_Part_78854_1462168451.1660404889220" X-Priority: 3 Importance: Normal Received-SPF: pass client-ip=80.241.56.172; envelope-from=mail@maxheisinger.at; helo=mout-p-202.mailbox.org X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_LOW=-0.7, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Mailman-Approved-At: Sat, 13 Aug 2022 12:56:45 -0400 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1660409904; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:list-id:list-help:list-unsubscribe:list-subscribe: list-post:dkim-signature; bh=ugBfwExP9pqFp7Fzh18MxqZ3yTZmZOQ14UZnKuDRyXU=; b=jOYn1kdpesGa4fVlpg+jgpWUHuNYJl7BhfclFaloKYqeNSjvXv+HzNbnUwY9gSC43mqKTU jnf5eaWbz6VYu8N2VB5vG6cIvZBWG04IbWke2LQyVZghEHtMmKLAgfvtifKjK2tlh3stJ+ R9RF7h8of8Pb8cqkyTJUGQF2dz5qfq8eRP3GDrpaO3mNaRDoD8Pr4fKeY3gNBHzlzo+Cgp NeO50b5Hf4WGe1cHxJu7/5/hg75s1ivx+rRtKYSbJyDoxS8BFAaMEpCKTSfNKoUr8IC0h9 IXRmmVGjgxOC/ofuW50Oky05NHICIiEozfMunrpGMQ4PkJLdYnCJCvs1UkGXFA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1660409904; a=rsa-sha256; cv=none; b=eaXafqKXRjOMFYuiMx6pOgBFfxb94qN39DXwrdp80DVSdNiJDbkePrFg8q7D0OHpeCI8a4 WZs3ntnB6Gb201hXjAMca6X4z48frUxSrzuWVuzzVESuXKGgzQZZTdinH4G3QZlogv3G8a CjNjqxmbsiSXuiorPQP0WBTiFf3Fa5UNELv0mbDhel39bAx9jN5m8xGkpoxyetXDDTJLEB /T/kUmPbbjqZJJ1GyAnNiQmqeNUkec0wHi9kaD5FTlmmDjcaL4DR9ZfWcKhtoWdpWB9Ne6 bNreZlZR+CD4LFMB2ijxfey+qt/8dKImWxuOrOQ30pOMGj1mdolbdKF/qO98Jg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=maxheisinger.at header.s=MBO0001 header.b=JZVb1JsP; dmarc=fail reason="SPF not aligned (relaxed)" header.from=maxheisinger.at (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: 3.34 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=maxheisinger.at header.s=MBO0001 header.b=JZVb1JsP; dmarc=fail reason="SPF not aligned (relaxed)" header.from=maxheisinger.at (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: D5CFB3C9DB X-Spam-Score: 3.34 X-Migadu-Scanner: scn0.migadu.com X-TUID: cDshQudnZMqx ------=_Part_78854_1462168451.1660404889220 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit >From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001 From: Maximilian Heisinger 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 ------=_Part_78854_1462168451.1660404889220 Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc -----BEGIN PGP SIGNATURE----- Version: BCPG v1.65 iQEcBAABCgAGBQJi98SZAAoJEIhyV2pwqbcQW1UH/ijwpo9WkbAbaJ+oW5YBz9K9 ogx65DSyABAtwd5z0wyKvERSBuSB/z0W4jeOjwrCIXCDIV1aDlHR6WHVvfIUgLk0 7GtiwnZW6nCnAYQBP8Zm7WdeEAucrhops5JDTzk/evI5rwJceC396yVH4lBv+3Q9 VRPDlQI/kQ3gPsXjIUbpUFSY8zQM5Dp1EPp2IaVteuy0r42XHET/hQLOuKK8BXwt rnfFlu3RcdfbKHH/2xTaIEwHeLp3FdmAZeMNuHdDEls2LY14lYSQEQeP4uVKk66m Wo29zupk86eDWsvMqjP8Ic1Jj0GA33XlajEH5ail4ymtMRITiO/74OkjiZPBrgo= =SmL6 -----END PGP SIGNATURE----- ------=_Part_78854_1462168451.1660404889220--