Problem C
Counting Clauses
It’s time for the annual 3-SAT competition, where the contestants compete to answer as many instances of 3-SAT as possible within the time limit. 3-SAT is a classic NP-complete problem, where you are given a boolean formula in conjunctive normal form, in which we have a set of clauses each consisting of exactly three literals. Each literal refer either positively or negatively to a variable, which can be assigned a value of either True or False. The question is whether there exists an assignment to the variables such that every clause evaluates to True. No clause will contain duplicates of a literal (however it is possible that a clause contain both $\neg x_ i$ and $x_ i$). An example of a 3-SAT instance is shown below (from sample input 1):
\[ (\neg x_1 \vee x_2 \vee x_3) \wedge (\neg x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee \neg x_2 \vee \neg x_3) \wedge (x_1 \vee x_2 \vee \neg x_3) \]
Input
The input is a single instance of the 3-SAT problem. The first line is two space-separated integers: $m$ ($1 \leq m \leq 20$), the number of clauses and $n$ ($3 \leq n \leq 20$), the number of variables. Then $m$ clauses follow, one clause per line. Each clause consists of 3 distinct space-separated integers in the range $[-n, n] \setminus \{ 0\} $. For each clause, the three values correspond to the three literals in the clause. If the literal is negative, that means that the clause is satisfied if the corresponding variable is set to False, and if it is positive the clause is satisfied if the variable is set to True.
Output
Print “satisfactory” on a single line if Øyvind finds the 3-SAT instance to be satisfactory, and “unsatisfactory” otherwise.
| Sample Input 1 | Sample Output 1 |
|---|---|
5 3 -1 2 3 -1 -2 3 1 -2 3 1 -2 -3 1 2 -3 |
unsatisfactory |
| Sample Input 2 | Sample Output 2 |
|---|---|
8 3 1 2 3 1 2 -3 1 -2 3 1 -2 -3 -1 2 3 -1 2 -3 -1 -2 3 -1 -2 -3 |
satisfactory |
