# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 5 Experimental Results
### Performance Comparison  
Table 1 exhibits the results of vanilla (no extension) PHP instances. The second to sixth columns (n, #V, #C, #EV, and #EC) indicate the number of pigeons, variables (including extended variables), clauses (including extended clauses), extended variables, and clauses including extended variables, respectively. The seventh and later columns stand for the results of each solver. The \"M\" and \"G\" indicate MiniSAT 2.2 and Glucose 3, respectively. A solver with one of our methods is expressed as \"M/G +m1/m2\". The values for each solver indicate the processing time in seconds, and the best one is bolded. Instances with more pigeons are difficult to solve from the point of view of processing time. Specifically, instances with more than 13 pigeons could not be solved by any solvers. Since Glucose is the enhanced solver based on MiniSAT, it could solve instances with 13 pigeons. Note that due to the lack of extended variables, our two methods have essentially no effect for these instances.  
Table 2 exhibits the results of the PHP instances with full extension. Glucose with \"m1\" and Glucose with \"m2\" exhibited good performance, especially for large instances. Only these solvers could solve the instances with 14 pigeons. The two methods could consistently improve the performance for instances with more than 11 pigeons. On the other hand, the effect of \"m2\" is moderate on MiniSAT. Even though it could shorten the processing time for all the instances with 11 pigeons, this is not the case for 12 pigeons. One of the possible reasons is that MiniSAT conducts less restarts than Glucose. While MiniSAT version 2.2 implements Luby restart [20] based on a static policy, Glucose version 3 executes a dynamic restart policy [21] which invokes restarting more frequently in practice. Thus, the method \"m2\" can be called more in Glucose than MiniSAT, which enhances the performance of Glucose. In contrast, the method \"m1\" also worked on MiniSAT. These results reveal that we can boost the performance of a SAT solver that implements methods to leverage extended variables aggressively for \"fully\" extended instances.  
Table 3 exhibits the results of the PHP instances with partial extension. For this kind of instance, the two methods had good effects on MiniSAT but little impact on Glucose. MiniSAT with the methods stably outperformed the original MiniSAT for instances with 11 and 12 pigeons. On the other hand, Glucose with \"m2\" methods could not solve two instances with 13 pigeons that the original Glucose could solve. As mentioned in Section 4.1, partial extension can be useful for pruning the search space. However, in comparison with the results of full extension, partially extending variables cannot always help the solvers.  
In these experiments, we can use already extended instances under the ideal extension. However, we have no idea how to add extended variables for various types of problems in practice. The results obtained from our experiments indicate that if we only derive partial extension during (or before) the search, the performance gain cannot be so significant. We  
\begin{table}
\begin{tabular}{c c c c c c c c c c c c} \hline \hline
**Instance** & **n** & **\#V** & **\#C** & **\#EV** & **\#EC** & **M** & **M+m1** & **M+m2** & **G** & **G+m1** & **G+m2** \\ \hline no shuffle & 11 & 110 & 561 & 0 & 0 & 100.39 & 100.41 & **95.85** & 122.81 & 121.48 & 122.72 \\ shuffle1 & 11 & 110 & 561 & 0 & 0 & 105.26 & 104.96 & **100.27** & 119.39 & 117.89 & 119.26 \\ shuffle2 & 11 & 110 & 561 & 0 & 0 & 46.23 & 46.24 & **43.96  
can have full benefits of extended resolution if we can fully (completely) conduct extension, which is not easy in practice.