Python:实现DPLL（davisb putnamb logemannb loveland）算法
from __future__ import annotations
import random
from collections.abc import Iterable
class Clause:
"""
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
"""
def __init__(self, literals: list[str]) -> None:
"""
Represent the literals and an assignment in a clause."
"""
# Assign all literals to None initially
self.literals: dict[str, bool | None] = {literal: None for literal in literals}
def __str__(self) -> str:
"""
To print a clause as in Conjunctive Normal Form.
>>> str(Clause(["A1", "A2'", "A3"]))
"{A1 , A2' , A3}"
"""
return "{" + " , ".join(self.literals) + "}"
def __len__(self) -> int:
"""
To print a clause as in Conjunctive Normal Form.
>>> len(Clause([]))
0
>>> len(Clause(["A1", "A2'", "A3"]))
3
"""
return len(self.literals)
def assign(self, model: dict[str, bool | None]) -> None:
"""
Assign values to literals of the clause as given by model.
"""
for literal in self.literals:
symbol = literal[:2]
if symbol in model:
value = model[symbol]
else:
continue
if value is not None:
# Complement assignment if literal is in complemented form
if literal.endswith("'"):
value = not value
self.literals[literal] = value
def evaluate(self, 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.
"""
for literal in self.literals:
symbol = literal.rstrip("'") if literal.endswith("'") else literal + "'"
if symbol in self.literals:
return True
self.assign(model)
for value in self.literals.values():
if value in (True, None):
return value
return any(self.literals.values())
class Formula:
"""
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))
"""
def __init__(self, clauses: Iterable[Clause]) -> None:
"""
Represent the number of clauses and the clauses themselves.
"""
self.clauses = list(clauses)
def __str__(self) -> 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}}"
"""
return "{" + " , ".join(str(clause) for clause in self.clauses) + "}"
def generate_clause() -> Clause:
"""
Randomly generate a clause.
All literals have the name Ax, where x is an integer from 1 to 5.
"""
literals = []
no_of_literals = random.randint(1, 5)
base_var = "A"
i = 0
while i < no_of_literals:
var_no = random.randint(1, 5)
var_name = base_var + str(var_no)
var_complement = random.randint(0, 1)
if var_complement == 1:
var_name += "'"
if var_name in literals:
i -= 1
else:
literals.append(var_name)
i += 1
return Clause(literals)
def generate_formula() -> Formula:
"""
Randomly generate a formula.
"""
clauses: set[Clause] = set()
no_of_clauses = random.randint(1, 10)
while len(clauses) < no_of_clauses:
clauses.add(generate_clause())
return Formula(clauses)
def generate_parameters(formula: Formula) -> tuple[list[Clause], list[str]]:
clauses = formula.clauses
symbols_set = []
for clause in formula.clauses:
for literal in clause.literals:
symbol = literal[:2]
if symbol not in symbols_set:
symbols_set.append(symbol)
return clauses, symbols_set
def find_pure_symbols(
clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]
) -> tuple[list[str], dict[str, bool | None]]:
pure_symbols = []
assignment: dict[str, bool | None] = dict()
literals = []
for clause in clauses:
if clause.evaluate(model):
continue
for literal in clause.literals:
literals.append(literal)
for s in symbols:
sym = s + "'"
if (s in literals and sym not in literals) or (
s not in literals and sym in literals
):
pure_symbols.append(s)
for p in pure_symbols:
assignment[p] = None
for s in pure_symbols:
sym = s + "'"
if s in literals:
assignment[s] = True
elif sym in literals:
assignment[s] = False
return pure_symbols, assignment
def find_unit_clauses(
clauses: list[Clause], model: dict[str, bool | None]
) -> tuple[list[str], dict[str, bool | None]]:
unit_symbols = []
for clause in clauses:
if len(clause) == 1:
unit_symbols.append(list(clause.literals.keys())[0])
else:
Fcount, Ncount = 0, 0
for literal, value in clause.literals.items():
if value is False:
Fcount += 1
elif value is None:
sym = literal
Ncount += 1
if Fcount == len(clause) - 1 and Ncount == 1:
unit_symbols.append(sym)
assignment: dict[str, bool | None] = dict()
for i in unit_symbols:
symbol = i[:2]
assignment[symbol] = len(i) == 2
unit_symbols = [i[:2] for i in unit_symbols]
return unit_symbols, assignment
def dpll_algorithm(
clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]
) -> tuple[bool | None, dict[str, bool | None] | None]:
check_clause_all_true = True
for clause in clauses:
clause_check = clause.evaluate(model)
if clause_check is False:
return False, None
elif clause_check is None:
check_clause_all_true = False
continue
if check_clause_all_true:
return True, model
try:
pure_symbols, assignment = find_pure_symbols(clauses, symbols, model)
except RecursionError:
print("raises a RecursionError and is")
return None, {}
P = None
if len(pure_symbols) > 0:
P, value = pure_symbols[0], assignment[pure_symbols[0]]
if P:
tmp_model = model
tmp_model[P] = value
tmp_symbols = [i for i in symbols]
if P in tmp_symbols:
tmp_symbols.remove(P)
return dpll_algorithm(clauses, tmp_symbols, tmp_model)
unit_symbols, assignment = find_unit_clauses(clauses, model)
P = None
if len(unit_symbols) > 0:
P, value = unit_symbols[0], assignment[unit_symbols[0]]
if P:
tmp_model = model
tmp_model[P] = value
tmp_symbols = [i for i in symbols]
if P in tmp_symbols:
tmp_symbols.remove(P)
return dpll_algorithm(clauses, tmp_symbols, tmp_model)
P = symbols[0]
rest = symbols[1:]
tmp1, tmp2 = model, model
tmp1[P], tmp2[P] = True, False
return dpll_algorithm(clauses, rest, tmp1) or dpll_algorithm(clauses, rest, tmp2)
if __name__ == "__main__":
import doctest
doctest.testmod()
formula = generate_formula()
print(f"The formula {formula} is", end=" ")
clauses, symbols = generate_parameters(formula)
solution, model = dpll_algorithm(clauses, symbols, {})
if solution:
print(f"satisfiable with the assignment {model}.")
else:
print("not satisfiable.")
