ThresholdBehaviorinBooleanNetworkModelforSAT[pdf]-.PDF

Threshold behavior in a Boolean Network model for SAT Alejandro Bugacov, Aram Galstyan and Kristina Lerman Information Sciences Institute Univ. of Southern California 4676 Admiralty Way Marina del Rey, CA 90292 {bugacov,galstyan,lerman}@isi.edu February 21, 2003 Abstract Boolean satis?ability (SAT) is the canonical NP-complete problem that plays an important role in AI and has many practical applications in Computer Science in general. Boolean networks (BN) are dynamical systems that have recently been proposed as an algorithm for solving SAT problems [7]. We have carried out a detailed investigation of the dynamical properties of BN corresponding to random SAT problems of di?erent size. We varied the problem size by changing the number of variables and the number of clauses in the Boolean formula. We show that dynamics of BN corresponding to 3-SAT problems display a threshold-like behavior, although this transition occurs far below the well known phase transition in the computational complexity of random 3-SAT. This threshold behavior does not appear to be connected to the transition between frozen and chaotic dynamics regimes of random BN. 1 Introduction Boolean satis?ability (SAT) plays a fundamental role in modern problem-solving techniques. Most com- putational problems arising from real-world applications such as planning, scheduling, resource allocation, protein folding, computer chip veri?cation and routing can be encoded as SAT problems. Some of the most advanced solvers for these problems are based in SAT encodings that when used in combination with state- of-the-art SAT engines [8] can handle large-scale instances very e?c