Scale-Free Satisfiability

点击翻译按钮获取中文摘要

Boolean logic is the standard language to describe industrial decision problems coming from various domains like logistics and optimization. Solving these problems corresponds to finding a satisfying assignment to the Boolean variables of a given formula. This can be found very efficiently with industrial solvers for instances with millions of variables.This practical efficiency stands in contrast to the most classical result of theoretical computer science: the proven computational hardness of propositional satisfiability (SAT). The disparity between these results is due to the stark structural differences between worst-case formulas and those that appear in practical applications. To address this, the average-case behavior over random formulas was extensively studied in the last two decades. Most of this research assumes that variables appear uniformly at random. However, formulas drawn from a uniform distribution also have very different statistical structure than sets of industrial SAT instances. For example, industrial formulas often exhibit large fluctuations in variable occurrence.Thus it is one of the "grand challenges in SAT research" to generate synthetic instances that are more similar to real-world instances. This project will study non-uniform and scale-free distributions, which appear to resemble industrial SAT instances more closely. We want to determine which statistical properties make real-world SAT instances much easier to solve than theory can explain so far. We will develop the necessary mathematical machinery based on the probabilistic tools available for the analysis of large scale-free networks. A better understanding of the critical parameters will lead the way to more efficient and principled SAT solvers on industrial applications.