CDCL Algorithm [10 points]

Add clause learning and restarts to your DPLL solver.

Clause learning

When learning a clause, you can use several approaches

• learning multiple clauses from several cuts
• stop at the first UIP
• stop when the literal at current decision level has no antecedent

I recommend to stop at the first UIP, but you can compare this approach with the other ones to see which one is the most effective.

You can also use a heruistic minimization of the learned clause, e.g. by using subsuming resolution.

Clause deletion

Add a heuristic for regularly deleting some of the learned clauses. There is a bunch of possibilities how you can do that and these can be combined.

• Remove subsumed clauses (i.e. if clause \(C\) is learned and \(D\supset C\) is already in the cache, \(D\) can be removed).
• Keep short clauses (up to a limit which may increase over time)
• Use LBD
• Keep active clauses where activity can be measured in some way based on the number of unit propagations using the clause.

There are also several possibilities on how to determine when the clauses should be deleted, for instance

• At the time of restart
• When the current cache is full — the size of cache has to increase over time (e.g. during restart)
• After a specific number of conflicts

Restarts

Add periodic restarts to your solver, you can use either geometric or Luby sequences to determine when the search should be restarted.

Solver evaluation

To evaluate your solver, use some of the SATLIB Benchmark Problems. By now the algorithm you have implemented has a lot of parameters and possible choices. Your solver should be easily configurable to use a particular set of parameters and heuristics, try to check how the choice of parameters affects the solver performance. What parameters are best for your solver? Write a report summarizing the evaluation of your solver.