Look-Ahead Solver

This task assumes you have implemented a DPLL solver for the second task. Your task is to implement look-ahead algorithm for your solver. You might want to read the chapter on look-ahead solvers from the Handbook of Satisfiability.

Look-Ahead

For the Look-Ahead part implement two nontrivial difference heuristics and compare their behaviour. The ones described in the chapter on look-ahead solvers are

• Clause reduction heuristic (CRH)
• Weighted binaries heuristic (WBH)
• Backbone search heuristic (BSH)

A short note on heuristics

In case of WBH I think that there is a mistake in the description, because it uses \(\gamma_k:=5^{k-3}\). However, in the source code of satz (available at SATLIB - Solvers) it looks like the solver only considers clauses of size at most 3 for the heuristic. Considering the intended meaning of \(\gamma_k\) I believe that the correct definition should be \(\gamma_k:=5^{3-k}\). The same goes for BSH where I believe the correct definition should be \(\gamma_k:=2^{3-k}\).

Additional reasoning

Implement some additional reasoning (such as local learning, autarky reasoning, or double look-ahead resolvents). It is not necessary to implement all of them, pick the ones you consider useful.

Eager data structures

Implement some of the techniques of eager data structures which reduce the cost of unit propagation. Again, it is not necessary to implement all of them, pick the ones you consider useful.

Solver evaluation

To evaluate your solver, use some of the [SATLIB Benchmark Problems]. If you have implemented alternative approaches or heuristics, compare them on the benchmarks as well. Write a report with the results