SKEDSOFT

DIMACS file encoding: At this point, having generated the gate net-list and their clauses, we now need to generate a file format representing the conjunction of these clauses. The standard format employed is the so called DIMACS format, where the literals in each clause are listed on separate lines, terminated by 0.
Given such a DIMACS file, one can feed the file to a Boolean satisfiability solver.

The result of feeding the above file to zchaff is shown below:

The SAT solver Zchaff picked the assignment given by the line

which stands for the Boolean assignment

Suppose we force the assignment of x=0 by adding the clause ¬x: the assignment then becomes the one shown below, where p,q,r,s are set to 1: