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..
Solving #SAT and MAXSAT by Dynamic Programming
Authors: Sigve Hortemo Sæther, Jan Arne Telle, Martin Vatshelle
JAIR 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present some limited experimental results, comparing implementations of our algorithms to state-of-the-art #SAT and Max SAT solvers, as a proof of concept that warrants further research. |
| Researcher Affiliation | Academia | Sigve Hortemo Sæther EMAIL Jan Arne Telle EMAIL Martin Vatshelle EMAIL Department of Informatics, University of Bergen Bergen, Norway |
| Pseudocode | Yes | Procedure 1: Generating PS (Fv) input: PS (Fc1) and PS (Fc2) for children c1 and c2 of v in branch decomposition output: PS (Fv) L empty trie of projection satisfiable clause-sets for each (C1, C2) PS (Fc1) PS (Fc2) do add (C1 C2) cla(Fv) to L return L |
| Open Source Code | Yes | All our code can be found online (Sæther, Telle, & Vatshelle, 2015). We have implemented Greedy Order in Java, together with a straight-forward implementation of the DP algorithm of Theorem 3. ... All our implementations can be found online (Sæther, Telle, & Vatshelle, 2015). |
| Open Datasets | No | The paper describes the generation of synthetic instances for experimental evaluation (Generation of Instances, Section 6.1) rather than using existing publicly available datasets. For example: "To generate a formula of type 1 with n variables and m clauses, we generate n + m intervals of the real line...". |
| Dataset Splits | No | The paper describes methods for generating problem instances (CNF formulas) for testing and comparison of solvers, rather than using a fixed dataset with predefined train/test/validation splits. The experimental evaluation focuses on the performance of algorithms on these generated instances. |
| Hardware Specification | Yes | We ran all the solvers on a Dell Optiplex 780 running Ubuntu 12.04 64-Bit. The machine has 8GB of memory and an Intel Core 2 Quad Q9650 processor with Open JDK java 6 (Iced Tea6 1.13.5). |
| Software Dependencies | Yes | We ran all the solvers on a Dell Optiplex 780 running Ubuntu 12.04 64-Bit. The machine has 8GB of memory and an Intel Core 2 Quad Q9650 processor with Open JDK java 6 (Iced Tea6 1.13.5). ... We compare our implementation to the best solvers we could find online, respectively CCLS-to-akmaxsat (Luo, Cai, Wu, Jie, & Su, 2014) which was among the best solvers of the Ninth Max-SAT Evaluation (2014), and the latest version of the #SAT solver called sharp SAT (Thurley, n.d., 2006). ... a state-ofthe-art SAT solver, like lingeling (Biere, 2014), handles all generated instances within a few seconds. |
| Experiment Setup | Yes | Let us start by describing a very simple heuristic for step (1). It takes as input the bipartite graph I(F) with vertex set cla(F) var(F), and outputs a linear order σ on the vertex set. The below heuristic Greedy Order is a greedy algorithm... We do not enhance our implementations with any other techniques, not even simple pre-processing... The generation of these formulas is based on the definition of interval orderings given by the interval bigraph definition... To generate a formula of type 1 with n variables and m clauses, we generate n + m intervals of the real line... The formulas of type 2 are generated in a very similar fashion as type 1, except we guarantee that all clauses have the same size t... The formulas of type 3 are the CNF-representation of a conjunction of XOR functions where each XOR has a fixed number t of literals and the variables of the XOR functions overlap in such a way that the incidence graph will be the bipartization of a circular arc graph. A formula of type 3 is generated from three input parameters n, t, s. |