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 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.

Output
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise display unsatisfiable.

Sample Input

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

Sample Output satisfiable unsatisfiable

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 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.

Output
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise display unsatisfiable.

Sample Input

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 

Sample Output

satisfiable
unsatisfiable

i'm currently trying to solve this problem: https://open.kattis.com/problems/satisfiability

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 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 seperated 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.

And I have this code:

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.

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

It's obvious that the problem lies somewhere here, indented forloops just arent great, but 3sat should be at least exponential anyway. Could i do the same thing as I do here, using one less loop? thanks a lot

I've written a 3-SAT solver based on this prompt:

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 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.

Output
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise display unsatisfiable.

Sample Input

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

Sample Output satisfiable unsatisfiable

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.

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

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 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 seperated 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.