Satsisfiability and Systematicity
Authors: Matthew L Ginsberg
JAIR 2015 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results are presented in Section 4 and concluding remarks are in Section 5. On large number factoring problems, flex appears to outperform weakly systematic approaches. |
| Researcher Affiliation | Industry | Matthew L. Ginsberg Connected Signals, Inc. |
| Pseudocode | Yes | Procedure 2.12 (CDCL) Let T be a theory, Γ a set of clauses such that T |= Γ, and B a bias for T. Then to compute cdcl(T, Γ, B, n), one of: if T is shown to be unsatisfiable, a model P of T if one is found, or unknown if no solution is found after n steps: Procedure 3.6 To compute add(γ, Γ, ): Procedure 3.8 (Pure FLEX) Let T be a theory, Γ a set of clauses such that T |= Γ, a partial order on the variables in T, and B a bias for T. |
| Open Source Code | Yes | The software used in these experiments is available as an online appendix to this paper. stlsat.zip contains the source for stlsat, and flex.zip contains the source for flex. (Stlsat is just flex with the various extensions removed.) |
| Open Datasets | Yes | The first was the set of 1030 problems in the sat 2013 benchmarks. The second set of problems used were number factoring problems (Bebel & Yuen, 2013). The number factoring problems were generated by using an iterated Miller-Rabin test to generate pairs of primes and then using the Purdom/Sabry (2005) sat generator to produce a sat encoding of the problem of factoring the product of these primes. |
| Dataset Splits | Yes | For any given problem size (number of bits in the number being factored), fifty instances were generated randomly. |
| Hardware Specification | Yes | All experiments were run on a 24-core Intel Xeon machine running at 2.2GHz with 256K of L2 cache per processor, 24GB of main memory, and 75GB of swap space. |
| Software Dependencies | Yes | As a baseline solver, we used minisat 2.2 (S orensson & Een, 2005). But there were in fact three separate sets of changes that we needed to make to produce flex: 1. First, we converted minisat from C to C++ and changed it to use the C++ standard library in many locations instead of the variety of specialized techniques included in minisat. We will refer to this solver as stlsat. |
| Experiment Setup | Yes | In order to increase the number of probes, we reduced the multiplicative factor to four (so that the first probe involves only four backtracks). We will refer to this solver as stlsat4. 3. Finally, we modified stlsat to produce flex, also with an initial probe size of four. |