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 [1].
A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size
Authors: Mario Alviano, Carmine Dodaro, Francesco Ricca
IJCAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The performance of MAXINO was assessed on the industrial instances of the 2014 Max SAT Evaluation [Argelich et al., 2014], which includes three tracks, namely Max SAT (MS; 55 instances), Partial Max SAT (PMS; 568 instances) and Weighted Partial Max SAT (WPMS; 410 instances). The experiment was run on an Intel Xeon CPU 2.4 GHz with 16 GB of RAM. |
| Researcher Affiliation | Academia | Mario Alviano and Carmine Dodaro and Francesco Ricca Department of Mathematics and Computer Science, University of Calabria, Italy EMAIL |
| Pseudocode | Yes | Algorithm 1: Core-guided Max SAT algorithm |
| Open Source Code | Yes | Prototype and formal proofs are available online at the following link: http://alviano.net/software/maxino/. |
| Open Datasets | Yes | The performance of MAXINO was assessed on the industrial instances of the 2014 Max SAT Evaluation [Argelich et al., 2014], which includes three tracks, namely Max SAT (MS; 55 instances), Partial Max SAT (PMS; 568 instances) and Weighted Partial Max SAT (WPMS; 410 instances). |
| Dataset Splits | No | The paper describes using industrial instances for evaluation but does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) for training, validation, or testing. |
| Hardware Specification | Yes | The experiment was run on an Intel Xeon CPU 2.4 GHz with 16 GB of RAM. |
| Software Dependencies | Yes | ONE and K have been implemented in MAXINO, a new pseudo-Boolean solver extending the single-thread version of GLUCOSE 4 [Audemard and Simon, 2009] |
| Experiment Setup | Yes | CPU and memory usage were limited to 1,800 seconds and 8 GB, respectively. |