Yet Satisfiability Again!
Alice recently started to work for a hardware design company and as a part of her job, she needs to identify defects in fabricated integrated circuits. An approach for identifying these defects boils down to solving a satisfiability instance. She needs your help to write a program to do this task.
Input
The first line contains a single integer, not more than 5, indicating the number of test cases to follow. The first line of each test case contains two integers n (1 ≤ n ≤ 20) and m (1 ≤ m ≤ 100), where n indicates the number of variables and m indicates the number of clauses. Then m lines follow corresponding to each clause. Each clause is a disjunction of literals in the form X[i]
or ~X[i]
for some i (1 ≤ i ≤ n), where ~X[i]
indicates the negation of the literal X[i]
. The "or" operator is denoted by a v character and is separated from literals with a single space.
Output
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise display unsatisfiable.