Hacker News Reader

Comment by isolay | Hacker News Reader

This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. My homegrown solver finds all valuations that make a proposition true and then can eliminate redundancies, such that `X or not X and Y` gets simplified to `X or Y`, just to mention one example (proof: truth tables are identical). Are there any other SAT solvers out there that do something like that? My own one suffers from combinatorial explosion in the simplification stage when expressions get "complex" enough. But then, the simplification is NP-complete, AFAICT.

View on HN

  > This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true.

Most, if not all, current SAT solvers are incremental. They allow you to add clauses on the fly.

So, when you find the solution, you can add a (long!) clause that blocks that solution from appearing again and then run solver again.

Most, if not all, SAT solvers have a command line option for that enumeration done behind the scenes, for picosat it is "picosat --all".

For problems with a very large number of solutions this quickly becomes inefficient. The blocking clauses will bog down the solver hard and waste tons of memory.

A more clever approach is to emulate depth-first search using a stack of assumption literals. The solver still retains learned conflict clauses so it's more efficient than naive DPLL.

It's not very difficult to turn a CDCL solver into an ALL-SAT solver, and there are many publications available doing exactly that.

I would also add that #SAT solvers, aiming at counting the number of solutions, are often implicitly solving the ALL-SAT in a more efficient manner than what you would have with modified CDCL solvers because they use other caching and decomposability techniques. Check knowledge compiler d4 for example https://github.com/crillab/d4v2 that can build some kind of circuits representing every solution in a factorized yet tractable way.

Reply on news.ycombinator.com