Disjoint Partial Enumeration without Blocking Clauses
Authors: Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments clearly show the benefits of our novel approach. |
| Researcher Affiliation | Academia | 1DISI, University of Trento 2University of Freiburg giuseppe.spallitta@unitn.it, roberto.sebastiani@unitn.it, biere@cs.uni-freiburg.de |
| Pseudocode | Yes | Algorithm 1: CHRONO-CDCL(F, V), Algorithm 2: ANALYZECONFLICT(T, c, dl), Algorithm 3: ANALYZEASSIGNMENT(T, dl), Algorithm 4: IMPLICANT-SHRINKING(T), Algorithm 5: CHECK-LITERAL(ℓ, b, T ) |
| Open Source Code | Yes | The code of the algorithm and all benchmarks are available here: https://zenodo.org/records/10397723. |
| Open Datasets | Yes | The code of the algorithm and all benchmarks are available here: https://zenodo.org/records/10397723. We considered benchmarks having two characteristics: (i) each problem admits a high number of total assignments; (ii) the problem structure allows for some minimization of assignments, to test the efficiency of the chronological implicant shrinking algorithms. Binary clauses is a crafted dataset containing problems with n variables defined by binary clauses in the form: (x1 xn) (x2 xn 1) ... (xn/2 1 xn/2) Rnd3sat contains 410 random 3-SAT problems with n variables, n [10, 50]. We also tested our algorithms over SATLIB benchmarks, specifically CBS and BMS (Singer, Gent, and Smaill 2000). |
| Dataset Splits | No | The paper uses benchmarks but does not specify training/validation/test splits, nor does it mention cross-validation. |
| Hardware Specification | Yes | Experiments are performed on an Intel Xeon Gold 6238R @ 2.20GHz 28 Core machine with 128 GB of RAM, running Ubuntu Linux 20.04. |
| Software Dependencies | No | The paper mentions it is 'built on top of a minimal SAT solver' and that 'watching data structures are similar to Mini SAT', and that it's 'running Ubuntu Linux 20.04', but does not provide specific version numbers for any key software libraries, frameworks, or solvers used in its implementation or experiments. |
| Experiment Setup | Yes | Timeout has been set to 1200 seconds. After an empirical evaluation, we set Decide to select the priority score of a variable depending on the following ordered set of rules. First, we rely on the Variable State Aware Decaying Sum (VSADS) heuristic (Huang and Darwiche 2005) and set the priority of a variable according to two weighted factors: (i) the count of variable occurrences in the formula, as in the Dynamic Largest Combined Sum (DLCS) heuristics; and (ii) an activity score, which increases when the variable appears in conflict clauses and decreases otherwise, as in the Variable State Independent Decaying Sum (VSIDS) heuristic. If two variables have the same score, we set a higher priority to variables whose watch list is not empty (this is particularly helpful when the lighter variant of the implicant shrinking is used). If there is still a tie, we rely on the lexicographic order of the name of the variables. |