Augmenting the Power of (Partial) MaxSat Resolution with Extension
Authors: Javier Larrosa, Emma Rollon1561-1568
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To corroborate the ideas developed in the paper and demonstrate the potential of Max Res E, we conducted some experiments on hard and soft PHPs with 5 m 75 using SAT solvers Glucose 3.0 (Audemard and Simon 2018) and Minisat 2.2 (E en and S orensson 2003), and Max SAT solvers RC2 (Ignatiev, Morgado, and Marques-Silva 2018b) and FM (Manquinho, Marques-Silva, and Planes 2009) (extended to the case of weighted partial formulas) provided by the Py Sat 0.1.4 toolkit (Ignatiev, Morgado, and Marques Silva 2018a). For both Max SAT solvers we used Minisat 2.2 as their underline SAT solver. All experiments were performed in Ubuntu Linux 16.04.6 LTS with 8 Gb RAM and CPU Intel i5-7400 @ 3.00 GHz. Figure 7 shows the experimental results. |
| Researcher Affiliation | Academia | Javier Larrosa, Emma Rollon Universitat Polit ecnica de Catalunya, Jordi Girona 1-3, Barcelona 08034 {larrosa, erollon}@cs.upc.edu |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. It uses mathematical definitions and diagrams (e.g., Figure 2, 3, 4, 5, 6) to illustrate proofs. |
| Open Source Code | No | The paper mentions using existing SAT/MaxSAT solvers and a toolkit (Py Sat 0.1.4 toolkit) but does not provide open-source code for the Max Res E proof system or its implementation described in the paper. |
| Open Datasets | No | The paper discusses the Pigeon Hole Problem (PHP) and its soft/hard encodings, which are theoretical problem formulations rather than specific, publicly accessible datasets with links or formal citations. It mentions the 'size of the original formula is O(m3)' but this refers to the constructed problem instance, not an external dataset. |
| Dataset Splits | No | The paper does not explicitly provide training/test/validation dataset splits. It describes generating problem instances (PHPsoft, PHPhard) of varying sizes (m from 5 to 75) and solving them with different solvers, but not data partitioning for machine learning models. |
| Hardware Specification | Yes | All experiments were performed in Ubuntu Linux 16.04.6 LTS with 8 Gb RAM and CPU Intel i5-7400 @ 3.00 GHz. |
| Software Dependencies | Yes | SAT solvers Glucose 3.0 (Audemard and Simon 2018) and Minisat 2.2 (E en and S orensson 2003), and Max SAT solvers RC2 (Ignatiev, Morgado, and Marques-Silva 2018b) and FM (Manquinho, Marques-Silva, and Planes 2009) (extended to the case of weighted partial formulas) provided by the Py Sat 0.1.4 toolkit (Ignatiev, Morgado, and Marques Silva 2018a). For both Max SAT solvers we used Minisat 2.2 as their underline SAT solver. |
| Experiment Setup | Yes | To corroborate the ideas developed in the paper and demonstrate the potential of Max Res E, we conducted some experiments on hard and soft PHPs with 5 m 75 using SAT solvers Glucose 3.0 (Audemard and Simon 2018) and Minisat 2.2 (E en and S orensson 2003), and Max SAT solvers RC2 (Ignatiev, Morgado, and Marques-Silva 2018b) and FM (Manquinho, Marques-Silva, and Planes 2009) (extended to the case of weighted partial formulas) provided by the Py Sat 0.1.4 toolkit (Ignatiev, Morgado, and Marques Silva 2018a). For both Max SAT solvers we used Minisat 2.2 as their underline SAT solver. |