usrbinenv python3 davisputnamlogemannloveland dpll algorithm is a complete backtrackingbased search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form i e for solving the conjunctive normal form satisfiability cnfsat problem for more information about the algorithm https en wikipedia orgwikidpllalgorithm 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 clausea1 a2 a3 clause evaluatea1 true true represent the literals and an assignment in a clause assign all literals to none initially to print a clause as in conjunctive normal form strclausea1 a2 a3 a1 a2 a3 to print a clause as in conjunctive normal form lenclause 0 lenclausea1 a2 a3 3 assign values to literals of the clause as given by model complement assignment if literal is in complemented form 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 noneunable to complete evaluation if a literal has no assignment 4 compute disjunction of all values assigned in 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 represent the number of clauses and the clauses themselves to print a formula as in conjunctive normal form strformulaclausea1 a2 a3 clausea5 a2 a1 a1 a2 a3 a5 a2 a1 randomly generate a clause all literals have the name ax where x is an integer from 1 to 5 randomly generate a formula 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 formulaclausea1 a2 a3 clausea5 a2 a1 clauses symbols generateparametersformula clauseslist stri for i in clauses clauseslist a1 a2 a3 a5 a2 a1 symbols a1 a2 a3 a5 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 formulaclausea1 a2 a3 clausea5 a2 a1 clauses symbols generateparametersformula puresymbols values findpuresymbolsclauses symbols puresymbols a1 a2 a3 a5 values a1 true a2 false a3 true a5 false 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 clausea4 a3 a5 a1 a3 clause2 clausea4 clause3 clausea3 clauses symbols generateparametersformulaclause1 clause2 clause3 unitclauses values findunitclausesclauses unitclauses a4 a3 values a4 true a3 true 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 formulaclausea4 a3 a5 a1 a3 clausea4 clauses symbols generateparametersformula soln model dpllalgorithmclauses symbols soln true model a4 true usr bin env python3 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 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 represent the literals and an assignment in a clause assign all literals to none initially to print a clause as in conjunctive normal form str clause a1 a2 a3 a1 a2 a3 to print a clause as in conjunctive normal form len clause 0 len clause a1 a2 a3 3 assign values to literals of the clause as given by model complement assignment if literal is in complemented form 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 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 represent the number of clauses and the clauses themselves 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 randomly generate a clause all literals have the name ax where x is an integer from 1 to 5 randomly generate a formula 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 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 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 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
from __future__ import annotations

import random
from collections.abc import Iterable


class Clause:
    

    def __init__(self, literals: list[str]) -> None:
        
        
        self.literals: dict[str, bool | None] = {literal: None for literal in literals}

    def __str__(self) -> str:
        
        return "{" + " , ".join(self.literals) + "}"

    def __len__(self) -> int:
        
        return len(self.literals)

    def assign(self, model: dict[str, bool | None]) -> None:
        
        for literal in self.literals:
            symbol = literal[:2]
            if symbol in model:
                value = model[symbol]
            else:
                continue
            if value is not None:
                
                if literal.endswith("'"):
                    value = not value
            self.literals[literal] = value

    def evaluate(self, model: dict[str, bool | None]) -> bool | None:
        
        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:
    

    def __init__(self, clauses: Iterable[Clause]) -> None:
        
        self.clauses = list(clauses)

    def __str__(self) -> str:
        
        return "{" + " , ".join(str(clause) for clause in self.clauses) + "}"


def generate_clause() -> Clause:
    
    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:
    
    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] = {}
    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(next(iter(clause.literals.keys())))
        else:
            f_count, n_count = 0, 0
            for literal, value in clause.literals.items():
                if value is False:
                    f_count += 1
                elif value is None:
                    sym = literal
                    n_count += 1
            if f_count == len(clause) - 1 and n_count == 1:
                unit_symbols.append(sym)
    assignment: dict[str, bool | None] = {}
    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 = list(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 = list(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.")