Prof. Dr. Tobias Friedrich

Masterproject Winter Term 2017 - A Realistic Model for Random Satisfiability

Personen: Prof. Dr. Tobias Friedrich, Dr. Thomas BläsiusDr. Andreas Göbel, Ralf Rothenberger
Links: Lehrveranstaltungen IT-Systems Engineering, Algorithm Engineering Moodle


Satisfiability (SAT) is the problem of deciding whether there is a satisfying assignment for a given Boolean formula in conjunctive normal form. SAT plays a central role in computer science,  not only for historical reasons – it was the first natural problem known to be NP-complete – but also because it has a wide range of applications in industry. SAT is used in theory as a starting point for reductions of NP-completeness, while efficient SAT solvers are used in industry by reducing other problems to SAT, as heuristic algorithms for industrial SAT instances can solve the problem very efficiently. An approach for explaining this difference between theory and practice is to consider a model for generating random SAT formulae that resemble industrial instances and study the properties of the instances generated by the model.

Purpose of the project

The purpose of this project is to identify the properties of industrial SAT instances that makes them tractable. Two properties have been observed in industrial SAT instances. The first property is that the degrees of the variables in an industrial SAT instance follow a scale-free distribution, where the degree of a variable of a SAT formula is the number of clauses thatcontain this variable. The second property is that the variables of an industrial SAT instance tend to cluster in communities, that is sets of variables tend to appear in the same clauses. The standard model for generating random SAT instances does not produce formulae that have these two properties. Random SAT models have been proposed that encompass either scale-free degree distribution or a high clustering coefficient, but none of these models seems provides insight on why SAT solversperform so well on real world instances. Inspired by recent models designed to approximate real world networks, we propose to study a new model for generating random SAT instances that potentially addresses both of these properties. Our model uses geometry to address the community structure and a measure of importance, in the form of variable weights, to address the power-law degree distribution.