search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
385 stars 69 forks source link

Include kissat #61

Open haz opened 4 years ago

haz commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 3 years ago

@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 commented 3 years ago

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 commented 3 years ago

@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.)

lesshaste commented 1 week ago

+1 for inclusion of kissat, especially as the new version won three first places in the 2024 sat competition.