INPUT FILE: cnf.in
OUTPUT FILE: cnf.out
Given a formula in CNF - conjunctive normal form (a bunch of clauses ANDed together, where each clause consists of variables ORed together), determine what values of the variables (0 for false, 1 for true) satisfy the formula (i.e. make it true).
For a description of input/output see DNF.
Sample Input File
2 (a | a) & (!a | !a) -1
Output for Sample Input
UNSATISFIABLE