# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 4 Analysis Procedure
### _UNSAT Core Analysis_  
In addition to processing time, we also analyze the DRUP proof for each instance. The DRUP proof is a record of how the empty clause (causing the unsatisfiability of the instance) is derived: which clause is used for resolution to generate a new learnt clause. By analyzing this core, we can count the frequency of each clause that contributes to prove the unsatisfiability. For example, assume that there is an unsatisfiable CNF that consists of three clauses, A, B, and C. A SAT solver outputs a DRUP proof that tells that a learnt clause D is generated from A and B, a learnt clause E is from B and C, and finally an empty clause is from D and E. In this case, the frequency of each clause, A, B, and C, is 1, 2, and 1, respectively (note that clause B is used twice for deriving clause D and E).  
If extended variables and its clauses really impact the solution, these clauses can appear frequently in the DRUP proof. We use DRUP-trim [13] to translate the DRUP proof into a resolution graph (TRACECHECK format ([[http://fmv.jku.at/tracecheck/README.tracecheck](http://fmv.jku.at/tracecheck/README.tracecheck)]([http://fmv.jku.at/tracecheck/README.tracecheck](http://fmv.jku.at/tracecheck/README.tracecheck)), accessed on 20 November 2022)), and then count the frequency of each clause. After sorting the frequency, we observe the frequently used clauses (e.g., top-100).  
The TRACECHECK format is as follows:  
\[c_{index},\,l_{1},\,l_{2},\,\ldots,\,l_{x},\,0,\,a_{1},\,a_{2},\,\ldots,\,a_{y},\,0\]  
Each element is separated by a single space (commas are used for readability in the above example). One line corresponds to one clause. The number 0 is used as a delimiter. The \(c_{index}\) stands for its index: original clauses in a CNF with \(m\) clauses have an index 1 to \(m\), and derived (learnt) clauses have an index more than \(m\). The clause has \(x\) literals: \(l_{1}\), \(l_{2}\),..., \(l_{x}\). If the clause is a derived one, the clauses with index \(a_{1}\) to \(a_{y}\) are the antecedents that are used to derive the clause by resolution (note that all antecedent indices are less than the \(c_{index}\)).  
We denote \(D_{i}\) as a set of descendants of a clause \(c_{i}\), and define the frequency of a clause \(freq[c_{i}]\) for a DRUP by traversing clause indices in reverse order as follows:  
\[freq[c_{i}]=\sum_{c_{j}\in D_{i}}freq[c_{j}] \tag{4}\]  
Note that the frequency of a clause without any descendants is 1. Since the frequency increases exponentially, it is difficult to calculate exact values with the standard 32- or 64-bit integer used in the standard programming languages. We instead calculate approximated values with 64-bit double floating-point numbers: when the highest frequency exceeds a threshold (we set it as \(10^{200}\)) we multiply all the frequencies with \(10^{-200}\). This approximation can retain the magnitude relationship of the frequencies. Even though some small frequency values can be rounded to 0 due to underflow, we ignore these infrequent ones. In this manner, we finally examine the relative values in descending order, i.e., ranking of frequencies of all the clauses in which we can see the frequently used clauses in a resolution proof.