SAT Solver

To use the SAT solver, enter the formula below in DIMACS CNF format. This format starts with a line of the form:

    p cnf N M

where N is replaced by the number of variables (e.g., 6) and M is replaced by the number of conjuncts (e.g., 15) that are AND-ed together to make the full formula.

This first line is followed by M more lines, one describing each of the conjucts. An individual conjunct is described with a line like the following:

    1 2 -3 0

This describes a disjunction of the first, second, and third variables, with the "-" before 3 indicating that the third variable is negated. If the variables are "a", "b", and "c", then the line above represents the disjunction “a ∨ b ∨ ¬c”. The final 0 indicates the end of the conjunct.

(See here for a more detailed discussion of the format.)

Input

p cnf 6 15 1 2 3 0 -1 -2 0 -1 -3 0 -2 -3 0 4 5 6 0 -4 -5 0 -4 -6 0 -5 -6 0 1 4 0 -1 -4 0 2 5 0 -2 -5 0 -1 2 -6 0 -2 6 0 1 6 0

Output

(Acknowledgements: This page uses the minisat JS library from here.)