Finding the Hardest Formulas for Resolution
Authors: Tomáš Peitl, Stefan Szeider
JAIR 2021 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | As our main contribution, we compute the first ten resolution hardness numbers. In order to do so, we have to efficiently generate sets of formulas χ(m), for m = 1, . . . , 10, which contain at least one hardest formula, and compute their resolution complexity. We obtain our results by the combination of two techniques: 1. A candidate filtering and symmetry breaking search scheme for limiting the number of potential candidate formulas with m variables whose resolution complexity is hm. 2. An efficient SAT encoding for computing the resolution complexity of a given candidate formula. [...] In this section we present and explore in detail the results of our computation. |
| Researcher Affiliation | Academia | Tom aˇs Peitl EMAIL Institute of Computer Science, Friedrich Schiller University Jena Ernst-Abbe-Platz 2, 07743 Jena, Germany Stefan Szeider EMAIL Institute of Logic and Computation, TU Wien Favoritenstraße 9-11, 1040 Wien, Austria |
| Pseudocode | Yes | Algorithm 1 Deciding saturated minimal unsatisfiability in one pass through the set of assignments. |
| Open Source Code | Yes | Our encoding (Peitl & Szeider, 2021b) and our catalog of SMU formulas (Peitl & Szeider, 2021a), including the data from our computation, are publicly available. Peitl, T., & Szeider, S. (2021b). short.py: Encoding for the shortest resolution proof. Zenodo. https://doi.org/10.5281/zenodo.3951549. |
| Open Datasets | Yes | Our encoding (Peitl & Szeider, 2021b) and our catalog of SMU formulas (Peitl & Szeider, 2021a), including the data from our computation, are publicly available. Peitl, T., & Szeider, S. (2021a). Saturated Minimally Unsatisfiable Formulas on up to Ten Clauses. Zenodo. https://doi.org/10.5281/zenodo.3951545. |
| Dataset Splits | No | The paper describes generating candidate formulas and computing their resolution hardness. It does not involve typical dataset splits (training/validation/test) for model training or evaluation. The generated formulas are individual instances for which a property (resolution hardness) is computed. |
| Hardware Specification | Yes | Figure 3 shows the running time needed to compute shortest proofs as a function of their length, on a 10-core 2.40GHz Intel Xeon E5-2640 v4. |
| Software Dependencies | Yes | We implemented the encoding and the iterative search for a shortest proof in Python using the Py SAT framework (Ignatiev, Morgado, & Marques-Silva, 2018). Our tool allows the user to choose their favorite SAT solver among the ones included in Py SAT, or indeed any other that they have installed. Similarly, the user can specify which CNF cardinality encoding (among the ones implemented in Py SAT) to use within our encoding. Since these parameters can be expected to have a significant impact on performance, before we started our experiments, we performed a grid search through all pairs of SAT solver (the ones in Py SAT + Kissat and Crypto Mini SAT 5.8) and cardinality encoding, using a randomly sampled set of RSMU(8), RSMU(9), SSMU(8), and SSMU(9) formulas, 32 of each kind. From this training phase we concluded that the configuration with Ca Di Ca L 4 and sequential counter performed best, and we used it throughout the rest of the experiment. |
| Experiment Setup | Yes | Our implementation allows to pass the cardinality encoding to be used as a parameter. From this training phase we concluded that the configuration with Ca Di Ca L 4 and sequential counter performed best, and we used it throughout the rest of the experiment. We implemented the encoding and the iterative search for a shortest proof in Python using the Py SAT framework. |