660 lines
20 KiB
Python
660 lines
20 KiB
Python
"""Implementation of DPLL algorithm
|
|
|
|
Features:
|
|
- Clause learning
|
|
- Watch literal scheme
|
|
- VSIDS heuristic
|
|
|
|
References:
|
|
- https://en.wikipedia.org/wiki/DPLL_algorithm
|
|
"""
|
|
|
|
from collections import defaultdict
|
|
from heapq import heappush, heappop
|
|
|
|
from sympy.core.sorting import ordered
|
|
from sympy.assumptions.cnf import EncodedCNF
|
|
|
|
|
|
def dpll_satisfiable(expr, all_models=False):
|
|
"""
|
|
Check satisfiability of a propositional sentence.
|
|
It returns a model rather than True when it succeeds.
|
|
Returns a generator of all models if all_models is True.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.abc import A, B
|
|
>>> from sympy.logic.algorithms.dpll2 import dpll_satisfiable
|
|
>>> dpll_satisfiable(A & ~B)
|
|
{A: True, B: False}
|
|
>>> dpll_satisfiable(A & ~A)
|
|
False
|
|
|
|
"""
|
|
if not isinstance(expr, EncodedCNF):
|
|
exprs = EncodedCNF()
|
|
exprs.add_prop(expr)
|
|
expr = exprs
|
|
|
|
# Return UNSAT when False (encoded as 0) is present in the CNF
|
|
if {0} in expr.data:
|
|
if all_models:
|
|
return (f for f in [False])
|
|
return False
|
|
|
|
solver = SATSolver(expr.data, expr.variables, set(), expr.symbols)
|
|
models = solver._find_model()
|
|
|
|
if all_models:
|
|
return _all_models(models)
|
|
|
|
try:
|
|
return next(models)
|
|
except StopIteration:
|
|
return False
|
|
|
|
# Uncomment to confirm the solution is valid (hitting set for the clauses)
|
|
#else:
|
|
#for cls in clauses_int_repr:
|
|
#assert solver.var_settings.intersection(cls)
|
|
|
|
|
|
def _all_models(models):
|
|
satisfiable = False
|
|
try:
|
|
while True:
|
|
yield next(models)
|
|
satisfiable = True
|
|
except StopIteration:
|
|
if not satisfiable:
|
|
yield False
|
|
|
|
|
|
class SATSolver:
|
|
"""
|
|
Class for representing a SAT solver capable of
|
|
finding a model to a boolean theory in conjunctive
|
|
normal form.
|
|
"""
|
|
|
|
def __init__(self, clauses, variables, var_settings, symbols=None,
|
|
heuristic='vsids', clause_learning='none', INTERVAL=500):
|
|
|
|
self.var_settings = var_settings
|
|
self.heuristic = heuristic
|
|
self.is_unsatisfied = False
|
|
self._unit_prop_queue = []
|
|
self.update_functions = []
|
|
self.INTERVAL = INTERVAL
|
|
|
|
if symbols is None:
|
|
self.symbols = list(ordered(variables))
|
|
else:
|
|
self.symbols = symbols
|
|
|
|
self._initialize_variables(variables)
|
|
self._initialize_clauses(clauses)
|
|
|
|
if 'vsids' == heuristic:
|
|
self._vsids_init()
|
|
self.heur_calculate = self._vsids_calculate
|
|
self.heur_lit_assigned = self._vsids_lit_assigned
|
|
self.heur_lit_unset = self._vsids_lit_unset
|
|
self.heur_clause_added = self._vsids_clause_added
|
|
|
|
# Note: Uncomment this if/when clause learning is enabled
|
|
#self.update_functions.append(self._vsids_decay)
|
|
|
|
else:
|
|
raise NotImplementedError
|
|
|
|
if 'simple' == clause_learning:
|
|
self.add_learned_clause = self._simple_add_learned_clause
|
|
self.compute_conflict = self.simple_compute_conflict
|
|
self.update_functions.append(self.simple_clean_clauses)
|
|
elif 'none' == clause_learning:
|
|
self.add_learned_clause = lambda x: None
|
|
self.compute_conflict = lambda: None
|
|
else:
|
|
raise NotImplementedError
|
|
|
|
# Create the base level
|
|
self.levels = [Level(0)]
|
|
self._current_level.varsettings = var_settings
|
|
|
|
# Keep stats
|
|
self.num_decisions = 0
|
|
self.num_learned_clauses = 0
|
|
self.original_num_clauses = len(self.clauses)
|
|
|
|
def _initialize_variables(self, variables):
|
|
"""Set up the variable data structures needed."""
|
|
self.sentinels = defaultdict(set)
|
|
self.occurrence_count = defaultdict(int)
|
|
self.variable_set = [False] * (len(variables) + 1)
|
|
|
|
def _initialize_clauses(self, clauses):
|
|
"""Set up the clause data structures needed.
|
|
|
|
For each clause, the following changes are made:
|
|
- Unit clauses are queued for propagation right away.
|
|
- Non-unit clauses have their first and last literals set as sentinels.
|
|
- The number of clauses a literal appears in is computed.
|
|
"""
|
|
self.clauses = [list(clause) for clause in clauses]
|
|
|
|
for i, clause in enumerate(self.clauses):
|
|
|
|
# Handle the unit clauses
|
|
if 1 == len(clause):
|
|
self._unit_prop_queue.append(clause[0])
|
|
continue
|
|
|
|
self.sentinels[clause[0]].add(i)
|
|
self.sentinels[clause[-1]].add(i)
|
|
|
|
for lit in clause:
|
|
self.occurrence_count[lit] += 1
|
|
|
|
def _find_model(self):
|
|
"""
|
|
Main DPLL loop. Returns a generator of models.
|
|
|
|
Variables are chosen successively, and assigned to be either
|
|
True or False. If a solution is not found with this setting,
|
|
the opposite is chosen and the search continues. The solver
|
|
halts when every variable has a setting.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> list(l._find_model())
|
|
[{1: True, 2: False, 3: False}, {1: True, 2: True, 3: True}]
|
|
|
|
>>> from sympy.abc import A, B, C
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set(), [A, B, C])
|
|
>>> list(l._find_model())
|
|
[{A: True, B: False, C: False}, {A: True, B: True, C: True}]
|
|
|
|
"""
|
|
|
|
# We use this variable to keep track of if we should flip a
|
|
# variable setting in successive rounds
|
|
flip_var = False
|
|
|
|
# Check if unit prop says the theory is unsat right off the bat
|
|
self._simplify()
|
|
if self.is_unsatisfied:
|
|
return
|
|
|
|
# While the theory still has clauses remaining
|
|
while True:
|
|
# Perform cleanup / fixup at regular intervals
|
|
if self.num_decisions % self.INTERVAL == 0:
|
|
for func in self.update_functions:
|
|
func()
|
|
|
|
if flip_var:
|
|
# We have just backtracked and we are trying to opposite literal
|
|
flip_var = False
|
|
lit = self._current_level.decision
|
|
|
|
else:
|
|
# Pick a literal to set
|
|
lit = self.heur_calculate()
|
|
self.num_decisions += 1
|
|
|
|
# Stopping condition for a satisfying theory
|
|
if 0 == lit:
|
|
yield {self.symbols[abs(lit) - 1]:
|
|
lit > 0 for lit in self.var_settings}
|
|
while self._current_level.flipped:
|
|
self._undo()
|
|
if len(self.levels) == 1:
|
|
return
|
|
flip_lit = -self._current_level.decision
|
|
self._undo()
|
|
self.levels.append(Level(flip_lit, flipped=True))
|
|
flip_var = True
|
|
continue
|
|
|
|
# Start the new decision level
|
|
self.levels.append(Level(lit))
|
|
|
|
# Assign the literal, updating the clauses it satisfies
|
|
self._assign_literal(lit)
|
|
|
|
# _simplify the theory
|
|
self._simplify()
|
|
|
|
# Check if we've made the theory unsat
|
|
if self.is_unsatisfied:
|
|
|
|
self.is_unsatisfied = False
|
|
|
|
# We unroll all of the decisions until we can flip a literal
|
|
while self._current_level.flipped:
|
|
self._undo()
|
|
|
|
# If we've unrolled all the way, the theory is unsat
|
|
if 1 == len(self.levels):
|
|
return
|
|
|
|
# Detect and add a learned clause
|
|
self.add_learned_clause(self.compute_conflict())
|
|
|
|
# Try the opposite setting of the most recent decision
|
|
flip_lit = -self._current_level.decision
|
|
self._undo()
|
|
self.levels.append(Level(flip_lit, flipped=True))
|
|
flip_var = True
|
|
|
|
########################
|
|
# Helper Methods #
|
|
########################
|
|
@property
|
|
def _current_level(self):
|
|
"""The current decision level data structure
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{1}, {2}], {1, 2}, set())
|
|
>>> next(l._find_model())
|
|
{1: True, 2: True}
|
|
>>> l._current_level.decision
|
|
0
|
|
>>> l._current_level.flipped
|
|
False
|
|
>>> l._current_level.var_settings
|
|
{1, 2}
|
|
|
|
"""
|
|
return self.levels[-1]
|
|
|
|
def _clause_sat(self, cls):
|
|
"""Check if a clause is satisfied by the current variable setting.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{1}, {-1}], {1}, set())
|
|
>>> try:
|
|
... next(l._find_model())
|
|
... except StopIteration:
|
|
... pass
|
|
>>> l._clause_sat(0)
|
|
False
|
|
>>> l._clause_sat(1)
|
|
True
|
|
|
|
"""
|
|
for lit in self.clauses[cls]:
|
|
if lit in self.var_settings:
|
|
return True
|
|
return False
|
|
|
|
def _is_sentinel(self, lit, cls):
|
|
"""Check if a literal is a sentinel of a given clause.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> next(l._find_model())
|
|
{1: True, 2: False, 3: False}
|
|
>>> l._is_sentinel(2, 3)
|
|
True
|
|
>>> l._is_sentinel(-3, 1)
|
|
False
|
|
|
|
"""
|
|
return cls in self.sentinels[lit]
|
|
|
|
def _assign_literal(self, lit):
|
|
"""Make a literal assignment.
|
|
|
|
The literal assignment must be recorded as part of the current
|
|
decision level. Additionally, if the literal is marked as a
|
|
sentinel of any clause, then a new sentinel must be chosen. If
|
|
this is not possible, then unit propagation is triggered and
|
|
another literal is added to the queue to be set in the future.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> next(l._find_model())
|
|
{1: True, 2: False, 3: False}
|
|
>>> l.var_settings
|
|
{-3, -2, 1}
|
|
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> l._assign_literal(-1)
|
|
>>> try:
|
|
... next(l._find_model())
|
|
... except StopIteration:
|
|
... pass
|
|
>>> l.var_settings
|
|
{-1}
|
|
|
|
"""
|
|
self.var_settings.add(lit)
|
|
self._current_level.var_settings.add(lit)
|
|
self.variable_set[abs(lit)] = True
|
|
self.heur_lit_assigned(lit)
|
|
|
|
sentinel_list = list(self.sentinels[-lit])
|
|
|
|
for cls in sentinel_list:
|
|
if not self._clause_sat(cls):
|
|
other_sentinel = None
|
|
for newlit in self.clauses[cls]:
|
|
if newlit != -lit:
|
|
if self._is_sentinel(newlit, cls):
|
|
other_sentinel = newlit
|
|
elif not self.variable_set[abs(newlit)]:
|
|
self.sentinels[-lit].remove(cls)
|
|
self.sentinels[newlit].add(cls)
|
|
other_sentinel = None
|
|
break
|
|
|
|
# Check if no sentinel update exists
|
|
if other_sentinel:
|
|
self._unit_prop_queue.append(other_sentinel)
|
|
|
|
def _undo(self):
|
|
"""
|
|
_undo the changes of the most recent decision level.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> next(l._find_model())
|
|
{1: True, 2: False, 3: False}
|
|
>>> level = l._current_level
|
|
>>> level.decision, level.var_settings, level.flipped
|
|
(-3, {-3, -2}, False)
|
|
>>> l._undo()
|
|
>>> level = l._current_level
|
|
>>> level.decision, level.var_settings, level.flipped
|
|
(0, {1}, False)
|
|
|
|
"""
|
|
# Undo the variable settings
|
|
for lit in self._current_level.var_settings:
|
|
self.var_settings.remove(lit)
|
|
self.heur_lit_unset(lit)
|
|
self.variable_set[abs(lit)] = False
|
|
|
|
# Pop the level off the stack
|
|
self.levels.pop()
|
|
|
|
#########################
|
|
# Propagation #
|
|
#########################
|
|
"""
|
|
Propagation methods should attempt to soundly simplify the boolean
|
|
theory, and return True if any simplification occurred and False
|
|
otherwise.
|
|
"""
|
|
def _simplify(self):
|
|
"""Iterate over the various forms of propagation to simplify the theory.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> l.variable_set
|
|
[False, False, False, False]
|
|
>>> l.sentinels
|
|
{-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
|
|
|
|
>>> l._simplify()
|
|
|
|
>>> l.variable_set
|
|
[False, True, False, False]
|
|
>>> l.sentinels
|
|
{-3: {0, 2}, -2: {3, 4}, -1: set(), 2: {0, 3},
|
|
...3: {2, 4}}
|
|
|
|
"""
|
|
changed = True
|
|
while changed:
|
|
changed = False
|
|
changed |= self._unit_prop()
|
|
changed |= self._pure_literal()
|
|
|
|
def _unit_prop(self):
|
|
"""Perform unit propagation on the current theory."""
|
|
result = len(self._unit_prop_queue) > 0
|
|
while self._unit_prop_queue:
|
|
next_lit = self._unit_prop_queue.pop()
|
|
if -next_lit in self.var_settings:
|
|
self.is_unsatisfied = True
|
|
self._unit_prop_queue = []
|
|
return False
|
|
else:
|
|
self._assign_literal(next_lit)
|
|
|
|
return result
|
|
|
|
def _pure_literal(self):
|
|
"""Look for pure literals and assign them when found."""
|
|
return False
|
|
|
|
#########################
|
|
# Heuristics #
|
|
#########################
|
|
def _vsids_init(self):
|
|
"""Initialize the data structures needed for the VSIDS heuristic."""
|
|
self.lit_heap = []
|
|
self.lit_scores = {}
|
|
|
|
for var in range(1, len(self.variable_set)):
|
|
self.lit_scores[var] = float(-self.occurrence_count[var])
|
|
self.lit_scores[-var] = float(-self.occurrence_count[-var])
|
|
heappush(self.lit_heap, (self.lit_scores[var], var))
|
|
heappush(self.lit_heap, (self.lit_scores[-var], -var))
|
|
|
|
def _vsids_decay(self):
|
|
"""Decay the VSIDS scores for every literal.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
|
|
>>> l.lit_scores
|
|
{-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
|
|
|
|
>>> l._vsids_decay()
|
|
|
|
>>> l.lit_scores
|
|
{-3: -1.0, -2: -1.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -1.0}
|
|
|
|
"""
|
|
# We divide every literal score by 2 for a decay factor
|
|
# Note: This doesn't change the heap property
|
|
for lit in self.lit_scores.keys():
|
|
self.lit_scores[lit] /= 2.0
|
|
|
|
def _vsids_calculate(self):
|
|
"""
|
|
VSIDS Heuristic Calculation
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
|
|
>>> l.lit_heap
|
|
[(-2.0, -3), (-2.0, 2), (-2.0, -2), (0.0, 1), (-2.0, 3), (0.0, -1)]
|
|
|
|
>>> l._vsids_calculate()
|
|
-3
|
|
|
|
>>> l.lit_heap
|
|
[(-2.0, -2), (-2.0, 2), (0.0, -1), (0.0, 1), (-2.0, 3)]
|
|
|
|
"""
|
|
if len(self.lit_heap) == 0:
|
|
return 0
|
|
|
|
# Clean out the front of the heap as long the variables are set
|
|
while self.variable_set[abs(self.lit_heap[0][1])]:
|
|
heappop(self.lit_heap)
|
|
if len(self.lit_heap) == 0:
|
|
return 0
|
|
|
|
return heappop(self.lit_heap)[1]
|
|
|
|
def _vsids_lit_assigned(self, lit):
|
|
"""Handle the assignment of a literal for the VSIDS heuristic."""
|
|
pass
|
|
|
|
def _vsids_lit_unset(self, lit):
|
|
"""Handle the unsetting of a literal for the VSIDS heuristic.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> l.lit_heap
|
|
[(-2.0, -3), (-2.0, 2), (-2.0, -2), (0.0, 1), (-2.0, 3), (0.0, -1)]
|
|
|
|
>>> l._vsids_lit_unset(2)
|
|
|
|
>>> l.lit_heap
|
|
[(-2.0, -3), (-2.0, -2), (-2.0, -2), (-2.0, 2), (-2.0, 3), (0.0, -1),
|
|
...(-2.0, 2), (0.0, 1)]
|
|
|
|
"""
|
|
var = abs(lit)
|
|
heappush(self.lit_heap, (self.lit_scores[var], var))
|
|
heappush(self.lit_heap, (self.lit_scores[-var], -var))
|
|
|
|
def _vsids_clause_added(self, cls):
|
|
"""Handle the addition of a new clause for the VSIDS heuristic.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
|
|
>>> l.num_learned_clauses
|
|
0
|
|
>>> l.lit_scores
|
|
{-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
|
|
|
|
>>> l._vsids_clause_added({2, -3})
|
|
|
|
>>> l.num_learned_clauses
|
|
1
|
|
>>> l.lit_scores
|
|
{-3: -1.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -2.0}
|
|
|
|
"""
|
|
self.num_learned_clauses += 1
|
|
for lit in cls:
|
|
self.lit_scores[lit] += 1
|
|
|
|
########################
|
|
# Clause Learning #
|
|
########################
|
|
def _simple_add_learned_clause(self, cls):
|
|
"""Add a new clause to the theory.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
|
|
>>> l.num_learned_clauses
|
|
0
|
|
>>> l.clauses
|
|
[[2, -3], [1], [3, -3], [2, -2], [3, -2]]
|
|
>>> l.sentinels
|
|
{-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
|
|
|
|
>>> l._simple_add_learned_clause([3])
|
|
|
|
>>> l.clauses
|
|
[[2, -3], [1], [3, -3], [2, -2], [3, -2], [3]]
|
|
>>> l.sentinels
|
|
{-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4, 5}}
|
|
|
|
"""
|
|
cls_num = len(self.clauses)
|
|
self.clauses.append(cls)
|
|
|
|
for lit in cls:
|
|
self.occurrence_count[lit] += 1
|
|
|
|
self.sentinels[cls[0]].add(cls_num)
|
|
self.sentinels[cls[-1]].add(cls_num)
|
|
|
|
self.heur_clause_added(cls)
|
|
|
|
def _simple_compute_conflict(self):
|
|
""" Build a clause representing the fact that at least one decision made
|
|
so far is wrong.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.algorithms.dpll2 import SATSolver
|
|
>>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
|
|
... {3, -2}], {1, 2, 3}, set())
|
|
>>> next(l._find_model())
|
|
{1: True, 2: False, 3: False}
|
|
>>> l._simple_compute_conflict()
|
|
[3]
|
|
|
|
"""
|
|
return [-(level.decision) for level in self.levels[1:]]
|
|
|
|
def _simple_clean_clauses(self):
|
|
"""Clean up learned clauses."""
|
|
pass
|
|
|
|
|
|
class Level:
|
|
"""
|
|
Represents a single level in the DPLL algorithm, and contains
|
|
enough information for a sound backtracking procedure.
|
|
"""
|
|
|
|
def __init__(self, decision, flipped=False):
|
|
self.decision = decision
|
|
self.var_settings = set()
|
|
self.flipped = flipped
|