Last active
April 20, 2021 14:57
-
-
Save pqcfox/98961754e79b7434a2d1161d9ff933dc to your computer and use it in GitHub Desktop.
A tiny DPLL SAT solver in pure Python 🔬
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
"""sat.py: a simple DPLL SAT solver in pure python. | |
The API is designed to be as simple as possible: | |
>>> x = Var('x') | |
>>> y = Var('y') | |
>>> z = Var('z') | |
>>> DPLL([(x, y, z), | |
... (x, y, ~z), | |
... (x, ~y, z), | |
... (x, ~y, ~z), | |
... (~x, y, z), | |
... (~x, y, ~z), | |
... (~x, ~y, z), | |
... (~x, ~y, ~z)])) | |
None | |
>>> DPLL([(x, y, z), | |
... (x, y, ~z), | |
... (x, ~y, z), | |
... (x, ~y, ~z), | |
... (~x, y, z), | |
... (~x, y, ~z), | |
... (~x, ~y, z)]) | |
{'y': True, 'x': True, 'z': True} | |
Variable objects are identical when their names are. | |
""" | |
class Var: | |
"""A simple variable class for expressing CNF formulae.""" | |
def __init__(self, name): | |
"""Initializes the variable.""" | |
self.name = name | |
self.inverted = False | |
def __invert__(self): | |
"""Inverts the variable.""" | |
inverse = self.__class__(self.name) | |
inverse.inverted = not self.inverted | |
return inverse | |
def __str__(self): | |
"""Gives a short string representation of the variable.""" | |
return ('~' if self.inverted else '') + self.name | |
def __repr__(self): | |
"""Gives a precise string representation of the variable.""" | |
return 'Var(name={}, inverted={})'.format(self.name, self.inverted) | |
def __eq__(self, other): | |
"""Determines whether two variables are equal.""" | |
return self.name == other.name and self.inverted == other.inverted | |
def __ne__(self, other): | |
"""Determines whether two variables aren't equal.""" | |
return not self.__eq__(other) | |
def assign_to_true(var, clauses): | |
"""Assigns a variable to true in an expression, then simplifies.""" | |
new_clauses = [] | |
for clause in clauses: | |
if var in clause: | |
continue | |
new_clause = [clause_var for clause_var in clause | |
if clause_var != ~var] | |
new_clauses.append(new_clause) | |
return new_clauses | |
def find_pure_vars(clauses): | |
"""Finds all pure variables in a list of clauses.""" | |
seen_vars = [var for clause in clauses for var in clause] | |
return [var for var in seen_vars if ~var not in seen_vars] | |
def DPLL(clauses): | |
def DPLL_helper(clauses, values): | |
"""Determines if a list of CNF formulae is solvable.""" | |
# If all we have are literals, test if they're consistent | |
if all([len(clause) == 1 for clause in clauses]): | |
seen_vars = [] | |
for (var,) in clauses: | |
for seen_var in seen_vars: | |
name_match = (seen_var.name == var.name) | |
is_opposite = (seen_var.inverted != var.inverted) | |
if name_match and is_opposite: | |
return None | |
seen_vars.append(var) | |
values[var.name] = not var.inverted | |
return values | |
# Perform unit propagation on every unit clause | |
unit_clauses = [clause for clause in clauses if len(clause) == 1] | |
for unit_clause in unit_clauses: | |
(var,) = unit_clause | |
clauses = assign_to_true(var, clauses) | |
values[var.name] = not var.inverted | |
# Find pure literals and assign them properly | |
for var in find_pure_vars(clauses): | |
clauses = assign_to_true(var, clauses) | |
values[var.name] = not var.inverted | |
# Check if we're done | |
if len(clauses) == 0: | |
return values | |
# If we have any empty clauses, we can't satisfy those | |
if any([len(clause) == 0 for clause in clauses]): | |
return None | |
# Explore by choosing a literal | |
var = clauses[0][0] | |
# Try assinging the variable to true | |
values[var.name] = not var.inverted | |
with_true = DPLL_helper(assign_to_true(var, clauses), values) | |
if with_true is not None: | |
return with_true | |
# Try assigning the variable to false | |
values[var.name] = var.inverted | |
with_false = DPLL_helper(assign_to_true(var, clauses), values) | |
return with_false | |
return DPLL_helper(clauses, {}) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment