Reducing SAT to Max2SAT
Authors: Carlos Ansótegui, Jordi Levy
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this paper, we provide an efficient and constructive method for Reducing SAT to Max2SAT and show empirical results of how Max SAT solvers are more efficient than SAT solvers solving the translation of hard formulas for Resolution. |
| Researcher Affiliation | Academia | Carlos Ans otegui1 and Jordi Levy2 1Logic & Optimization Group (LOG), University of Lleida 2IIIA-CSIC carlos.ansotegui@udl.cat, levy@iiia.csic.es |
| Pseudocode | Yes | Algorithm 1: SAT through Max SAT |
| Open Source Code | No | The paper does not provide a link or explicit statement about releasing the source code for their methodology. |
| Open Datasets | No | The paper mentions generating PHPn n 1 SAT instances and the Pigeon Hole principle but does not provide access information (link, DOI, citation with authors/year) for a publicly available or open dataset. |
| Dataset Splits | No | The paper mentions generating PHPn n 1 SAT instances but does not specify any training, validation, or test splits for these instances. |
| Hardware Specification | Yes | The machine has 2.1GHz and 5GB RAM. We used a machine of 2.1GHz and 5GB RAM memory. |
| Software Dependencies | Yes | In particular, we experimented with SAT solver Ca Di Ca L (version 1.0.3) and the top performing three Max SAT solvers from the weighted category of the Max SAT Evaluation 2020 [Bacchus et al., 2019]: RC2 [Ignatiev et al., 2019], Max HS [Davies and Bacchus, 2011] and Uwrmaxsat [Piotr ow, 2020]. |
| Experiment Setup | Yes | The Max SAT solvers were run on a Max SAT formula built from the generated PHPn n 1 SAT instance ϕ as follows: the 2SAT clauses in ϕ are assigned weight and the rest (n 1)ary clauses are translated into Max SAT using a gadget. |