Combining the
Authors: k
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We show empirical evidence of a surprising phase-transition that follows a linear trade-off between k-CNF and XOR constraints. Furthermore, we prove that a phase-transition for k-CNF-XOR formulas exists for k = 2 and (when the number of k-CNF constraints is small) for k > 2. |
| Researcher Affiliation | Academia | Jeffrey M. Dudek Rice University Kuldeep S. Meel Rice University Moshe Y. Vardi Rice University |
| Pseudocode | No | The paper describes experimental procedures in prose but does not include any structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions data availability at a URL, and refers to the third-party tool Crypto Mini SAT with its own URL, but does not explicitly provide a link to the authors' own source code for their described methodology. |
| Open Datasets | No | The paper describes the generation process for k-CNF and XOR clauses for the experiments but does not refer to a pre-existing publicly available dataset or provide access information for specific experimental data. |
| Dataset Splits | No | The paper describes generating formulas for testing satisfiability but does not mention specific training, validation, or test dataset splits. |
| Hardware Specification | Yes | Each experiment was run on a node within a high-performance computer cluster. These nodes contain 12-processor cores at 2.83 GHz each with 48 GB of RAM per node. |
| Software Dependencies | No | The paper mentions using 'Crypto Mini SAT' and 'Python' but does not specify their version numbers or other software dependencies with versions. |
| Experiment Setup | Yes | In each experiment, the XOR-clause density s ranged from 0 to 1.2 in increments of 0.02. Since the location of phasetransition for k CNF depends on k, the range of k-clause density r also depends on k. For k = 3, r ranged from from 0 to 6 in increments of 0.04; for k = 5, r ranged from 0 to 26 in increments of 0.43, and the like. ... For each assignment of values to k, n, r, and s, we evaluated satisfiability, using Crypto Mini SAT, of 100 uniformly generated formulas of k(n, rn, sn) by constructing the conjunction of drne k-clauses and dsne XOR-clauses... Each formula was given a timeout of 1000 seconds. |