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

Previous Next

Full log

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

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: mail <at> maxheisinger.at
Cc: 57181 <at> debbugs.gnu.org
Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and
 kissat
Date: Wed, 17 Aug 2022 22:16:03 +0200

Hi,

Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb
mail <at> maxheisinger.at:
> [...] [W]e have two choices now I think:
> 
>  1. Try to unvendor everything and add minisat as transformed package
>     with different sources + lingeling as a new package.  This would
>     also still require to download the external test files as
>     additional source repositories.
>  2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
>     offers that is meant to build a simpler binary, but also
>     deactivates more complex tests.  We still build a complex binary
>     (i.e. Boost program options for options parsing) by not setting
>     it, but instead substitute the query for the option in the
>     ~test/CMakeLists.txt~ file.  Additionally, we substitute some
>     other issues away.
> 
> The second option loses some scripts and the more comprehensive
> tests.  I would argue though, that these would be better suited for
> developing the solver and less for such a package management
> situation.  What is your opinion about this trade-off?
Only running simple tests is preferable to running no tests at all.  If
you think that unvendoring everything is an unreasonable amount of
work, that's a viable solution.  However, we do strive to offer
complete packages, so feel free to do 1. :)

If you need some pointers as for the test files, ppsspp includes both
another package's source (not so great, needs better unvendoring) and
test files, and there's probably some other packages you could consult
as well.

> > "Incremental solving" sounds easier to understand.
> 
> Changed it.
LGTM.

> > If you have a Python interface, you probably also need python in
> > inputs, no?
> 
> True - it is better to directly expose it.  I also took another look
> at the solver's capabilities and output in more detail and added
> python-numpy (required dependency for the py API) and sqlite
> (optional dependency used for collecting statistics).
Note that python is now missing from native-inputs, but python-lit is
in there.  I suppose you need python both as input (for linking) and
native-input (to run whatever python-lit is supposed to do).


Cheers

Previous Next

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