Tutorial 3 - 3SAT Solver¶
The Boolean Satisfiability Problem (or SAT) is a problem in logics and computer science of finding solutions to logical equations. For instance, if we know that two properties $A$ and $B$ are bound by $A \Rightarrow B$ and $A \Rightarrow not\ B$, we can deduce that $A$ must be false.
The SAT problem, and its variants, appear commonly in optimization algorithms, software verification, electronics circuit generation and validation, artificial intelligence, etc.
The SAT problem has been demonstrated to be NP-complete. As of this writing, there is no exact solver that can generally solve the SAT problem (or its simpler sibling 3SAT) in polynomial time. In this notebook, we will demonstrate how we can resolve a restricted version of SAT named 3SAT, using MIS. The ideas exposed here can easily be expanded into a general SAT solver, as well as solvers for entirely different classes of problems.
# imports
from mis import MISSolver, MISInstance, SolverConfig
from mis.shared.types import MISSolution
import networkx as nx
from collections import defaultdict
Representing our 3SAT instance¶
In 3SAT, we restrict ourselves to formulas that look like $$(A \vee B \vee \neg C) \wedge (D \vee C \vee E) \wedge ...$$
In other words an instance of 3SAT is a conjonction ("ands") of clauses, where each clauses is a disjunctions ("ors") of terms, where each term is either a variable or a negated variable. We further restrict that the same variable may not appear more than once in one clause (it may, of course, appear more than once in an instance).
From this, we want to convert our instance of 3SAT into an instance of MIS.
The general idea is that:
We want to convert an instance of 3SAT into a graph in which if a node is part of a MIS solution, it MUST be true (note that a node that is not part of a MIS solution may or may not be true, we don't care, as it does not contribute to the result) every term is compiled into a node in our graph
Since X and NOT X cannot be both true simultaneously, if there is a term X and a term NOT X, we connect their representations in our graph, to make sure that both of them cannot appear simultaneously in a solution to MIS
In every clause, we connect the three nodes in the graph, to make sure that only one of them MUST be true (This bounds the maximum number of nodes to the number of clauses)
Once we have a MIS solution, we only need to confirm that one node in each clause is part of the MIS solution, i.e. we only need to check the length of the MIS solution (Since the maximum number of nodes is the number of clauses, and that in each triangle representing a clause we can have at most one node, reaching a configuration with exactly the good number of nodes implies that the solution is valid).
class ThreeSATTerm:
"""
A 3SAT term, i.e. a variable (for instance "x3") and possibly a negation.
"""
variable: str
positive: bool
def __init__(self, variable : str, positive : bool):
self.variable = variable
self.positive = positive
def eval(self, values: dict[str, bool]) -> bool:
"""
Evaluate this term with the value of the variables as specified in `values`.
"""
if self.variable not in values:
raise ValueError(f"Variable '{self.variable}' not found in values.")
return values[self.variable] == self.positive
class ThreeSATClause:
"""
A 3SAT clause, i.e. T1 OR T2 OR T3 where T1, T2 and T3 are exactly three 3SAT terms.
"""
terms: list[ThreeSATTerm]
def __init__(self, terms : list[ThreeSATTerm]):
if len(terms) != 3:
raise ValueError("A 3SAT clause must have exactly three terms.")
self.terms = terms
def eval(self, values: dict[str, bool]) -> bool:
"""
Evaluate this clause with the value of the variables as specified in `values`.
Returns `True` if and only for any `term`, `term.eval(values)` returns `True`.
"""
if len(self.terms) != 3:
raise ValueError("A 3SAT clause must have exactly three terms.")
for term in self.terms:
if term.eval(values):
return True
return False
class ThreeSATInstance:
"""
A 3SAT instance, i.e. C1 AND C2 AND C3 AND Cn where each Ci is a 3SAT Clause.
"""
clauses: list[ThreeSATClause]
_variables: set[str]
def __init__(self, clauses : list[ThreeSATClause]):
self.clauses = clauses
self._variables = set()
for clause in self.clauses:
for term in clause.terms:
self._variables.add(term.variable)
def eval(self, values: dict[str, bool]) -> bool:
"""
Evaluate this instance with the value of the variables as specified in `values`.
Returns `True` if and only for each `clause`, `clause.eval(values)` returns `True`.
"""
for clause in self.clauses:
if not clause.eval(values):
return False
return True
def __len__(self) -> int:
"""
The number of clauses in this instance.
"""
return len(self.clauses)
def compile_to_mis(self) -> MISInstance:
"""
Compile this instance of 3SAT into an instance of MIS.
"""
# A mapping of variable to nodes.
#
# Keys: `VarName + "T"` (for terms that represent a positive variable) / `VarName + "F"` (for terms that represent a negative variable).
# Values: All the nodes found so far representing this term.
term_to_nodes : dict[str, list[int]] = defaultdict(lambda : []) # set the default value of a key to an empty list
def get_key(term, reverse) : return term.variable + ("F" if term.positive ^ reverse else "T")
"""
If a node representing X is part of the MIS, then X must be true;
If a node representing NOT X is part of the MIS, then NOT X must be true;
Otherwise, the term does not contribute to the solution (we don't care whether it's true or false).
"""
graph = nx.Graph()
for i in range(len(self.clauses)):
# From all the terms in one clause, it's sufficient that one of them be true.
graph.add_edges_from([(3*i,3*i+1), (3*i+1, 3*i+2), (3*i, 3*i+2)])
# If X is true, NOT X cannot be true and vice-versa.
for j in range(3):
for node in term_to_nodes[get_key(self.clauses[i].terms[j], True)]:
graph.add_edge(3*i + j, node)
# Add the new nodes to the cache
for j in range(3):
term_to_nodes[get_key(self.clauses[i].terms[j], False)].append(3*i+j)
return MISInstance(graph)
def rebuild_result_from_mis(self, solutions: list[MISSolution]) -> dict[str, bool] | None:
"""
Search in a list of MISSolution if any of them is a possible solution to 3SAT.
"""
if solutions is None:
return None
for solution in solutions:
if len(solution.nodes) != len(self.clauses):
continue # skip if the number of nodes isn't enough to be a solution
# otherwise, we have a solution
result = dict()
for variable in self._variables:
result[variable] = False # set the default of every variable to False in case the current solution makes them free
for node in solution.nodes:
term = self.clauses[node//3].terms[node%3] # since each node has index equal to 3*clause + term
result[term.variable] = term.positive
if not self.eval(result):
continue # The MIS provided is not valid, as the quantum algorithm is non-deterministic
return result
return None
# Testing our class
three_sat_instance_1 = ThreeSATInstance(clauses=[
ThreeSATClause([
ThreeSATTerm("X1", positive=True),
ThreeSATTerm("X2", positive=True),
ThreeSATTerm("X3", positive=True),
]),
ThreeSATClause([
ThreeSATTerm("X1", positive=True),
ThreeSATTerm("X2", positive=False),
ThreeSATTerm("X3", positive=False),
]),
])
Let's explore some possibilities :
print(three_sat_instance_1.eval({'X1': True, 'X2': True, 'X3': True})) # True
print(three_sat_instance_1.eval({'X1': False, 'X2': False, 'X3': False})) # False
print(three_sat_instance_1.eval({'X1': True, 'X2': False, 'X3': False})) # True
print(three_sat_instance_1.eval({'X1': False, 'X2': True, 'X3': True})) # False
True False True False
Time to try our solver :
config = SolverConfig()
# Create the MIS instance
instance = three_sat_instance_1.compile_to_mis()
# Run the solver
solver = MISSolver(instance, config)
solutions = solver.solve().result()
result = three_sat_instance_1.rebuild_result_from_mis(solutions)
if result is None:
print("No solution exists")
else:
print("Possible solution : ", result)
print(three_sat_instance_1.eval(result)) # Should output True
Possible solution : {'X2': False, 'X1': True, 'X3': False} True
Remark : Many solutions are actually possible, our algorithm takes the first suitable one it explored
Example 2 :¶
$(X_1 \text{ OR } \overline X_2 \text{ OR } X_1) \text{ AND } (\overline X_1 \text{ OR } \overline X_1 \text{ OR } \overline X_2) \text{ AND } ( X_2 \text{ OR } X_2 \text{ OR } X_2)$
This one actually doesn't have a solution as we will see :
three_sat_instance_2 = ThreeSATInstance(clauses=[
ThreeSATClause([
ThreeSATTerm("X1", positive=True),
ThreeSATTerm("X2", positive=False),
ThreeSATTerm("X1", positive=True),
]),
ThreeSATClause([
ThreeSATTerm("X1", positive=False),
ThreeSATTerm("X1", positive=False),
ThreeSATTerm("X2", positive=False),
]),
ThreeSATClause([
ThreeSATTerm("X2", positive=True),
ThreeSATTerm("X2", positive=True),
ThreeSATTerm("X2", positive=True),
]),
])
config = SolverConfig()
# Create the MIS instance
instance = three_sat_instance_2.compile_to_mis()
# Run the solver
solver = MISSolver(instance, config)
solutions = solver.solve().result()
result = three_sat_instance_2.rebuild_result_from_mis(solutions)
if result is None:
print("No solution exists")
else:
print("Possible solution : ", result)
print(three_sat_instance_2.eval(result))
# Should output "No Solution exists"
No solution exists
Example 3 :¶
$(X_1 \text{ OR } \overline X_2 \text{ OR } X_3) \text{ AND } (\overline X_1 \text{ OR } X_2 \text{ OR } \overline X_3) \text{ AND } (X_2 \text{ OR } X_3 \text{ OR } X_4) \text{ AND } (\overline X_2 \text{ OR } \overline X_3 \text{ OR } \overline X_4) \text{ AND } (X_1 \text{ OR } X_4 \text{ OR } \overline X_3)$
three_sat_instance_3 = ThreeSATInstance(clauses=[
ThreeSATClause([
ThreeSATTerm("X1", positive=True),
ThreeSATTerm("X2", positive=False),
ThreeSATTerm("X3", positive=True),
]),
ThreeSATClause([
ThreeSATTerm("X1", positive=False),
ThreeSATTerm("X2", positive=True),
ThreeSATTerm("X3", positive=False),
]),
ThreeSATClause([
ThreeSATTerm("X2", positive=True),
ThreeSATTerm("X3", positive=True),
ThreeSATTerm("X4", positive=True),
]),
ThreeSATClause([
ThreeSATTerm("X2", positive=False),
ThreeSATTerm("X3", positive=False),
ThreeSATTerm("X4", positive=False),
]),
ThreeSATClause([
ThreeSATTerm("X1", positive=True),
ThreeSATTerm("X4", positive=True),
ThreeSATTerm("X3", positive=False),
]),
])
config = SolverConfig()
# Create the MIS instance
instance = three_sat_instance_3.compile_to_mis()
# Run the solver
solver = MISSolver(instance, config)
solutions = solver.solve().result()
result = three_sat_instance_3.rebuild_result_from_mis(solutions)
if result is None:
print("No solution exists")
else:
print("Possible solution : ", result)
print(three_sat_instance_3.eval(result))
Possible solution : {'X2': False, 'X1': False, 'X4': True, 'X3': True} True