Hasso-Plattner-Institut
Prof. Dr. Tobias Friedrich
  
 

Scale-Free Satisfiability

This site provides an overview over the research project on industrial satisfiability (SAT) instances and their relation to scale-free and other non-uniform SAT models of the HPI's Algorithm Engineering group led by Tobias Friedrich.

Description

Satisfiability of propositional formulas (SAT) stands at the core of many researched questions in theoretical computer science. Its computational hardness gave rise to many complexity-theoretical concepts, e.g. NP-hardness and lower bounds on algorithmic runtime via the (Strong) Exponential Time Hypothesis. Additionally, it is used to model practical problems such as bounded model checking, hardware and software verification, automated planning and scheduling, and circuit design. Such instances that originate from practical and industrial problems are also referred to as industrial instances. Despite SAT being NP-complete in theory, even large industrial instances with millions of variables can often be solved very efficiently by modern SAT solvers. The structure of these industrial instances appears to allow a much faster processing than the theoretical worst-case.

In our research group we study this phenomenon in two ways. On the one hand, we study industrial instances and try to discover properties that might make them easier to solve. On the other hand, we try to incorporate such properties into random models. Instances generated with such models can than be analyzed rigorously regarding their structural properties and their computational hardness.

 

Studying Industrial Instances

Some families of industrial SAT instances share properties which can alse be found in complex real-world networks like community structure and a highly non-uniform distribution of clauses and variables. Finding out which other structural properties these instances have is the next step in trying to explain why they can be solved efficiently.

 

Analyzing models for industrial instances

The properties of industrial instances can be incorporated into random models. Non-uniform random k-SAT can be used to model different variable distributions that are found in real-world instances. In this model there are n Boolean variables, each of which has a certain probability. Then, m clauses are drawn independently at random. For each clause k different variables are drawn according to their distribution and then negated wit probability 1/2 independently. If the distribution we use is a power law, we also call the model power-law random k-SAT.

One property of this model we are interested in is the emergence of the satisfiability threshold. The satisfiability threshold is the number of clauses at which the probability to generate satisfiable formulas goes from one to zero. Such a threshold is called sharp if it approches a step function for growing n. Otherwise it is called coarse.

We showed upper and lower bounds on the position of the satisfiability threshold for power-law random k-SAT with k ≥ 3. For non-uniform random 2-SAT we determined for which distributions the threshold is sharp and for which it is coarse. For the regime of distributions with a sharp threshold we also determined the exact threshold position. For non-uniform random k-SAT we also gave sufficient conditions on the probability distribution for the threshold to be sharp if its asymptotic position is known already.

Codebase

We implemented a generator for the power-law random k-SAT model, the double power-law random SAT model, and the uniform random k-SAT model in C++. The first two models were proposed by Ansótegui et al. in the paper Towards industrial-like random SAT instances (IJCAI 2009). The code of the generator can be found here.

Publications

The following publications by our group are related to this project.

  • Friedrich, Tobias; Rothenberger, Ralf Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT. International Joint Conference on Artificial Intelligence (IJCAI) 2019
    Extended abstract.
     
  • Friedrich, Tobias; Rothenberger, Ralf The Satisfiability Threshold for Non-Uniform Random 2-SAT. International Colloquium on Automata, Languages and Programming (ICALP) 2019: 61:1-61:14
     
  • On the Empirical Time Com... - Download
    Bläsius, Thomas; Friedrich, Tobias; Sutton, Andrew M. On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019: 117-134
     
  • Sharpness of the Satisfia... - Download
    Friedrich, Tobias; Rothenberger, Ralf Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT. Theory and Applications of Satisfiability Testing (SAT) 2018: 273--291
    Best Paper Award
     
  • Bounds on the Satisfiabil... - Download
    Friedrich, Tobias; Krohmer, Anton; Rothenberger, Ralf; Sauerwald, Thomas; Sutton, Andrew M. Bounds on the Satisfiability Threshold for Power Law Distributed Random SAT. European Symposium on Algorithms (ESA) 2017: 37:1-37:15
     
  • Phase Transitions for Sca... - Download
    Friedrich, Tobias; Krohmer, Anton; Rothenberger, Ralf; Sutton, Andrew M. Phase Transitions for Scale-Free SAT Formulas. Conference on Artificial Intelligence (AAAI) 2017: 3893-3899