KIT | KIT-Bibliothek | Impressum | Datenschutz

The impact of heterogeneity and geometry on the proof complexity of random satisfiability

Bläsius, Thomas ORCID iD icon 1; Friedrich, Tobias; Friedrich, Tobias; Goebel, Andreas; Göbel, Andreas
1 Institut für Theoretische Informatik (ITI), Karlsruher Institut für Technologie (KIT)

Abstract:

Satisfiability is considered the canonical NP-complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms can solve large-scale industrial SAT instances very efficiently. This disparity between theory and practice is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two characteristic properties seem to be prevalent in the majority of real-world SAT instances, heterogeneous degree distribution and locality. To understand the impact of these two properties on SAT, we study the proof complexity of random -SAT models that allow to control heterogeneity and locality. Our findings show that heterogeneity alone does not make SAT easy as heterogeneous random -SAT instances have superpolynomial resolution size. This implies intractability of these instances for modern SAT-solvers. In contrast, modeling locality with underlying geometry leads to small unsatisfiable subformulas, which can be found within polynomial time.


Verlagsausgabe §
DOI: 10.5445/IR/1000161241
Veröffentlicht am 08.08.2023
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Zeitschriftenaufsatz
Publikationsmonat/-jahr 12.2023
Sprache Englisch
Identifikator ISSN: 1042-9832, 1098-2418
KITopen-ID: 1000161241
Erschienen in Random Structures & Algorithms
Verlag John Wiley and Sons
Band 63
Heft 4
Seiten 885–941
Vorab online veröffentlicht am 28.06.2023
Nachgewiesen in Web of Science
Dimensions
Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page