# 3-SAT Solver Python

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.

import sys

def GetReverse(literal):
if literal[0] == '~':
return literal[1:]
else:
return '~' + literal

for i in range(cases):

mySets = []

for c in firstClause:
this = set()
mySets.append(this)

for i in range(clauses-1):
tempSets = []

for s in mySets:
for literal in currentClause:

if not s.__contains__(GetReverse(literal)):

newset = s.copy()

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 = []

for s in mySets:
for literal in currentClause:

if not s.__contains__(GetReverse(literal)):

newset = s.copy()

tempSets.append(newset)
mySets = tempSets

• Welcome to the Code Review site, the title of the question should indicate what the code does, rather than your concerns about the code. Links can break so you should include the text of the programming challenge as well. Please read How do I ask a good question. Questions like this should include the programming-challenge tag. Commented Oct 22, 2020 at 13:56
• It looks like the code is not indented correctly. Shouldn't everything from mySets = [] to the end be indented under for i in range(cases):? Commented Oct 22, 2020 at 17:39
• There are indeed indentation problems. If you copy and paste this, the syntax errors will show you what's incorrect. Commented Oct 22, 2020 at 18:45

If you instrument your code with some strategically place print statements, you will see that there is some repeated computations going on. In the second test case when processing the clause X2 v ~X3, the set {'X1', 'X2'} gets added to mySets twice. When processing the clause X3 v ~X1, the set {'X3', 'X1', 'X2'} gets added to mySets three times.

For large cases, it might speed things up to change mySets to a set() instead of a list to eliminate the duplicates. Then the inner sets need to be frozensets.

mySets is a set of possible solutions that satisfy all the clauses, so I renamed it to candidates.

If you initialize candidates to contain a single empty set, then the first clause doesn't need to be handled separately.

I think you can stop anytime candidates is empty.

Also, split up the code into functions.

def is_satisfiable(n_vars, clauses):
candidates = {frozenset()}

for clause in clauses:
temp = set()

for s in candidates:
for literal in clause:

if GetReverse(literal) not in s:

candidates = temp

if len(candidates) == 0:
return False

return True

clauses = [f.readline().strip().split(' v ') for _ in range(int(n_clauses))]
return int(n_vars), clauses

def main(f=sys.stdin):

for i in range(num_cases):
result = is_satisfiable(n_vars, clauses)

print(f"{'satisfiable' if result else 'unsatisfiable'}")


Called like:

import io

data = """
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
""".strip()

main(io.StringIO(data))


or

import sys

main(sys.stdin)


Here's a suggested implementation that changes basically nothing about your algorithm, but

• has proper indentation
• uses a little bit of type hinting
• uses set literals and generators
• uses _ for "unused" variables
• adds a parse_clause() because the clause code is repeated
• uses a StringIO, for these purposes, to effectively mock away stdin and use the example input you showed
• uses PEP8-compliant names (with underscores)
from io import StringIO
from typing import List

stdin = StringIO('''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
'''
)

def get_reverse(literal: str) -> str:
if literal[0] == '~':
return literal[1:]
return '~' + literal

def parse_clause() -> List[str]:

for _ in range(n_cases):
n_vars, n_clauses = (int(s) for s in stdin.readline().split())
my_sets = [{c} for c in parse_clause()]

for _ in range(n_clauses - 1):
temp_sets = []
current_clause = parse_clause()

for s in my_sets:
for literal in current_clause:
if get_reverse(literal) not in s:
new_set = s.copy()