Basics of Conflict-Driven Clause Learning

The fundamental CDCL algorithm is shown in the image below. This image is taken from Kroening and Strichman's book Decision Procedures, an algorithmic point of view.

Translating this into C++ may look like the following:

int cdcl()
{
  while (true) {
    while (bcp() == CONFLICT) {
      bt_level = analyse_conflict();
      if (bt_level < 0)
	return UNSATISFIABLE;
      backtrack(bt_level);
    }
    if (!decide())
      return SATISFIABLE;
}

This leaves us with various concerns:

• How do we get the CNF formula into cdcl()?
• What is bcp()?
• What does it mean to analyse a conflict?
• What does decide() do?

Here are some partial answers:

• I'll write a separate article on parsing DIMACS files and adding clauses to a solver object.
• bcp() is 'boolean constraint propagation', also known as unit propagation, which assigns values based on the existence of clauses containing a single literal.
• Analysing a conflict is the process of computing the backtracking level, detecting global unsatisfiability and adding new constraints.
• decide() assigns a truth value to an unassigned variable.

Return to the homepage.