# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## Appendix A Code of Our Proposed Methods  
In this section, we show the actual code of our proposed methods, \"m1\" and \"m2\". Note that the code of Glucose is based on MiniSAT, thus the codes can work in both solvers. We show the source code of the \"m1\" method in Listings A1 and A2. Listing A1 is embedded in Solver.h file of MiniSAT/Glucose, and Listing A2 is embedded in Solver.cc file (head and tail parts are the same as the original code and omitted). By extremely increasing the VSIDS scores of extended variables, the solver always selects them as decision variables prior to non-extended variables. \begin{table}
\begin{tabular}{c c c c c c c c c c c c c} \hline \hline  & & & & & \multicolumn{3}{c}{**G**} & \multicolumn{3}{c}{**G+m1**} & \multicolumn{3}{c}{**G+m2**} \\ \cline{4-13}
**Instance** & **n** & **\#V** & **\#C** & **ECR** & **top-10** & **top-100** & **\(p\)-Value** & **top-10** & **top-100** & **\(p\)-Value** & **top-10** & **top-100** & **\(p\)-Value** \\ \hline no shuffle & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & 0.01 & \(1.29\times 10^{-1}\) & 0.10 & 0.27 & \(2.74\times 10^{-11}\) \\ shuffle1 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.02 & \(9.26\times 10^{-2}\) & 0.00 & 0.03 & \(8.60\times 10^{-1}\) \\ shuffle2 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(9.98\times 10^{-1}\) & 0.10 & 0.02 & \(7.78\times 10^{-1}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) \\ shuffle3 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(6.82\times 10^{-1}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) \\ \hline no shuffle & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(3.73\times 10^{-1}\) & 0.10 & 0.01 & \(7.14\times 10^{-3}\) & 0.00 & 0.00 & \(9.98\times 10^{-1}\) \\ shuffle1 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(9.52\times 10^{-1}\) & 0.00 & 0.00 & \(9.98\times 10^{-1}\) \\ shuffle2 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & 0.02 & \(4.89\times 10^{-1}\) & 0.00 & 0.02 & \(4.69\times 10^{-1}\) \\ shuffle3 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(3.23\times 10^{-1}\) & 0.10 & 0.04 & \(4.29\times 10^{-2}\) \\ \hline no shuffle & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & 0.10 & 0.02 & \(1.00\times 10^{0}\) & no-data & no-data & no-data & no-data \\ shuffle1 & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ shuffle2 & 13 & 167 & 993 & 0.04 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & \(0.01\) & \(1.38\times 10^{-1}\) & no-data & no-data & no-data \\ shuffle3 & 13 & 167 & 993 & 0.04 & 0.00 & 0.00 & \(9.94\times 10^{-1}\) & no-data & no-data & no-data & no-data & no-data & no-data \\ \hline \hline \end{tabular}
\end{table} 
Table 7: DRUP analysis results of PHP instances with partial extension for Glucose. ```
``` intnum_org_vars;//calculatedfromthenumberofpigeonsdoublevar_inc=1e100;//incrementalscoreforextendedvariables voidbumpExtendedVars( constintnum_org_vars,constintcurr_restarts){ if(curr_restarts!=0)return; constintnv=nVars(); for(inti=num_org_vars;i<nv;i++){ varBumpActivity(i,evar_inc); } } }
```

```
intinvoidSolver::varBumpActivity(Varv,doubleinc){ if(v<num_org_vars) activity[v]+=inc; else activity[v]+=inc*evar_inc; if((v<num_org_vars&&activity[v]>1e100)|| (v>=num_org_vars&&activity[v]>1e200)){ //Rescale: for(inti=0;i<nVars();i++) activity[i]=1e-100; var_inc*=1e-100; } //Updaterorder_heapwithrespecttonewactivity: if(order_heap.inHeap(v)) order_heap.decrease(v); }
```

Listing 12: Code of m1 method implemented in Solver.cc. ```
lboolSolver::solve_(){... intcurr_restarts=0; bumpExtendedVars(num_org_vars,curr_restarts); while(status==1_Undef){ doublerest_base=luby_restart?luby(restart_inc,curr_restarts):
```

```
status=search(rest_base*restart_first);... }
```

Listing 13: Code of m2 method implemented in Solver.h. We show the source code of the \"m2\" method in Listings 14 and 15.