71 lines
2.4 KiB
Markdown
71 lines
2.4 KiB
Markdown
- 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)
|
|
![[control_trail.png]]
|
|
|
|
## 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);
|
|
}
|
|
}
|
|
|
|
``` |