Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

A SAT solver will stop at the first solution. But it is easy to make it generate all the solutions. A solution takes the form of a list of true and false terms. To force the generation of a new solution, forbid the old one. Take the solution, expressed as a clause, negate it and append the new clause to the end of the CNF. Rerun the CNF and a new solution will appear. Repeat as necessary. This whole processes is automated in the library.

Mail: (not shown)

Please type this: