search

pysathq / pysat

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

Is there any way to solve DNF formulas? #56

Closed Biowav closed 3 years ago

Biowav commented 4 years ago

Greetings,

I am trying to use PySAT to solve some non-CNF formulas, concretly, most of my formulas are in DNF. I make thousand of calls to the solver and I'm very interested in performance, so I can't transform formulas to CNF all the time, Is there any way to work directly with non-CNF formulas?

Thank you in advance!

alexeyignatiev commented 4 years ago

Hi there,

What exactly do you want to do with DNF formulas? Checking satisfiability should be trivial. :) I presume something else is needed.

Anyway, regarding performance, can't you encode the formula once and then do incremental SAT calls with the use of varying list of assumptions? This is the first suggestion that comes to my mind - as SAT solvers support CNF only, you have to encode your formulas into CNF one way or another.

Biowav commented 4 years ago

Hello alex,

Your are right! For DNF the satisfiability is trivial, but the problem is that we don't know in what form the formula comes. We are developing a model checker and given a formula (DNF, CNF or none of them) we pass it to a SAT-Solver that give us a satisfiable model reducing the size of the problem. However, maybe with that model we can't solve the problem and in these cases the SAT-Solver is usually asked to return a different model.

We know that some SAT-Solvers for example Z3 returns an answer regardless of input form, but as we have seen, it's much slower than this library! (with what you said, maybe Z3 itself encodes it to CNF, and that's why it's much slower) So the question goes in that direction, but I think we will have to take a different approach.

alexeyignatiev commented 4 years ago

Hi @Biowav,

Well, as far as I can get, you have something like the standard abstraction refinement loop, right? Normally, you should be able to make small changes to the formula on-the-fly, when "refining it" and then make incremental calls to a SAT oracle so that it could give you a different model. Isn't this possible in your case? If you have a small example, I could try to think about some basic ideas to do it more-or-less efficiently.