On the Empirical Time Complexity of Random 3-SAT at the Phase Transition
Authors: Zongxu Mu, Holger H. Hoos
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Here, we study the empirical scaling of the running time of several prominent, high-performance SAT solvers on random 3-SAT instances from the phase transition region. |
| Researcher Affiliation | Academia | Zongxu Mu and Holger H. Hoos Department of Computer Science University of British Columbia {zongxumu, hoos}@cs.ubc.ca |
| Pseudocode | No | The paper does not contain any sections or figures explicitly labeled as 'Pseudocode' or 'Algorithm', nor does it present any structured, code-like blocks for its methods. |
| Open Source Code | No | The paper mentions specific software versions for solvers used (e.g., UBCSAT version 1.2, Balanced Z V2014.05.07), but does not state that the code developed for this research (e.g., for scaling analysis, model fitting, or the new phase transition model) is publicly available. |
| Open Datasets | Yes | All sets of uniform random 3-SAT instances used in our study were obtained using the generator which produced SAT competition instances [Balint et al., 2012]. |
| Dataset Splits | Yes | For each SLS-based solver, both models were fitted using median running times for n = 200, 250, . . . 500 (support) and later challenged with median running times for n = 600, 700, . . . 1000. For each DPLL-based solver, we used support data for n = 200, 250, . . . 400 and challenge data for n = 450, . . . 550... |
| Hardware Specification | Yes | For collecting running time data for our solvers, we used the Compute Canada / Westgrid cluster orcinus (DDR), each equipped with two Intel Xeon E5450 quad-core CPUs at 3.0 GHz with 16GB of RAM running 64-bit Red Hat Enterprise Linux Server 5.3. |
| Software Dependencies | Yes | Walk SAT/SKC [Selman et al., 1994] (UBCSAT version 1.2 [Tompkins and Hoos, 2005]), Balanced Z [Li et al., 2014] (V2014.05.07) and prob SAT [Balint and Schöning, 2014] (version sc14), and three DPLL-based solvers, kcnfs [Dequen and Dubois, 2004] (V2004), march_hi [Heule and van Maaren, 2009] and march_br [Heule, 2013] (version sat+unsat). ... we used runsolver [Roussel, 2011] to record CPU times |
| Experiment Setup | Yes | For our scaling analysis, we considered two parametric models: Exp [a, b] (n) := a bn (2-parameter exponential); Poly [a, b] (n) := a nb (2-parameter polynomial). ... For fitting parametric scaling models to observed data, we used the non-linear least-squares Levenberg Marquardt algorithm. ... we computed 95% bootstrap confidence intervals for the performance predictions obtained from our scaling models, based on 1000 bootstrap samples per instance set and 1000 automatically fitted variants of each scaling model. ... Considering the stochastic nature of the SLS-based solvers, we performed 5 independent runs per instance and used the median over those 5 running times as the running time for the respective instance. |