other.davis_putnam_logemann_loveland

Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e, for solving the Conjunctive Normal Form SATisfiability (CNF-SAT) problem.

For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm

Attributes

formula

Classes

Clause

Formula

Functions

dpll_algorithm(→ tuple[bool | None, dict[str, ...)

Returns the model if the formula is satisfiable, else None

find_pure_symbols(→ tuple[list[str], dict[str, ...)

find_unit_clauses(→ tuple[list[str], dict[str, ...)

Returns the unit symbols and their values to satisfy clause.

generate_clause(→ Clause)

generate_formula(→ Formula)

Randomly generate a formula.

generate_parameters(→ tuple[list[Clause], list[str]])

Module Contents

class other.davis_putnam_logemann_loveland.Clause(literals: list[str])
A clause represented in Conjunctive Normal Form.
A clause is a set of literals, either complemented or otherwise.
For example:

  • {A1, A2, A3’} is the clause (A1 v A2 v A3’)

  • {A5’, A2’, A1} is the clause (A5’ v A2’ v A1)

Create model

>>> clause = Clause(["A1", "A2'", "A3"])
>>> clause.evaluate({"A1": True})
True
__len__() → int

To print a clause as in Conjunctive Normal Form.

>>> len(Clause([]))
0
>>> len(Clause(["A1", "A2'", "A3"]))
3
__str__() → str

To print a clause as in Conjunctive Normal Form.

>>> str(Clause(["A1", "A2'", "A3"]))
"{A1 , A2' , A3}"
assign(model: dict[str, bool | None]) → None

Assign values to literals of the clause as given by model.

evaluate(model: dict[str, bool | None]) → bool | None

Evaluates the clause with the assignments in model.

This has the following steps:

  1. Return True if both a literal and its complement exist in the clause.

  2. Return True if a single literal has the assignment True.

  3. Return None (unable to complete evaluation) if a literal has no assignment.

  4. Compute disjunction of all values assigned in clause.

literals: dict[str, bool | None]
class other.davis_putnam_logemann_loveland.Formula(clauses: collections.abc.Iterable[Clause])
A formula represented in Conjunctive Normal Form.
A formula is a set of clauses.
For example,
{{A1, A2, A3’}, {A5’, A2’, A1}} is ((A1 v A2 v A3’) and (A5’ v A2’ v A1))
__str__() → str

To print a formula as in Conjunctive Normal Form.

>>> str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
"{{A1 , A2' , A3} , {A5' , A2' , A1}}"
clauses
other.davis_putnam_logemann_loveland.dpll_algorithm(clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]) → tuple[bool | None, dict[str, bool | None] | None]

Returns the model if the formula is satisfiable, else None

This has the following steps:

  1. If every clause in clauses is True, return True.

  2. If some clause in clauses is False, return False.

  3. Find pure symbols.

  4. Find unit symbols.

>>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
>>> clauses, symbols = generate_parameters(formula)
>>> soln, model = dpll_algorithm(clauses, symbols, {})
>>> soln
True
>>> model
{'A4': True}
other.davis_putnam_logemann_loveland.find_pure_symbols(clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]) → tuple[list[str], dict[str, bool | None]]
Return pure symbols and their values to satisfy clause.
Pure symbols are symbols in a formula that exist only in one form,
either complemented or otherwise.
For example,
{{A4 , A3 , A5’ , A1 , A3’} , {A4} , {A3}} has pure symbols A4, A5’ and A1.
This has the following steps:

  1. Ignore clauses that have already evaluated to be True.

  2. Find symbols that occur only in one form in the rest of the clauses.

  3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively.

>>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
>>> clauses, symbols = generate_parameters(formula)
>>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
>>> pure_symbols
['A1', 'A2', 'A3', 'A5']
>>> values
{'A1': True, 'A2': False, 'A3': True, 'A5': False}
other.davis_putnam_logemann_loveland.find_unit_clauses(clauses: list[Clause], model: dict[str, bool | None]) → tuple[list[str], dict[str, bool | None]]

Returns the unit symbols and their values to satisfy clause.

Unit symbols are symbols in a formula that are:

  • Either the only symbol in a clause

  • Or all other literals in that clause have been assigned False

This has the following steps:

  1. Find symbols that are the only occurrences in a clause.

  2. Find symbols in a clause where all other literals are assigned False.

  3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively.

>>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
>>> clause2 = Clause(["A4"])
>>> clause3 = Clause(["A3"])
>>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
>>> unit_clauses, values = find_unit_clauses(clauses, {})
>>> unit_clauses
['A4', 'A3']
>>> values
{'A4': True, 'A3': True}
other.davis_putnam_logemann_loveland.generate_clause() → Clause
Randomly generate a clause.
All literals have the name Ax, where x is an integer from 1 to 5.
other.davis_putnam_logemann_loveland.generate_formula() → Formula

Randomly generate a formula.

other.davis_putnam_logemann_loveland.generate_parameters(formula: Formula) → tuple[list[Clause], list[str]]
Return the clauses and symbols from a formula.
A symbol is the uncomplemented form of a literal.
For example,

  • Symbol of A3 is A3.

  • Symbol of A5’ is A5.

>>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
>>> clauses, symbols = generate_parameters(formula)
>>> clauses_list = [str(i) for i in clauses]
>>> clauses_list
["{A1 , A2' , A3}", "{A5' , A2' , A1}"]
>>> symbols
['A1', 'A2', 'A3', 'A5']
other.davis_putnam_logemann_loveland.formula