# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 2 Preliminaries
### SAT Solver  
Solvers for SAT problem are called SAT solvers. The mainstream algorithm for practical instances (no random generation) is a backtracking search, which is called the Davis-Putnam-Logemann-Loveland (DPLL) algorithm [7]. The DPLL has been enhanced by adding a conflict clause learning mechanism [8], and today the DPLL combined with the clause learning is called the Conflict-Driven Clause Learning (CDCL) algorithm. Algorithm 1 shows the pseudo code of the CDCL. The details are in [14]. In the algorithm, unit propagation Line 9) conducts forcing assignments to variables in unit clauses in which only one remaining literal is unassigned, and the others are false. After propagation, there can be a conflicting clause. A clause is in conflict when all of its literals are false. The clause learning (Line 11) conducts multiple resolution processeswhen a conflict in the search occurs (Line 10). Suppose there are two clauses, \((x\lor A)\) and \((\
eg x\lor B)\), where \(A\) and \(B\) are sub-clauses. Resolution on the variable \(x\) is defined as follows:  
\[\frac{(x\lor A),(\
eg x\lor B)}{(A\lor B)}\]  
This is the reason why the CDCL solvers are based on the resolution. The most popular learning scheme (i.e., what kind of clauses should be selected for resolution) is first-UIP [17]. ```
0: a CNF formula \(\mathbb{T}\)
0: SATISFIABLE or UNSATISFIABLE
1: level = 0 // decision level (depth of search tree)
2: learnts = \(\emptyset\) // learnt clauses
3: inc_score = 1.0 // incremental value for VSIDS scores
4: conf // conflicting clause
5: learnt // learnt clause
6: blevel // level to backtrack
7: next // next decision variable
8:while true do
9: conf = unitPropagation(\(\mathbb{T}\))
10: if conf \(\
eq\) NULL then
11: learnt = conflictAnalysis(\(\mathbb{T}\), conf)
12: blevel = calcBackjumpLevel(learnt)
13:if blevel \(<\) 0 then
14: return UNSATISFIABLE
15: end if
16:for each var in learnt do
17: increaseVSIDSScores(var, inc_score)
18:endfor
19: inc_score = inc_score / 0.95
20: learnts = learnts \(\cup\) learnt
21:if restart() then
22: blevel = 0
23:endif
24: backjump(blevel)
25: level = blevel
26: else
27: next = chooseDecisionVariable(\(\mathbb{T}\))
28:if next == NULL then
29: return SATISFIABLE
30:endif
31: assignValue(next)
32: level = level + 1
33:endif
34:endwhile
```  
**Algorithm 1** Pseudo code of CDCL. After learning a learnt clause, backjump (Line 24) [18] undoes the variable assignment to a certain level (depth of search tree) where the newly learnt clause becomes a unit. The level to backjump is calculated at Line 12 (\"calcBackjumpLevel\" function) from the learnt clause. If the learnt clause cannot be a unit, then the given formula is unsatisfiable (Lines 13 and 14). While general backtracking just cancels the assignment of the last variable, backjumping directly goes back to the culprit variable that causes the conflict (and is included in the learnt clause). Restart (Line 21) [19] cancels all the variable assignments. SAT solvers are often stuck in a desert search space where no solution exists and no useful information (i.e., useful learnt clause) can be extracted. Restart is effective to escape such a search area. There are two types for determining when to restart: statically [20] and dynamically [21]. If there is no conflict after the unit propagation, decision process chooses a variable, called decision variable, to be assigned (Line 27). The most popular decision heuristic is the Variable State Independent Decaying Sum (VSIDS) [17]. The VSIDS attaches a score for each variable and chooses the highest scored variable at decision. The scores are increased when the corresponding variable is included in a learnt clause (Lines 16 and 17). The incremental value for the VSIDS score grows exponentially (Line 19) to prioritize variables recently assigned and to neglect past scores. In recent solvers, machine-learning-based scores such as Learning Rate Branching (LRB) [22] are used together. There are also other decision techniques that combine multiple methods [23; 24].