Code editing task: dpll
Topic: DSA; change kind: corrective

Original code:
from copy import deepcopy
from typing import Optional


class DPLLSolver:
    def __init__(self, cnf):
        """
        initializes the DPLL Solver with a given CNF (Conjunctive Normal Form) input.

        :param cnf: a string representing the CNF, where each clause is on a new line,
                    literals are separated by spaces, negation is denoted by '!', and
                    variables are single characters.
        """
        self.assign_true = set()  # set of literals assigned True
        self.assign_false = set()  # set of literals assigned False
        self.n_props = 0          # count of propositions made
        self.n_splits = 0         # count of splits (decisions) made
        self.cnf = cnf            # the CNF input

    def print_cnf(self):
        """
        prints the CNF in a more readable format, where clauses are enclosed in parentheses
        and literals are separated by '+'.
        """
        s = ''
        for i in self.cnf:
            if len(i) > 0:
                s += '(' + i.replace(' ', '+') + ')'
        print(s)

    def solve(self, cnf, literals):
        """
        recursively solves the CNF using the DPLL algorithm.

        :param cnf: the CNF in its current state (as clauses get simplified).
        :param literals: list of literals that haven't been assigned yet.
        :return: True if the CNF is satisfiable, False otherwise.
        """
        new_true = []  # literals assigned True in this decision level
        new_false = []  # literals assigned False in this decision level
        self.n_splits += 1
        cnf = list(set(cnf))  # remove duplicate clauses
        units = [i for i in cnf if len(i) < 3]  # unit clauses
        units = list(set(units))  # remove duplicate units

        # Unit Propagation
        if len(units):
            for unit in units:
                self.n_props += 1
                if '!' in unit:
                    self.assign_false.add(unit[-1])
                    new_false.append(unit[-1])
                    # simplify the CNF by removing clauses and literals
                    i = 0
                    while True:
                        if unit in cnf[i]:
                            cnf.remove(cnf[i])
                            i -= 1
                        elif unit[-1] in cnf[i]:
                            cnf[i] = cnf[i].replace(unit[-1], '').strip()
                        i += 1
                        if i >= len(cnf):
                            break
                else:
                    self.assign_true.add(unit)
                    new_true.append(unit)
                    i = 0
                    while True:
                        if '!'+unit in cnf[i]:
                            cnf[i] = cnf[i].replace('!'+unit, '').strip()
                        elif unit in cnf[i]:
                            cnf.remove(cnf[i])
                            i -= 1
                        i += 1
                        if i >= len(cnf):
                            break

        # check if CNF is solved
        if len(cnf) == 0:
            return True

        # splitting (choose a literal and try both True and False)
        literals = [k for k in list(set(''.join(cnf))) if k.isalpha()]
        x = literals[0]
        if self.solve(deepcopy(cnf) + [x], deepcopy(literals)):
            return True
        elif self.solve(deepcopy(cnf) + ['!' + x], deepcopy(literals)):
            return True
        else:
            # undo assignments made in this decision level
            for i in new_false:
                self.assign_false.remove(i)
            return False

    def dpll(self) -> Optional[dict]:
        """
        public method to solve the CNF using the DPLL algorithm.

        :return: a dictionary mapping each literal to its boolean value if the CNF is satisfiable,
                 or None if the CNF is unsatisfiable.
        """
        literals = [i for i in list(set(self.cnf)) if i.isalpha()]
        cnf = self.cnf.splitlines()
        res = {}
        if self.solve(cnf, literals):
            # assign values to literals based on the assignments made during solving
            for i in self.assign_true:
                res[i] = True
            for i in self.assign_false:
                res[i] = False

            return res
        else:
            return None  # unsat!

Instruction (descriptive):
Correct the logic of the solver, it is currently not backtracking on empty clauses, which are unsatisfiable. If found, the solver should undo assignments made in the current decision level.

Instruction (lazy):
Fix the solver, it does not backtrack on empty clauses.

Edited code:
from copy import deepcopy
from typing import Optional


