From Single-Objective to Bi-Objective Maximum Satisfiability Solving
Authors: Christoph Jabs, Jeremias Berg, Andreas Niskanen, Matti Järvisalo
JAIR 2024 | Venue PDF | Archive PDF | Plain Text | 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. |