modelparameters.sympy.logic.algorithms package

Submodules

modelparameters.sympy.logic.algorithms.dpll module

Implementation of DPLL algorithm

Further improvements: eliminate calls to pl_true, implement branching rules, efficient unit propagation.

References

modelparameters.sympy.logic.algorithms.dpll.dpll(clauses, symbols, model)[source]

Compute satisfiability in a partial model. Clauses is an array of conjuncts.

>>> from ...abc import A, B, D
>>> from .dpll import dpll
>>> dpll([A, B, D], [A, B], {D: False})
False
modelparameters.sympy.logic.algorithms.dpll.dpll_int_repr(clauses, symbols, model)[source]

Compute satisfiability in a partial model. Arguments are expected to be in integer representation

>>> from .dpll import dpll_int_repr
>>> dpll_int_repr([{1}, {2}, {3}], {1, 2}, {3: False})
False
modelparameters.sympy.logic.algorithms.dpll.dpll_satisfiable(expr)[source]

Check satisfiability of a propositional sentence. It returns a model rather than True when it succeeds

>>> from ...abc import A, B
>>> from .dpll import dpll_satisfiable
>>> dpll_satisfiable(A & ~B)
{A: True, B: False}
>>> dpll_satisfiable(A & ~A)
False
modelparameters.sympy.logic.algorithms.dpll.find_pure_symbol(symbols, unknown_clauses)[source]

Find a symbol and its value if it appears only as a positive literal (or only as a negative) in clauses.

>>> from ... import symbols
>>> from ...abc import A, B, D
>>> from .dpll import find_pure_symbol
>>> find_pure_symbol([A, B, D], [A|~B,~B|~D,D|A])
(A, True)
modelparameters.sympy.logic.algorithms.dpll.find_pure_symbol_int_repr(symbols, unknown_clauses)[source]

Same as find_pure_symbol, but arguments are expected to be in integer representation

>>> from .dpll import find_pure_symbol_int_repr
>>> find_pure_symbol_int_repr({1,2,3},
...     [{1, -2}, {-2, -3}, {3, 1}])
(1, True)
modelparameters.sympy.logic.algorithms.dpll.find_unit_clause(clauses, model)[source]

A unit clause has only 1 variable that is not bound in the model.

>>> from ... import symbols
>>> from ...abc import A, B, D
>>> from .dpll import find_unit_clause
>>> find_unit_clause([A | B | D, B | ~D, A | ~B], {A:True})
(B, False)
modelparameters.sympy.logic.algorithms.dpll.find_unit_clause_int_repr(clauses, model)[source]

Same as find_unit_clause, but arguments are expected to be in integer representation.

>>> from .dpll import find_unit_clause_int_repr
>>> find_unit_clause_int_repr([{1, 2, 3},
...     {2, -3}, {1, -2}], {1: True})
(2, False)
modelparameters.sympy.logic.algorithms.dpll.pl_true_int_repr(clause, model={})[source]

Lightweight version of pl_true. Argument clause represents the set of args of an Or clause. This is used inside dpll_int_repr, it is not meant to be used directly.

>>> from .dpll import pl_true_int_repr
>>> pl_true_int_repr({1, 2}, {1: False})
>>> pl_true_int_repr({1, 2}, {1: False, 2: False})
False
modelparameters.sympy.logic.algorithms.dpll.unit_propagate(clauses, symbol)[source]

Returns an equivalent set of clauses If a set of clauses contains the unit clause l, the other clauses are simplified by the application of the two following rules:

  1. every clause containing l is removed

  2. in every clause that contains ~l this literal is deleted

Arguments are expected to be in CNF.

>>> from ... import symbols
>>> from ...abc import A, B, D
>>> from .dpll import unit_propagate
>>> unit_propagate([A | B, D | ~B, B], B)
[D, B]
modelparameters.sympy.logic.algorithms.dpll.unit_propagate_int_repr(clauses, s)[source]

Same as unit_propagate, but arguments are expected to be in integer representation

>>> from .dpll import unit_propagate_int_repr
>>> unit_propagate_int_repr([{1, 2}, {3, -2}, {2}], 2)
[{3}]

modelparameters.sympy.logic.algorithms.dpll2 module

Implementation of DPLL algorithm

Features:

  • Clause learning

  • Watch literal scheme

  • VSIDS heuristic

References

class modelparameters.sympy.logic.algorithms.dpll2.Level(decision, flipped=False)[source]

Bases: object

Represents a single level in the DPLL algorithm, and contains enough information for a sound backtracking procedure.

class modelparameters.sympy.logic.algorithms.dpll2.SATSolver(clauses, variables, var_settings, symbols=None, heuristic='vsids', clause_learning='none', INTERVAL=500)[source]

Bases: object

Class for representing a SAT solver capable of

finding a model to a boolean theory in conjunctive normal form.

modelparameters.sympy.logic.algorithms.dpll2.dpll_satisfiable(expr, all_models=False)[source]

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 ...abc import A, B
>>> from .dpll2 import dpll_satisfiable
>>> dpll_satisfiable(A & ~B)
{A: True, B: False}
>>> dpll_satisfiable(A & ~A)
False

Module contents