class DPLLSolver:
    def __init__(self, cnf):
        """
        initializes the DPLL Solver with a given CNF (Conjunctive Normal Form) input.

        :param cnf: a string representing the CNF, where each clause is on a new line,
                    literals are separated by spaces, negation is denoted by '!', and
                    variables are single characters.
        """
        self.assign_true = set()  # set of literals assigned True
        self.assign_false = set()  # set of literals assigned False
        self.n_props = 0          # count of propositions made
        self.n_splits = 0         # count of splits (decisions) made
        self.cnf = cnf            # the CNF input

    def print_cnf(self):
        """
        prints the CNF in a more readable format, where clauses are enclosed in parentheses
        and literals are separated by '+'.
        """
        s = ''
        for i in self.cnf:
            if len(i) > 0:
                s += '(' + i.replace(' ', '+') + ')'
        print(s)

    def solve(self, cnf, literals):
        """
        recursively solves the CNF using the DPLL algorithm.

        :param cnf: the CNF in its current state (as clauses get simplified).
        :param literals: list of literals that haven't been assigned yet.
        :return: True if the CNF is satisfiable, False otherwise.
        """
        new_true = []  # literals assigned True in this decision level
        new_false = []  # literals assigned False in this decision level
        self.n_splits += 1
        cnf = list(set(cnf))  # remove duplicate clauses
        units = [i for i in cnf if len(i) < 3]  # unit clauses
        units = list(set(units))  # remove duplicate units

        # Unit Propagation
        if len(units):
            for unit in units:
                self.n_props += 1
                if '!' in unit:
                    self.assign_false.add(unit[-1])
                    new_false.append(unit[-1])
                    # simplify the CNF by removing clauses and literals
                    i = 0
                    while True:
                        if unit in cnf[i]:
                            cnf.remove(cnf[i])
                            i -= 1
                        elif unit[-1] in cnf[i]:
                            cnf[i] = cnf[i].replace(unit[-1], '').strip()
                        i += 1
                        if i >= len(cnf):
                            break
                else:
                    self.assign_true.add(unit)
                    new_true.append(unit)
                    i = 0
                    while True:
                        if '!'+unit in cnf[i]:
                            cnf[i] = cnf[i].replace('!'+unit, '').strip()
                        elif unit in cnf[i]:
                            cnf.remove(cnf[i])
                            i -= 1
                        i += 1
                        if i >= len(cnf):
                            break

        # check if CNF is solved
        if len(cnf) == 0:
            return True

        # check for an empty clause (unsatisfiable)
        if sum(len(clause) == 0 for clause in cnf):
            # Undo assignments made in this decision level
            for i in new_true:
                self.assign_true.remove(i)
            for i in new_false:
                self.assign_false.remove(i)
            return False

        # splitting (choose a literal and try both True and False)
        literals = [k for k in list(set(''.join(cnf))) if k.isalpha()]
        x = literals[0]
        if self.solve(deepcopy(cnf) + [x], deepcopy(literals)):
            return True
        elif self.solve(deepcopy(cnf) + ['!' + x], deepcopy(literals)):
            return True
        else:
            # undo assignments made in this decision level
            for i in new_false:
                self.assign_false.remove(i)
            return False

    def dpll(self) -> Optional[dict]:
        """
        public method to solve the CNF using the DPLL algorithm.

        :return: a dictionary mapping each literal to its boolean value if the CNF is satisfiable,
                 or None if the CNF is unsatisfiable.
        """
        literals = [i for i in list(set(self.cnf)) if i.isalpha()]
        cnf = self.cnf.splitlines()
        res = {}
        if self.solve(cnf, literals):
            # assign values to literals based on the assignments made during solving
            for i in self.assign_true:
                res[i] = True
            for i in self.assign_false:
                res[i] = False

            return res
        else:
            return None  # unsat!

