- Time limit: 5.00 s
- Memory limit: 512 MB
SAT solvers find satisfying assignments to Boolean formulas. The formulas are given in the conjunctive normal form:
- the formula is a conjunction of clauses:
- each clause is a disjunction of literals:
- each literal is either a Boolean variable or is negation .
Here is the "AND" operation, is the "OR" operation, and is the "NOT" operation. We will always assume that the variables are called .
For example, here is a Boolean formula in the conjunctive normal form; we have clauses and variables: This formula is satisfiable; we can find the following variable assignment that makes the formula true: Such formulas are commonly represented in the standard DIMACS format: the first line contains the magic words "p" ("problem") and "cnf" ("conjunctive normal form"), and then it is followed by the number of variables and the number of clauses . This is followed by lines, each describing one clause. The line contains just one number per literal: a positive literal is written as , and a negated literal is written as . The clause is terminated with a .
For example, the above formula would be written as follows in the DIMACS format:
p cnf 3 3 1 2 3 0 -1 -2 -3 0 -1 2 3 0
Now we could take a commonly used SAT solver, for example "picosat", and ask it to solve this. We will get e.g. the following output:
s SATISFIABLE v -1 2 3 0
Here the first line of output that starts with an "s" indicates that this formula was indeed satisfiable, and the second line of output that starts with a "v" gives the variable assingment. For each , we write if is true and if is false. Again, the list is terminated with a .
Your task here is to write a SAT solver that solves formulas in certain special cases.
Input
The input is a Boolean formula in the conjunctive normal form, given in the DIMACS format.
Each clause will contain exactly 2 literals. (It is possible that the same variable occurs twice in one clause.)
Output
Output a satisfying assignment in a format similar to the one used in the "picosat" example above.
If a solution exists, there should be two lines of output: first one that says "s SATISFIABLE", and then one that starts with "v", then contains values that indicate the satisfying assignment, and finally a "0".
If there is no solution, you should print out just one line that says "s UNSATISFIABLE".
Limits
- Number of variables:
- Number of clause:
Example 1
Input:
p cnf 4 5 2 -1 0 -1 -2 0 1 3 0 -2 -3 0 1 4 0
Output:
s SATISFIABLE v -1 -2 3 4 0
Example 2
Input:
p cnf 3 4 1 2 0 1 -2 0 -1 3 0 -1 -3 0
Output:
s UNSATISFIABLE