Programming Challenge

Write a program that takes a boolean expression in conjunctive normal form and either outputs a set of values for the variables that makes the expression true or “no variable values can make this true”.

You can assume the following input format:

For example:

0 1
1 -2 3
0 -1
4 5 -3

Means:

(x0 ∨ x1) ∧ (x1 ∨ ¬x2 ∨ x3) ∧ (x0 ∨ ¬x1) ∧ (x4 ∨ x5 ∨ ¬x3)

Visit ToughSAT to get test cases.

Try:

AND = ∧ OR = ∨ NOT = ¬