3 ms·
> 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 a
by thesz 1y ago
> 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".
- sirwhinesalot 1y agoFor 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.