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.

Clean Citation Style 002

{ "authors" : [{ "lastname":"Bläsius" , "initial":"T" , "url":"https://hpi.de/friedrich/publications/people/thomas-blaesius.html" , "mail":"thomas.blasius(at)hpi.de" }, { "lastname":"Casel" , "initial":"K" , "url":"https://hpi.de/friedrich/publications/people/katrin-casel.html" , "mail":"katrin.casel(at)hpi.de" }, { "lastname":"Chauhan" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/ankit-chauhan.html" , "mail":"ankit.chauhan(at)hpi.de" }, { "lastname":"Cohen" , "initial":"S" , "url":"https://hpi.de/friedrich/publications/people/sarel-cohen.html" , "mail":"sarel.cohen(at)hpi.de" }, { "lastname":"Cseh" , "initial":"�" , "url":"https://hpi.de/friedrich/publications/people/agnes-cseh.html" , "mail":"agnes.cseh(at)hpi.de" }, { "lastname":"Doskoč" , "initial":"V" , "url":"https://hpi.de/friedrich/publications/people/vanja-doskoc.html" , "mail":"vanja.doskoc(at)hpi.de" }, { "lastname":"Elijazyfer" , "initial":"Z" , "url":"https://hpi.de/friedrich/people/ziena-elijazyfer.html" , "mail":"ziena.elijazyfer(at)hpi.de" }, { "lastname":"Fischbeck" , "initial":"P" , "url":"https://hpi.de/friedrich/publications/people/philipp-fischbeck.html" , "mail":"philipp.fischbeck(at)hpi.de" }, { "lastname":"Friedrich" , "initial":"T" , "url":"https://hpi.de/friedrich/publications/people/tobias-friedrich.html" , "mail":"friedrich(at)hpi.de" }, { "lastname":"Göbel" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/andreas-goebel.html" , "mail":"andreas.goebel(at)hpi.de" }, { "lastname":"Issac" , "initial":"D" , "url":"https://hpi.de/friedrich/publications/people/davis-issac.html" , "mail":"davis.issac(at)hpi.de" }, { "lastname":"Katzmann" , "initial":"M" , "url":"https://hpi.de/friedrich/publications/people/maximilian-katzmann.html" , "mail":"maximilian.katzmann(at)hpi.de" }, { "lastname":"Khazraei" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/ardalan-khazraei.html" , "mail":"ardalan.khazraei(at)hpi.de" }, { "lastname":"Kötzing" , "initial":"T" , "url":"https://hpi.de/friedrich/publications/people/timo-koetzing.html" , "mail":"timo.koetzing(at)hpi.de" }, { "lastname":"Krejca" , "initial":"M" , "url":"https://hpi.de/friedrich/publications/people/martin-krejca.html" , "mail":"martin.krejca(at)hpi.de" }, { "lastname":"Krogmann" , "initial":"S" , "url":"https://hpi.de/friedrich/publications/people/simon-krogmann.html" , "mail":"simon.krogmann(at)hpi.de" }, { "lastname":"Krohmer" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/anton-krohmer.html" , "mail":"none" }, { "lastname":"Kumar" , "initial":"N" , "url":"https://hpi.de/friedrich/publications/people/nikhil-kumar.html" , "mail":"nikhil.kumar(at)hpi.de" }, { "lastname":"Lagodzinski" , "initial":"G" , "url":"https://hpi.de/friedrich/publications/people/gregor-lagodzinski.html" , "mail":"gregor.lagodzinski(at)hpi.de" }, { "lastname":"Lenzner" , "initial":"P" , "url":"https://hpi.de/friedrich/publications/people/pascal-lenzner.html" , "mail":"pascal.lenzner(at)hpi.de" }, { "lastname":"Melnichenko" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/anna-melnichenko.html" , "mail":"anna.melnichenko(at)hpi.de" }, { "lastname":"Molitor" , "initial":"L" , "url":"https://hpi.de/friedrich/publications/people/louise-molitor.html" , "mail":"louise.molitor(at)hpi.de" }, { "lastname":"Neubert" , "initial":"S" , "url":"https://hpi.de/friedrich/publications/people/stefan-neubert.html" , "mail":"stefan.neubert(at)hpi.de" }, { "lastname":"Pappik" , "initial":"M" , "url":"https://hpi.de/friedrich/publications/people/marcus-pappik.html" , "mail":"marcus.pappik(at)hpi.de" }, { "lastname":"Quinzan" , "initial":"F" , "url":"https://hpi.de/friedrich/publications/people/francesco-quinzan.html" , "mail":"francesco.quinzan(at)hpi.de" }, { "lastname":"Rizzo" , "initial":"M" , "url":"https://hpi.de/friedrich/publications/people/manuel-rizzo.html" , "mail":"manuel.rizzo(at)hpi.de" }, { "lastname":"Rothenberger" , "initial":"R" , "url":"https://hpi.de/friedrich/publications/people/ralf-rothenberger.html" , "mail":"ralf.rothenberger(at)hpi.de" }, { "lastname":"Schirneck" , "initial":"M" , "url":"https://hpi.de/friedrich/publications/people/martin-schirneck.html" , "mail":"martin.schirneck(at)hpi.de" }, { "lastname":"Seidel" , "initial":"K" , "url":"https://hpi.de/friedrich/publications/people/karen-seidel.html" , "mail":"karen.seidel(at)hpi.de" }, { "lastname":"Sutton" , "initial":"A" , "url":"https://hpi.de/friedrich/publications/people/andrew-m-sutton.html" , "mail":"none" }, { "lastname":"Weyand" , "initial":"C" , "url":"https://hpi.de/friedrich/publications/people/christopher-weyand.html" , "mail":"none" }]}

$Sharpness of the Satisfiability Threshold for Non-Uniform Random $k$-SAT.$

Friedrich, Tobias; Rothenberger, Ralf Sharpness of the Satisfiability Threshold for Non-Uniform Random $k$-SAT.International Joint Conference on Artificial Intelligence (IJCAI) 2019: 6151–6155

[ Abstract ] [ BibTeX ] [ URL ] [ DOI ] [ Download ]

Friedrich, Tobias; Rothenberger, Ralf The Satisfiability Threshold for Non-Uniform Random 2-SATInternational Colloquium on Automata, Languages and Programming (ICALP) 2019: 61:1–61:14

[ Abstract ] [ BibTeX ] [ URL ] [ DOI ] [ Download ]

Bläsius, Thomas; Friedrich, Tobias; Sutton, Andrew M. On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase TransitionTools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019: 117–134

[ Abstract ] [ BibTeX ] [ URL ] [ DOI ] [ Download ]

@inproceedings{blasius2019empirical,
  abstract = {The hardness of formulas at the solubility phase transition of random propositional satisfiability (SAT) has been intensely studied for decades both empirically and theoretically. Solvers based on stochastic local search (SLS) appear to scale very well at the critical threshold, while complete backtracking solvers exhibit exponential scaling. On industrial SAT instances, this phenomenon is inverted: backtracking solvers can tackle large industrial problems, where SLS-based solvers appear to stall. Industrial instances exhibit sharply different structure than uniform random instances. Among many other properties, they are often heterogeneous in the sense that some variables appear in many while others appear in only few clauses. We conjecture that the heterogeneity of SAT formulas alone already contributes to the trade-off in performance between SLS solvers and complete backtracking solvers. We empirically determine how the run time of SLS vs. backtracking solvers depends on the heterogeneity of the input, which is controlled by drawing variables according to a scale-free distribution. Our experiments reveal that the efficiency of complete solvers at the phase transition is strongly related to the heterogeneity of the degree distribution. We report results that suggest the depth of satisfying assignments in complete search trees is influenced by the level of heterogeneity as measured by a power-law exponent. We also find that incomplete SLS solvers, which scale well on uniform instances, are not affected by heterogeneity. The main contribution of this paper utilizes the scale-free random 3-SAT model to isolate heterogeneity as an important factor in the scaling discrepancy between complete and SLS solvers at the uniform phase transition found in previous works.},
  author = {Bläsius, Thomas and Friedrich, Tobias and Sutton, Andrew M.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  keywords = {andrewmsutton scalefree_sat tacas thomasblaesius tobiasfriedrich year2019},
  pages = {117-134},
  title = {On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition},
  year = 2019
}

Friedrich, Tobias; Rothenberger, Ralf Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SATTheory and Applications of Satisfiability Testing (SAT) 2018: 273–291

Best Paper Award

[ Abstract ] [ BibTeX ] [ URL ] [ DOI ] [ Download ]

Friedrich, Tobias; Krohmer, Anton; Rothenberger, Ralf; Sauerwald, Thomas; Sutton, Andrew M. Bounds on the Satisfiability Threshold for Power Law Distributed Random SATEuropean Symposium on Algorithms (ESA) 2017: 37:1–37:15

[ Abstract ] [ BibTeX ] [ URL ] [ DOI ] [ Download ]

Friedrich, Tobias; Krohmer, Anton; Rothenberger, Ralf; Sutton, Andrew M. Phase Transitions for Scale-Free SAT FormulasConference on Artificial Intelligence (AAAI) 2017: 3893–3899

[ Abstract ] [ BibTeX ] [ URL ] [ Download ]

Scale-Free Satisfiability

Description

Studying Industrial Instances

Analyzing models for industrial instances

Codebase

Publications

Algorithm Engineering

News

13.09.2024 | Best Paper awarded at IPEC

11.09.2024 | PhD awarded to Philipp Fischbeck

05.09.2024 | Two Papers accepted at RANDOM and ESA

01.08.2024 | PhD awarded to Gregor Lagodzinski

17.07.2024 | Two Papers accepted at FOCS and PPSN

31.05.2024 | Two Papers accepted at SAND and IWOCA

Contact

Apply