Addition of AI algorithms

[payallenka]

Feature description

I would like to add a few AI algorithms like DPLL, TT-ENTAILS, WALKSAT, UNIFY, FOL-BC-ASK algorithms. To your repository as I beleive it will be a good contribution.

[amirkhantemirov]

i am planning to contribute to this issue by implemmenting the DPLL algoritm in Python. Here's the code that solves this problem. Let me know if this aligns with your expetations.

def dpll(clauses, assignment):
    if all(is_satisfied(clause, assignment) for clause in clauses):
        return True, assignment
    if any(is_unsatisfied(clause, assignment) for clause in clauses):
        return False, None

    unassigned_vars = {var for clause in clauses for var in clause if var not in assignment}
    chosen_var = next(iter(unassigned_vars))

    assignment[chosen_var] = True
    result, final_assignment = dpll(clauses, assignment)
    if result:
        return True, final_assignment
    assignment[chosen_var] = False
    result, final_assignment = dpll(clauses, assignment)
    if result:
        return True, final_assignment

    del assignment[chosen_var]
    return False, None

def is_satisfied(clause, assignment):
    return any(literal in assignment and assignment[literal] for literal in clause)
def is_unsatisfied(clause, assignment):
    return all(literal in assignment and not assignment[literal] for literal in clause)

if __name__ == "__main__":

    clauses = [
        {"A", "-B"},
        {"-A", "B"},
        {"A", "B"}
    ]
    assignment = {}
    satisfiable, final_assignment = dpll(clauses, assignment)

    if satisfiable:
        print("SATISFIABLE")
        print("Assignment:", final_assignment)
    else:
        print("UNSATISFIABLE")