Week 1: Implementation of Backtracking logic

Continuing with the implementation of the already discussed function in Week 0. The implementation was done in the PR#29806

Implementation

The implementation of the backtracking function is pretty straight-forward and intutive. The code for it being

def backtrack(self):
    if not self.bound_history:
        raise ValueError("Cannot backtrack, bound_history stack is empty")

    xi, old_bound, upper = self.bound_history.pop()

    if upper:
        xi.upper = old_bound
    else:
        xi.lower = old_bound

    for var in self.all_var:
        var.assign = self.last_assign_snapshot[var]

    self.is_sat = True
    self.result = None

Apart from the function declaration and defination, I had to add two state variables to the LRASolver class, bound_history which is a stack and keeps a track of previous bounds and last_assign_snapshot which is the assignment of the variables in the last valid state.

Testing

A major part of the PR was adding tests to see if the backtracking logic is working correctly. I particularly added 5 tests.

test_example_from_paper()

This particular test is the exact same example as discussed in the 4.6 section of the paper. I have specifically added variable bounds and assignments checks for each state.

Constraints:

$x \le -4$
$x \ge -8$
$-x + y \le 1$
$x + y \ge -3$

test_backtracking_single_variable()

In this particular test, Assert catches the error with the bounds on the variable and there is no need to explicitly call the expensive Check to see if the state is valid or not.

Constraints:

$x \le -4$
$x \ge -8$
$x \ge -2$

test_backtracking_multiple_variables()

This particular test is somewhat similar to the test from the paper just with a set of different constraints.

Constraints:

$2x + 3y \le 12$
$x \ge 3$
$y \ge 3$

test_backtracking_single_variable_multiple_backtracks()

This particular test is made to check if the solver can come back to a particular state after multiple backtracks successfully. In this particular test, similar to test_backtracking_single_variable(), Assert catches the error with the bounds of the variable and Check is not necessary to be called.

Constraints:

$x \le 10$
$x \ge 0$
$x \ge 5$
$x \le 2$

test_backtracking_multiple_variables_multiple_backtracks()

This test is similar to the previous test but with multiple variables. Here, Check should be called to pivot the variables.

Constraints:

$x \le 10$
$x \ge 0$
$y \ge 0$
$x \ge 5$
$y \ge 5$
$x + y \le 4$

Issues faced

EncodedCNF sorts the hashes created for the constraints, which is an issue, as everytime the tests are ran, a new environment is created, so in some instances the tests used to fail while in some it used to pass as I am manually tracing the logic for backtracking.

A fix for this was use the function add_prop so it sequentially adds the constraints thus preserving the order. Another way to reduce this nondeterminism as suggested by Tilo was to testing_mode=True in the LRASolver. By doing these, the tests are consistent for now.

Final Remarks

The PR#29806 has been merged! The next work should be to integrate this backtracking logic with dpll2.py

Another major task in hand is to start with the Phase 1 of the proposal that will be discussed in the next meet. Looking foward to it. :D

Sujal Kumar