The goal of this project is to implement, study and experiment with different backtracking heuristics in the winner of the latest SAT evaluation contest (SAT Race 2019). We will try to find a backtracking heuristic, which would improve the performance of the already very efficient solver. It should be noticed that we won’t need to implement any new backtracking algorithm (as the complexity of such an implementation would go beyond the scope of the project), but only implement heuristics in an existing algorithm.
Backtrack-search SAT solving has been extremely useful for over two decades as it enabled solving real-world instances of intractable problems across many domains.
Backtracking is an essential component of modern SAT solvers. After the solver completes exploring a branch in the decision tree, it has to choose the backtrack level (that is, the decision level it will backtrack to), carry out the backtracking and then resume the search in another branch.
Since the original SAT solvers, developed in the 90th, and until very recently, the backtrack level had been found deterministically by applying the so-called Non-Chronological Backtracking (NCB) algorithm. However, last year it was shown that relaxing the NCB algorithm and letting the solver to choose the backtrack level is not only algorithmically possible, but also advantageous [1]. The SAT solver, presented in [1], won the SAT Competition 2018.
This recent development opened up new possibilities for improving the SAT solver’s performance by tuning its backtracking heuristic. For example, a new backtracking heuristic, different from [1], was already shown to be useful in [2].
The goal of this project is to implement, study and experiment with different backtracking heuristics in the winner of the latest SAT evaluation contest (SAT Race 2019). We will try to find a backtracking heuristic, which would improve the performance of the already very efficient solver. It should be noticed that we won’t need to implement any new backtracking algorithm (as the complexity of such an implementation would go beyond the scope of the project), but only implement heuristics in an existing algorithm.
[1] Alexander Nadel and Vadim Ryvchin, “Chronological Backtracking”. SAT 2018.
[2] Sibylle Möhle and Armin Biere, “Backing Backtracking”. SAT 2019.
Supervisor : Alexander Nadel – Intel