[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