On: SATisfying Solutions to Difficult Problems

[thesz]

  > 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 → thesz]

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.