# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 1 Introduction  
The Boolean satisfiability problem (SAT problem for short) deals with whether specific Boolean variables can evaluate whether a given Boolean formula is true. The SAT problem is known as the first NP-complete problem [1]. Many practical problems can be reduced to SAT, and there are many applications, such as circuit design [2], neural network verification [3], and mathematical problem solving [4; 5; 6], where SAT can be applied. To solve the Boolean satisfiability problem, we use what is called a SAT solver which is based on general resolution. The state-of-the-art SAT solvers are based on a backtrack search algorithm, called the Davis-Putnum-Logemann-Loveland (DPLL) algorithm [7]. The DPLL has been enhanced by a conflict clause learning mechanism [8], and today the DPLL, combined with clause learning, is called the Conflict-Driven Clause Learning (CDCL) algorithm. Clause learning conducts multiple resolution processes when a conflict occurs in a search and then derives a new learned clause. On the other hand, extended resolution (ER) [9] is different from general resolution. ER introduces new variables (i.e., extended variables) that do not exist in a given formula. [PERSON] proved that the pigeonhole principle can be solved in polynomial steps by using extended resolution [10]. From this point of view, there is a possibility that solvers with ER can outperform the solvers based on CDCL, at least for the pigeonhole principle. However, today's SAT solvers are still based on CDCL that uses general resolution. One of the main reasons is that there is no stable way to choose effective extended variables. Although existing research such as [11; 12] tried to find extended variables that reduce the size of clauses (or resolution steps), there is much room for improvement. In this paper, we try to answer the question: If the SAT solver can add appropriate extended variables as proposed in [10], can the solver enhance its performance by utilizing these variables for the pigeonhole principle? The extended variables introduced in [10] are theoretically the most suitable but their practical application is not clear. As a first step, we confirm thattrying to solve a SAT problem by adding extended variables has almost no effect. Then, we analyze two simple methods to leverage these variables in a search. From experimental results, we show that our method can speed up the overall processing time. In addition, analytical results of the DRUP (Delete Reverse Unit Propagation) proof [13] reveal that our method can utilize extended variables more frequently. We provide practical evidence that extended resolution (variables) can boost the performance of CDCL solvers. Our contributions are as follows:  
* We introduce two ways to add extended variables: full extension introduced by [10] and partial extension by restricting a large part of the variables in [10]. * We show that trying to solve instances of the pigeonhole principle with full and partial extension using basic solvers (MiniSAT [14] and Glucose [15]) has almost no effect. * We analyze two simple methods to utilize extended variables in the search. Experimental results indicate that these methods can improve the performance of the solvers. This fact implies that if extended variables are properly selected and properly utilized, the extended resolution can practically improve the performance of the pigeonhole principle. Note that our aim is neither to tackle difficult (or large) pigeonhole principle instances (e.g., [16]) nor to develop a specific solver better than state-of-the-art solvers for the pigeonhole principle, but to analyze the effect of extended resolution based on [10]. From that perspective, the implementation of our contribution is a proof of concept. However, our proposed methods can be easily applied to state-of-the-art solvers because the methods do not depend on implementation of specific solvers.