Include kissat

[haz]

The latest contest results are out, and we have a new top-solver: http://fmv.jku.at/kissat/

It's an improved version of CaDiCaL, and so hopefully not a big undertaking to include.

In a related note, we'll be shifting the nnf package to optionally use the pysat package for solving. Among other things, this will allow users to write arbitrary NNF formula, compile it using Tseitin, and then solve using pysat. The combination of the two libraries should hopefully address what you had in mind with the fourth bullet in the main TODO list.

[alexeyignatiev]

Hi @haz,

Yes, sure, I know what kissat is. I agree it would be great to have it included in pysat. In fact, I have already thought about this and I asked @arminbiere about incrementality features in kissat here immediately after SAT2020 where the competition results were announced.

The bottom line is I will add it for sure when there is at least some rudimentary support of incrementality added in kissat.

Bullet 4 is partially covered by the ability to use AIG graphs now. But having NNFs would be indeed great, absolutely! Thank you!

[haz]

Ah, hadn't thought about incremental aspect. Is there any option to have a baseline compatibility for the pysat functionality using the solvers as a black-box (i.e., external calls only)? Then it's just a matter of performance when it comes to having a full proper integration.

[alexeyignatiev]

Sorry for this belated response. To be honest, PySAT is all about incrementality and efficient use of original SAT solvers. So I don't see a point right now in including a non-incremental solver here. Let's wait a bit. I am sure Armin will not take too long to add the necessary stuff in kissat.

[hellman]

@alexeyignatiev this is sad, PySAT seems to be the only generic python frontend for various SAT solvers. Even without incrementality, just solving SAT and being able to switch the solver by changing an argument is very useful.

[haz]

If you really just want the hot swap of kissat, then you can use the library we have for nnf: https://python-nnf.readthedocs.io/en/stable/nnf.html#module-nnf.kissat

It hooks into pysat as well, but we found it useful to have an out-of-the-box access to kissat (wrapping the command-line rather than the solver internals).

It's not entirely ready for prime-time, but bauhaus is another library on its way that will provide some nice abstraction if you're modelling in Python.

[alexeyignatiev]

@hellman, well, I am not completely against adding kissat to PySAT as a non-incremental solver. It's just that I don't feel enough motivation to spend my time doing this if there is only a single possible use-case scenario, which not many I believe will find useful. If you want to add the solver to the toolkit then great, PRs are more than welcome. (But the solver should be used through the API - not an external tool.)