Behavior of heuristics and state space structure near SAT/UNSAT transition
Statistical Mechanics
2013-05-29 v1
Abstract
We study the behavior of ASAT, a heuristic for solving satisfiability problems by stochastic local search near the SAT/UNSAT transition. The heuristic is focused, i.e. only variables in unsatisfied clauses are updated in each step, and is significantly simpler, while similar to, walksat or Focused Metropolis Search. We show that ASAT solves instances as large as one million variables in linear time, on average, up to 4.21 clauses per variable for random 3SAT. For K higher than 3, ASAT appears to solve instances at the ``FRSB threshold'' in linear time, up to K=7.
Cite
@article{arxiv.cond-mat/0601703,
title = {Behavior of heuristics and state space structure near SAT/UNSAT transition},
author = {John Ardelius and Erik Aurell},
journal= {arXiv preprint arXiv:cond-mat/0601703},
year = {2013}
}
Comments
12 pages, 6 figures, longer version available as MSc thesis of first author at http://biophys.physics.kth.se/docs/ardelius_thesis.pdf