SAT-SOLVING-EXAMPREP/Implementation Details.md

• See Solvers#Boolean Constraint Propagation (BCP)

Occurrence Stack/ List

• Array/Map from literals to clause pointers
• Keep track of all Clauses which contain lit

Specifically for 2 watch

• can also be a linked list of clauses (pointer chasing)

Trick for binary clauses

• Store the other literal instead of a pointer to the clause

Clause Counting

• Keep track of assigned (false) literals in a clause
• If there is only one unassigned literal left (and there is no unassigned literal)
• That literal needs to be assigned
• Needs to be adjusted during (decision,) propagation and backtracking

Head & Tail scheme (SATO, Zhang'97)

• Each clause has head & tail
• before head & after tail all literals are falsified
• if head >= tail => conflict

(Two) Watch scheme

• Watch first two instead of all literals in a clause
  • I.e. Do not keep full occurrence list
  • You could also watch whatever two literals using a watcher structure
• If a watched literal is assigned to false, replace it if possible
• If not possible => Assign other True

Blocking Literal

• Add an additional entry in the watch list, which carries a literal that was recently \top in the clause
• If it is still \top no derefering the pointer is needed (cache friendly)

Control and Trail

• Keep track of assigned variables in order on the trail
• Keep track of size of trail after each decision (trail is decided var + propagated) !

Finding an UIP

• You can traverse the implication graph in reverse order of trail to find the first UIP

  for (auto it = trail.rbegin(); it < trail.rend(); ++it) {
    // Walk backwards in trail
    // Mark clauses to visit
    auto var = abs(*it);
    if (!marked[var]) continue;
    // Found UIP
    if (lowest_level == 1) {
      uip = *it;
      break;
    }
    marked[var] = false;
    lowest_level--;
    for (auto other : *implication[var]) {
      if (var == other)
        continue;
      if (var == -other)
        continue;
      if (marked[abs (other)])
         continue;
      if (levels[abs (other)] == level) {
        debug ("new literal on highest level %s", debug (other));
        lowest_level++;
      }
      marked[abs(other)] = true;
    }
  }

  for (auto it = trail.rbegin(); it != trail.rend(); ++it) {
    if (marked[abs(*it)]) {
      marked[abs(*it)] = false;
      learned_clause.push_back(-*it); 
    }
  }