INPUT FILE: dnf.in
OUTPUT FILE: dnf.out
Given a formula in DNF - disjunctive normal form (a bunch of clauses ORed together, where each clause consists of variables ANDed together), determine what values of the variables (0 for false, 1 for true) satisfy the formula (i.e. make it true).
For example,
(a & b) | (x & !y)
is satisfied for (a, b, x, y) = (1, 1, 0, 0) or (0, 0, 1, 0), etc.
You only need to print out one such assignment ("&" means AND, "|" means OR and "!" means NOT); print out the variables in alphabetical order and separate outputs by a blank line. Print "UNSATISFIABLE" if no such assignment exists.
There will be <= 26 variables (a to z) and each clause will be <= 250 characters long. There will be < 1000 clauses in formula. There will never be more than "!" in a row, as I would be too lazy to code it.
The first line of each input contains the number of clauses; "-1" denotes the end of the input.
Sample Input File
1 (!a) 2 (a & b) | (x & !y) -1
Output for Sample Input
a=0 a=1 b=1 x=0 y=0