Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Unifying SAT-Based Approaches to Maximum Satisfiability Solving
Authors: Hannes Ihalainen, Jeremias Berg, Matti Järvisalo
JAIR 2024 | Venue PDF | 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. |