Phase transitions of boolean satisfiability variants
Delbert D. Bailey, Phokion G. Kolaitis · 2004
During the past decade, there has been an intensive investigation of phase transitions in Boolean satisfiability problems. This work has been motivated in large part by the apparent striking relationship of algorithm performance to the location of the phase transition. We explore three different types of generalizations of Boolean satisfiability with the goal to extend the understanding of how the structural phase transition emerges and how its emergence affects the behavior of algorithms. The generalizations consist of introducing variations in the definition of the SAT decision problem in three different ways. Threshold Counting SAT is a decision problem that allows specification of a threshold value for the number of satisfying assignments that must exist. Bounded SAT allows specification of a bound for how many clauses may be violated. Generalized SAT allows specification of the kinds of clause types that are allowed and provides for specification of more than just simple disjunctions. We explore these problems both analytically and experimentally. With the threshold problems, we discover an interesting PP-complete problem phase transition, and develop a parameterized family of decision problems that gives insight into the relationship of the performance factors of the decision problems and their associated function problems. We discover that peak algorithmic cost is not necessarily at the phase transition and also not necessarily at the cross-over point. With the Bounded SAT problems, we discover a discover a new type of emergence for phase transitions. With the Generalized SAT problems we develop a uniform approach for determining upper bounds that yields tighter bounds than the previously reported uniform technique.