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.
The first line of input 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 and m where 1 ≤ n ≤ 20 indicates the number of variables and 1 ≤ m ≤ 100 indicates the number of clauses. Then, m lines follow corresponding to each clause. Each clause is a disjunction of literals in the form Xi or ~Xi for some 1 ≤ i ≤ n, where ~Xi indicates the negation of the literal Xi. The “or” operator is denoted by a ‘v’ character and is separated from literals with a single space.
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise display unsatisfiable.
2 3 3 X1 v X2 ~X1 ~X2 v X3 3 5 X1 v X2 v X3 X1 v ~X2 X2 v ~X3 X3 v ~X1 ~X1 v ~X2 v ~X3
This code basically maintains
mySets which is a list of sets, which all represent possible combinations of literals that could make the entire statement true. Every time we parse a new clause, we check if it's negation exists already in a set, if it does, the set is not included.
This works, but it runs a bit slow.
import sys cases = int(sys.stdin.readline()) def GetReverse(literal): if literal == '~': return literal[1:] else: return '~' + literal for i in range(cases): vars, clauses = map(int, sys.stdin.readline().split()) mySets =  firstClause = sys.stdin.readline().strip().split(" v ") for c in firstClause: this = set() this.add(c) mySets.append(this) for i in range(clauses-1): tempSets =  currentClause = sys.stdin.readline().strip().split(" v ") for s in mySets: for literal in currentClause: if not s.__contains__(GetReverse(literal)): newset = s.copy() newset.add(literal) tempSets.append(newset) mySets = tempSets if mySets: print("satisfiable") else: print("unsatisfiable")
I think the problem is here, due to the indented for-loops. 3-SAT is supposed to be exponential, but I would like to speed it up a bit (perhaps by removing a loop?)
for i in range(clauses-1): tempSets =  currentClause = sys.stdin.readline().strip().split(" v ") for s in mySets: for literal in currentClause: if not s.__contains__(GetReverse(literal)): newset = s.copy() newset.add(literal) tempSets.append(newset) mySets = tempSets