Phase Transitions for Scale-Free SAT Formulas
Authors: Tobias Friedrich, Anton Krohmer, Ralf Rothenberger, Andrew Sutton
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We also perform computational studies that suggest our bound is tight and investigate the critical density for formulas with higher clause lengths. For k > 2, we perform a computational study to provide a more detailed picture of the phase transition for scale-free formulas, and clarify the regime of hard formulas. |
| Researcher Affiliation | Academia | Tobias Friedrich, Anton Krohmer, Ralf Rothenberger, Andrew M. Sutton Algorithm Engineering Group Hasso Plattner Institute Potsdam, Germany |
| Pseudocode | Yes | To sample Φ, we generate each clause c as follows. 1. Sample k variables independently at random according to the distribution pi. Repeat until no variables coincide. 2. Negate each of the k variables independently at random with probability 1/2. |
| Open Source Code | No | The paper does not provide any links to open-source code or state that the code for the described methodology is publicly available. |
| Open Datasets | Yes | We used the Clauset-Shalizi-Newman method (2009) to estimate the power-law exponent in the industrial data and match it in the randomly generated formula. The figure is generated by plotting the empirical cumulative variable distribution of two groups of industrial formulas selected from SAT Race 2015 competition: hwmcc10 (hardware model checking) and SAT dat (IBM formal verification suite). |
| Dataset Splits | No | The paper describes how formulas are generated and then solved by various SAT solvers. It does not refer to or provide specific training/validation/test dataset splits in the context of training a model for their own research. |
| Hardware Specification | No | The paper does not specify any particular hardware (e.g., CPU, GPU models, memory) used for running the experiments. |
| Software Dependencies | Yes | Each resulting formula is solved by the CDCL-based solver Maple COMSPS (Liang et al. 2016) with a time cutoff of 900 seconds (15 min). Our solver choice is motivated by the good performance of Maple COMSPS on the Application Benchmarks at the SAT 2016 competition. |
| Experiment Setup | Yes | In an interest to eliminate statistical fluctuations that can arise at small problem sizes, we set n very large, specifically n = 107 for k = 2 and n = 106 for k > 2. For the appropriate value of n, 50 scale-free formulas are generated for each β = 1.5, 1.6, . . . , 3.5 and each m such that m/n = 1/10, 2/10, . . . , 5 (for k = 2 we use increments of 1/50 with maximum m/n = 1). Each resulting formula is solved by the CDCL-based solver Maple COMSPS (Liang et al. 2016) with a time cutoff of 900 seconds (15 min). |