Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Clause Elimination for SAT and QSAT
Authors: Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere
JAIR 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving. |
| Researcher Affiliation | Academia | Marijn Heule EMAIL Department of Computer Science, The University of Texas at Austin, USA Matti Jarvisalo EMAIL HIIT, Department of Computer Science, University of Helsinki, Finland Florian Lonsing EMAIL Institute of Information Systems, Vienna University of Technology, Austria Martina Seidl EMAIL Institute for Formal Models and Verification, Johannes Kepler University Linz, Austria Armin Biere EMAIL Institute for Formal Models and Verification, Johannes Kepler University Linz, Austria |
| Pseudocode | Yes | Figure 3: Pseudo-code for reconstructing a solution with F a reduced formula, τ a satisfying assignment for F and S a set of eliminated clauses ordered by last eliminated. |
| Open Source Code | Yes | To this end, we implemented those techniques in the QSAT preprocessor BLOQQER (version 35) (Seidl & Biere, 2015). Seidl, M., & Biere, A. (2015). Bloqqer. http://fmv.jku.at/bloqqer. |
| Open Datasets | Yes | As benchmarks, we used standard competition benchmark sets from the most recent SAT Competition (SAT Competitions Organizing Committee, 2014) and QSAT solver evaluation (Jordan & Seidl, 2014), focusing on real-world application instances. For evaluating our implementation, we considered the benchmarks of the QBFLib track and of the Application track of the QBF Gallery 2014 (Jordan & Seidl, 2014). |
| Dataset Splits | No | The paper mentions using competition benchmark sets from SAT Competition 2013 and QBF Gallery 2014, including the QBFLib track (345 formulas) and Application track (735 formulas). While these are standard benchmark sets, the paper does not specify how these datasets were further split (e.g., into training, validation, or test sets with percentages or sample counts) for their own experiments beyond using the competition sets themselves. |
| Hardware Specification | Yes | All experiments were performed on a cluster of 2.8-GHz Intel Core 2 Quad machines each equipped with 8-GB memory and running Ubuntu 9.04. |
| Software Dependencies | Yes | We evaluated the effectiveness of clause elimination procedures in the context of state-of-the-art SAT solvers, more specifically LINGELING version aqw (Biere, 2013). ... we implemented those techniques in the QSAT preprocessor BLOQQER (version 35) (Seidl & Biere, 2015). |
| Experiment Setup | Yes | As the benchmark set we used the same instances as in the application track of the SAT 2013 competition, with the time limit of 5000 seconds per benchmark... The time and memory limits were set to 900 seconds and 7 GB, respectively. ... The configuration of LINGELING with all the clause elimination procedures disabled is called with the following command line options: --no-bate --no-block --no-cce --no-transred. By specifying --plain we further compare a configuration where preand inprocessing is disabled with a configuration which only uses clause elimination procedures during preand inprocessing, using --plain --bate --block --cce=3 --transred, which first disables all preprocessing and then selectively enables all clause elimination procedure, combined with --batewait=0 --blockwait=0 --ccewait=1. |