Hasso-Plattner-Institut
Prof. Dr. Tobias Friedrich
 

A Realistic Model for Random Satisfiability

Master Project - Winter 2017/18

Motivation

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.

Project Team

The Master Project is organized by the Algorithm Engineering Group. The following group members and students are participating:

Project Supervisor

Hasso Plattner Institute

Office: A-1.10
Tel.: +49 331 5509-410
E-Mail: Friedrich(at)hpi.de

Advisor

Chair for Algorithm Engineering
Hasso Plattner Institute

Office: A-1.4
Tel.: +49 331 5509-412
E-Mail: Thomas.Blaesius(at)hpi.de
Links: Homepage, Publications

Advisor

Chair for Algorithm Engineering
Hasso Plattner Institute

Offices: A-1.6
Tel.: +49 331 5509-424
E-Mail: Andreas.Goebel(at)hpi.de
Links: Homepage, Publications

Tobias Knöschke

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Tobias.Knoeschke(at)student.hpi.de

Simon Krogmann

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Simon.Krogmann(at)student.hpi.de

Dimitri Schmidt

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Dimitri.Schmidt(at)student.hpi.de

Sören Tietböhl

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Soeren.Tietboehl(at)student.hpi.de

Juliane Waack

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Juliane.Waack(at)student.hpi.de

Christopher Weyand

Participant

Chair for Algorithm Engineering
Hasso Plattner Institute

E-Mail: Christopher.Weyand(at)student.hpi.de