Tests:
### START TESTS ###
if True:  # pragma: no cover
    input1 = 'A\n!A'
    assert DPLLSolver(input1).dpll() is None

    input2 = 'A'
    assert DPLLSolver(input2).dpll() == {'A': True}

    false_input = '!A'
    assert DPLLSolver(false_input).dpll() == {'A': False}

    false_double_input = '!A\nA'
    assert DPLLSolver(false_double_input).dpll() is None

    false_ab_input = '!A\n!B'
    assert DPLLSolver(false_ab_input).dpll() == {'A': False, 'B': False}

    empty_input = ''
    assert DPLLSolver(empty_input).dpll() == {}

    input3 = 'A\nB\n!A\n!B'
    assert DPLLSolver(input3).dpll() is None

    input4 = 'A\nB C\n!A !B\n!B !C'
    assert DPLLSolver(input4).dpll() == {'A': True, 'C': True, 'B': False}

    input5 = 'A B C\n!A !B\n!B !C\n!C !A'
    # in this case, only one literal can be True; all others must be False
    assert list(DPLLSolver(input5).dpll().values()).count(True) == 1

    solver = DPLLSolver('A B C')
    assert solver.assign_true == set()
    assert solver.assign_false == set()
    assert solver.n_props == 0
    assert solver.n_splits == 0
    assert solver.cnf == 'A B C'

    solver = DPLLSolver('A')
    assert solver.solve(['A'], ['A']) == True
    assert 'A' in solver.assign_true

    solver = DPLLSolver('A\n!A')
    assert solver.solve(['A', '!A'], ['A']) == False

    solver = DPLLSolver('A B')
    assert solver.solve(['A', 'B'], ['A', 'B']) == True
    assert 'A' in solver.assign_true and 'B' in solver.assign_true
    assert solver.n_props > 0
    assert solver.n_splits > 0

    assert DPLLSolver('A\n!A').dpll() is None
    assert DPLLSolver('A').dpll() == {'A': True}
    assert DPLLSolver('').dpll() == {}
    assert DPLLSolver('A\nB\n!A\n!B').dpll() is None
    assert DPLLSolver('A B\n!A !B\n!B !A').dpll() != None

    # mock the print function

    old_print = print
    def print(x): return x

    # run print_cnf method
    DPLLSolver('A B\n!A !B\n!B !A').print_cnf()

    # restore the print function
    print = old_print

    assert DPLLSolver('A B C\n!A D E\n!B !D\n!C E').dpll(
    ) is not None  # should be satisfiable

    backtrack_input1 = 'A B\n!A C\n!B !C\nC'
    solver = DPLLSolver(backtrack_input1)
    assert solver.dpll() is not None  # should be satisfiable after backtracking
    # one of them should be backtracked
    assert 'A' in solver.assign_false or 'B' in solver.assign_false

    cnf1 = 'A\n!A B\n!B'
    solver1 = DPLLSolver(cnf1)
    assert solver1.dpll() is None
    assert solver1.assign_true == set(), "No assignments should remain after backtracking."
    assert solver1.assign_false == set(), "No assignments should remain after backtracking."

    cnf2 = 'A B\n!A C\n!B\n!C'
    solver2 = DPLLSolver(cnf2)
    assert solver2.dpll() is None
    assert solver2.assign_true == set(), "No assignments should remain after backtracking."
    assert solver2.assign_false == set(), "No assignments should remain after backtracking."

    cnf3 = 'A B\n!A C\n!B\n!C'
    solver3 = DPLLSolver(cnf3)
    assert solver3.dpll() is None
    assert solver3.assign_true == set(
    ), "No assignments should remain after backtracking."
    assert solver3.assign_false == set(
    ), "No assignments should remain after backtracking."

    solver = DPLLSolver('A\n!A B\n!B')
    assert not solver.solve(['A', '!A B', '!B'], [
                            'A', 'B'])
    assert 'A' not in solver.assign_true
    assert 'B' not in solver.assign_true

    solver = DPLLSolver('A B\n!A C\n!C\n!B')
    assert not solver.solve(['A B', '!A C', '!C', '!B'], [
                            'A', 'B', 'C'])
    assert 'A' not in solver.assign_true
    assert 'B' not in solver.assign_true
    assert 'C' not in solver.assign_true

    solver = DPLLSolver('A B\n!A C\n!C D\n!B D\n!D')
    assert not solver.solve(['A B', '!A C', '!C D', '!B D', '!D'], [
                            'A', 'B', 'C', 'D'])
    assert 'A' not in solver.assign_true
    assert 'B' not in solver.assign_true
    assert 'C' not in solver.assign_true
    assert 'D' not in solver.assign_true