MaxSAT Resolution With the Dual Rail Encoding
Authors: Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results on formulas encoding this variant of PHP confirm that the practical implementation of DRMax SAT outperforms modern CDCL SAT solvers. |
| Researcher Affiliation | Academia | Maria Luisa Bonet,1 Sam Buss,2 Alexey Ignatiev,3,4 Joao Marques-Silva,3 Antonio Morgado3 1Computer Science Department, Universidad Polit ecnica de Catalu na, Barcelona, Spain 2Department of Mathematics, University of California, San Diego, USA 3LASIGE, Faculdade de Ciˆencias, Universidade de Lisboa, Portugal 4ISDCT SB RAS, Irkutsk, Russia |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide concrete access to source code for the methodology described in this paper. |
| Open Datasets | No | The paper describes generating specific formula instances ('doubled pigeonhole formulas', 'PHP2m+1 m formulas') for experiments but does not provide concrete access information (link, DOI, repository, or formal citation with authors/year) for a publicly available or open dataset. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce the data partitioning. |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types with speeds, memory amounts, or detailed computer specifications) used for running its experiments. |
| Software Dependencies | Yes | We tested two CDCL SAT solvers: Glucose 3 (Audemard, Lagniez, and Simon 2013) and lingeling2 (Biere 2013a; 2014). Also, the Max SAT solvers used are: Max HS (Davies and Bacchus 2011; 2013a; 2013b), LMHS (Saikko, Berg, and J arvisalo 2016), Eva500a (Narodytska and Bacchus 2014), Open WBO16 (Martins, Manquinho, and Lynce 2014), and MSCG (Morgado, Ignatiev, and Marques-Silva 2015). |
| Experiment Setup | Yes | SAT solvers can only deal with PHP2m+1 m for m 7 given 1800s timeout... Cardinality reasoning (Biere 2013a), which helps lingeling deal with PHP formulas, was disabled... the performance of all Max SAT solvers gets tremendously increased when clauses (pi ni, ) are discarded |