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.")
