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.

In [1]:

# imports
from mis import MISSolver, MISInstance, SolverConfig
from mis.shared.types import MISSolution
import networkx as nx
from collections import defaultdict

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

In [2]:

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
    
    

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¶

Example 1¶

$(X_1 \text{ OR } X_2 \text{ OR } X_3) \text{ AND }(X_1 \text{ OR } \overline X_2 \text{ OR } \overline X_3)$

Initializing our instance :

In [3]:

# 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),
   ]),
])

# 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 :

In [4]:

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

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 :

In [5]:

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

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 :

In [6]:

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"

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)$

In [7]:

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

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