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..
From Single-Objective to Bi-Objective Maximum Satisfiability Solving
Authors: Christoph Jabs, Jeremias Berg, Andreas Niskanen, Matti Järvisalo
JAIR 2024 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective Max SAT solving on several real-world domains from the literature, showing the practical benefits of our approach. |
| Researcher Affiliation | Academia | Christoph Jabs EMAIL Jeremias Berg EMAIL Andreas Niskanen EMAIL Matti J arvisalo EMAIL Department of Computer Science, University of Helsinki, Finland |
| Pseudocode | Yes | Algorithm 1 describes in pseudocode the Bi Opt Sat framework for computing the Paretooptimal solutions of a given bi-objective Max SAT instance I = (F, OI, OD). |
| Open Source Code | Yes | We provide an open-source implementation (available at https://bitbucket.org/coreogroup/bioptsat/) of all the described instantiations of Bi Opt Sat. |
| Open Datasets | Yes | The benchmarks are available at https://bitbucket.org/coreo-group/bioptsat/src/master/jair24. ... We generated the LIDR instances using 24 UCI (Dua & Graff, 2021) and Kaggle (https: //www.kaggle.com) benchmark datasets ... We used Pack UP to generate instances based on 142 package upgradeability instances from Mancoosi International Solver Competition 2011 (https:// www.mancoosi.org/misc-2011/). ... obtained from Max SAT Lib (http://www.cs.toronto.edu/maxsat-lib/maxsat-instances/). |
| Dataset Splits | No | The paper describes how instances were generated and sampled (e.g., 'independently at random sampled subsets of n {50, 100, 1000, 5000, 10000} data samples from the datasets'), but does not specify traditional training/test/validation splits for the evaluation of a learning model. The problem is framed as a combinatorial optimization task to find Pareto-optimal solutions directly from the dataset, not to train a model on one split and evaluate on another. |
| Hardware Specification | Yes | All experiments reported on in this section were run on 2.60-GHz Intel Xeon E5-2670 machines with 64-GB RAM in RHEL under a 1.5-hour per-instance time and 16-GB memory limit. |
| Software Dependencies | Yes | All of our implementations use the state-of-the-art SAT solver Ca Di Ca L 1.5.2 (Biere, Fazekas, Fleury, & Heisinger, 2020). ... We use CPLEX v20.10 for the hitting set computations in the experiments. |
| Experiment Setup | Yes | All experiments reported on in this section were run on 2.60-GHz Intel Xeon E5-2670 machines with 64-GB RAM in RHEL under a 1.5-hour per-instance time and 16-GB memory limit. ... The hybrids MSHybrid and OSHybrid are configured to switch between MSU3/OLL and SAT-UNSAT once 70% of OI is active. |