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

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

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

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

preprocessing - current kernel size is 6

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 = 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"

preprocessing - current kernel size is 9

preprocessing - current kernel size is 2

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

preprocessing - current kernel size is 15

preprocessing - current kernel size is 11

preprocessing - current kernel size is 1

Possible solution :  {'X4': True, 'X2': False, 'X1': False, 'X3': True}
True

Previous
Tutorial 2 - GreedyMIS Example Use Case Next
Tutorial 4 - Graph Coloring Solver