# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 3 Related Work  
There are various works related to extended resolution for SAT solvers.  
[PERSON] [9] first introduced the extension rule adding a new variable to the original formula and retaining its satisfiability-equivalency. [PERSON] [10] used this extension rule, i.e., as extended resolution, and established the polynomial-step solution of the pigeonhole principle. Although [PERSON]'s original extension was the form \(x\leftrightarrow(\
eg a\vee\
eg b)\), more general extensions (including [10]) are commonly used [30]. [PERSON] [31] generalized extended resolution as an addition of blocked clauses and proved it can speed up resolution proofs (later, in reverse, blocked clause elimination [32] was shown to be helpful for SAT solvers). DRAT (Deletion Resolution Asymmetric Tautology) [33], used as the standard proof format (known as the successor of DRUP) for unsatisfiable instances, has also been proven to generalize extended resolution [34; 35].  
[PERSON] [11] proposed extended clause learning (ECL). It conducts an extended resolution when a conflict occurs. When a clause \(\gamma=\alpha\vee\beta\) such that \(|\alpha|\geq 2\) and \(|\beta|\geq 1\) is learnt by a standard learning scheme (e.g., 1-UIP), the ECL learns clauses \((x\vee\beta)\) and \((x\leftrightarrow\alpha)\) instead of \(\gamma\) where \(x\) is a fresh variable. The ECL only applies the extension when \(|\gamma|>30\) and conducts a restart after the extension. The author implemented the ECL on Tinisat [36] and confirmed that TinisAT with ECL could solve more instances for specific problems. [PERSON] et al. [12] proposed a local extension. When two consecutive learnt clauses \(C_{i}=(\
eg l_{1}\lor D)\) and \(C_{i+1}=(\
eg l_{2}\lor D)\) are derived, a new variable \(v\leftrightarrow(l_{1}\lor l_{2})\) is introduced. The clauses \(C_{i}\) and \(C_{i+1}\) can be replaced with \(C^{\prime}=(\
eg v\lor D)\); thus, the number of learnt clauses can be reduced. Moreover, all clauses, including \(l_{1}\) and \(l_{2}\), can be replaced by using the variable \(v\) (a clause \((l_{1}\lor l_{2}\lor A)\) is equivalent to \((v\lor A)\)). They implemented the proposed method on MiniSAT 2.2 and (the first version of) Glucose and confirmed performance improvements on instances of SAT Competition 2007 and 2009. [PERSON] [37] improved the work by using a Bloom filter and reducing some overheads. [PERSON] et al. [38] proposed a way to detect auxiliary variables by exploiting the hidden Boolean functions used for the problem encoding. The method tries to detect a new variable \(y=(x_{1}\vee\ldots\lor x_{n})\) or \(y=(x_{1}\wedge\ldots\wedge x_{n})\) (equivalent to \(\
eg y=(\
eg x_{1}\vee\ldots\vee\
eg x_{n})\)) during the search and then substitutes the variable \(y\) for clauses including \((x_{1}\vee\ldots\lor x_{n})\). They implemented the method to MiniSAT 2.2 and attained a performance gain on specific problem instances. [PERSON] proposed blocked variable addition (BVA) [39] as a preprocessing technique. BVA introduces a new variable that reduces the number of clauses in a given CNF instance, in reverse manner of general resolution. Although we tried BVA implemented in a coprocessor [40] on PHP instances as a preliminary experiment, BVA did not reproduce the extended variables introduced by [PERSON] [10]. [PERSON] et al. [16] tackled the PHP as a MAXSAT problem by transforming the original SAT problem. In fact, they solved larger instances than the ones we try. Our focus is not to challenge solving difficult (or large) instances but to analyze the practical effect of extended resolution in a (theoretically) ideal condition.  
As a representative instance that extended resolution was proved to be powerful in theory, we show the practical usefulness of extended resolution on the PHP in this paper.