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.