Behavior of heuristics and state space structure near SAT/UNSAT transition

@misc{citeulike:488637, 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.}, author = {Ardelius, John and Aurell, Erik }, citeulike-article-id = {488637}, eprint = {cond-mat/0601703}, keywords = {0-student-shelaev, phase-transition, satisfiability}, month = {Jan}, posted-at = {2006-02-01 15:39:46}, priority = {3}, title = {Behavior of heuristics and state space structure near SAT/UNSAT transition}, url = {http://arxiv.org/abs/cond-mat/0601703}, year = {2006} }

TY - ELEC ID - citeulike:488637 L3 - citeulike-article-id:488637 TI - Behavior of heuristics and state space structure near SAT/UNSAT transition N2 - 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. KW - 0-student-shelaev KW - phase-transition KW - satisfiability AU - Ardelius, John AU - Aurell, Erik PY - 2006/Jan/31/ UR - http://arxiv.org/abs/cond-mat/0601703 ER -