SAT Modulo Monotonic Theories
Authors: Sam Bayless, Noah Bayless, Holger Hoos, Alan Hu
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We have implemented several monotonic theory solvers using the techniques we present in this paper and applied these to content generation problems, demonstrating major speed-ups over SAT, SMT, and Answer Set Programming solvers, easily solving instances that were previously out of reach. |
| Researcher Affiliation | Academia | Sam Bayless sbayless@cs.ubc.ca Univ. of British Columbia Noah Bayless nbayless@pgmini.org Point Grey Mini Sec. School Holger H. Hoos hoos@cs.ubc.ca Univ. of British Columbia Alan J. Hu ajh@cs.ubc.ca Univ. of British Columbia |
| Pseudocode | No | The paper describes algorithms (e.g., "Algorithm: Ramalingam-Reps", "Algorithm: Andrew’s monotone chain algorithm") but does not provide structured pseudocode blocks or algorithms. |
| Open Source Code | Yes | MONOSAT is open-source and freely available online, at www.cs.ubc.ca/labs/isd/Projects/monosat |
| Open Datasets | No | The paper describes problem instances for content generation (e.g., 'Diorama considers a set of undirected, planar edges arranged in a grid') and evaluates solvers on these instances, but does not refer to a publicly available dataset with clear access information for training purposes. The problems are generated for testing solver performance rather than using a pre-existing dataset with train/validation/test splits. |
| Dataset Splits | No | The paper evaluates solver performance on various problem instances but does not specify dataset splits (e.g., percentages or sample counts) for training, validation, or testing, nor does it refer to predefined splits from standard benchmarks. |
| Hardware Specification | Yes | Experiments were conducted on an Intel X5650 CPU, 2.67GHz (12MB L3), in Ubuntu 12.04, 64-bit, with 16 GB RAM, limited to 3600 seconds (walltime). |
| Software Dependencies | Yes | We provide comparisons of our solver MONOSAT (based on the SAT solver MINISAT 2.2) against MINISAT and the ASP solver CLASP 3.10 (for the graph predicates) and against the SMT solver Z3 4.3.1 [De Moura and Bjorner, 2008] (for the geometric predicates, which rely on arbitrary precision arithmetic and cannot be concisely encoded in SAT or ASP). |
| Experiment Setup | Yes | For shortest paths, we show only results for the unary encodings, as we found that the more concise binary encoding always performed very poorly. For maximum flows, both encodings require the solver to guess flows non-deterministically, and here the binary encodings perform better (and we present those results). For the SMT convex-hull encoding, we used an encoding that nondeterministically guesses separating axes between hulls; it compares all pairs of points and requires quadratic space. |