Solving #SAT and MAXSAT by Dynamic Programming
Authors: Sigve Hortemo Sæther, Jan Arne Telle, Martin Vatshelle
JAIR 2015 | Venue PDF | Archive PDF | Plain Text | 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. |