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

Previous Next

Full log

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

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

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

Previous Next

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