Unifying SAT-Based Approaches to Maximum Satisfiability Solving
Authors: Hannes Ihalainen, Jeremias Berg, Matti Järvisalo
JAIR 2024 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | While the main focus of this work is evidently on the general formal algorithmic framework, as an illustration of its potential for obtaining novel types of unsatisfiability-based algorithms we more shortly outline and provide a prototype implementation of a core-guided variant for Max SAT obtained through the framework. We empirically compare the runtimes of CGSS2-Abst CG (our prototype implementation of Abst CG) to those of CGSS2-OLL, i.e., the base CGSS2 implementation. Figure 5 (left) provides a runtime comparison for the two solvers with all additional heuristics implemented in CGSS2 enabled. |
| Researcher Affiliation | Academia | Hannes Ihalainen EMAIL Jeremias Berg EMAIL Matti J arvisalo EMAIL Department of Computer Science, University of Helsinki, Finland |
| Pseudocode | Yes | Algorithm 1 The objective-bounding search approach to Max SAT Algorithm 2 The core-guided approach to Max SAT Algorithm 3 The implicit hitting set approach to Max SAT Algorithm 4 Uni Max SAT, a unifying framework for SAT-based Max SAT algorithms |
| Open Source Code | Yes | we developed a prototype implementation of Abst CG on top of CGSS2, a state-of-the-art C++ implementation of OLL (Ihalainen, 2022). This implementation of Abst CG is available online at https://bitbucket.org/coreo-group/cgss2/ as a command line option of CGSS2. |
| Open Datasets | Yes | As benchmarks, we used the 558 instances weighted instances9 from the exact track of Max SAT Evaluation 2023 (https://maxsat-evaluations.github.io/2023/). |
| Dataset Splits | No | As benchmarks, we used the 558 instances weighted instances9 from the exact track of Max SAT Evaluation 2023 (https://maxsat-evaluations.github.io/2023/). The experiments were run using 2.6GHz AMD EPYC 7H12 processors under a per-instance 3600-second time and 16-GB memory limit. |
| Hardware Specification | Yes | The experiments were run using 2.6GHz AMD EPYC 7H12 processors under a per-instance 3600-second time and 16-GB memory limit. |
| Software Dependencies | No | we developed a prototype implementation of Abst CG on top of CGSS2, a state-of-the-art C++ implementation of OLL (Ihalainen, 2022). |
| Experiment Setup | Yes | The experiments were run using 2.6GHz AMD EPYC 7H12 processors under a per-instance 3600-second time and 16-GB memory limit. Figure 5 (left) provides a runtime comparison for the two solvers with all additional heuristics implemented in CGSS2 enabled. Figure 5 (right) provides a runtime comparison for the two solvers with WCE and SS disabled. |