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

Previous Next

Full log

Message #17 received at 57181 <at> debbugs.gnu.org (full text, mbox):

From: Maximilian Heisinger <mail <at> maxheisinger.at>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 57181 <at> debbugs.gnu.org
Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and
 kissat
Date: Mon, 15 Aug 2022 12:50:30 +0200 (CEST)

[Message part 1 (text/plain, inline)]

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

[0002-PATCH-gnu-Add-modern-SAT-solver-kissat.patch (text/x-patch, attachment)]

[0001-PATCH-gnu-Add-modern-SAT-solver-cryptominisat5.patch (text/x-patch, attachment)]

[signature.asc (application/pgp-signature, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.