"Boolean Satisfiability and Phase-Transition Phenomena"
Boolean Satisfiability (SAT) is a fundamental problem in many diverse areas across computer science such as artificial intelligence, formal verification, and bioinformatics. Despite the famous theoretical (conjectured) difficulty of SAT, modern tools known as "SAT solvers" can successfully handle industrial inputs with millions of variables. Understanding the practical runtime of SAT solvers is an area of active research.
Recently, the performance of SAT solvers has been studied by analyzing their behavior on random inputs, sampled from well-defined probability distributions. For certain special input distributions, small changes in the distribution dramatically affect the runtime of the SAT solver (or other properties, e.g. the probability that a sampled input has a solution). These dramatic changes are called "Phase-Transitions". Although phase-transitions are readily apparent experimentally, in most cases we are unable to prove theoretically that the phase-transition truly exists.
In this talk, I will introduce SAT and discuss prior-work on phase-transition phenomena. I will then introduce a new distribution of random inputs (motivated by the problem of approximate counting), prove that a phase-transition exists in the satisfiability of this new distribution, and show experimental evidence for the shape of the phase-transition.