Non-Restarting SAT Solvers with Simple Preprocessing Can Efficiently Simulate Resolution
Authors: Paul Beame, Ashish Sabharwal
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We study non-restarting CDCL solvers that learn only one asserting clause per conflict and show that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. We show, moreover, that this preprocessing allows one to convert any CDCL solver to one that is non-restarting. |
| Researcher Affiliation | Collaboration | Paul Beame Computer Science and Engineering University of Washington Seattle, WA 98195, USA beame@cs.washington.edu Ashish Sabharwal IBM Watson Research Center 1101 Kitchawan Road Yorktown Heights, NY 10598, USA ashish.sabharwal@us.ibm.com |
| Pseudocode | Yes | Algorithm 1: p-simulation of a resolution refutation by a CDCL solver with simple preprocessing |
| Open Source Code | No | The information is insufficient. The paper does not provide any statement or link regarding the release of source code for the methodology described. |
| Open Datasets | No | The information is insufficient. The paper is theoretical and uses general 'CNF formulas' without reference to specific datasets, their availability, or access information. |
| Dataset Splits | No | The information is insufficient. The paper does not describe any dataset splits for training, validation, or testing. |
| Hardware Specification | No | The information is insufficient. The paper is theoretical and does not describe empirical experiments, thus no hardware specifications are provided. |
| Software Dependencies | No | The information is insufficient. The paper is theoretical and does not describe empirical experiments, thus no specific software dependencies with version numbers are provided. |
| Experiment Setup | No | The information is insufficient. The paper is theoretical and does not describe empirical experiments, thus no specific experimental setup details like hyperparameters or training configurations are provided. |