Nils Froleyks, Emily Zhengqi Yu, Armin Biere,
"BIG Backbones"
, in Nadel, Alexander Rozier, Kristin Yvonne: Proceedings of the 23rd Conference on Formal Methods inComputer-Aided Design FMCAD 2023, Serie Conference Series: Formal Methods in Computer-A on Formal Methods inComputer-Aided Design FMCAD 2023, TU Wien Academic Press, Seite(n) 162-167, 10-2023, ISBN: 978-3-85448-060-0
Original Titel:
BIG Backbones
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of the 23rd Conference on Formal Methods inComputer-Aided Design FMCAD 2023
Original Kurzfassung:
The backbone of a satisfiable formula is the set ofliterals that hold true in every model. In this paper we introduceSingle Unit Resolution Backbone (SURB) which names both apolynomial-time algorithm for backbone extraction and a class ofpropositional formulas on which it is complete. We show that thisclass is a superset of the polynomial-time solvable SLUR formulas.The presented algorithm meets a lower bound on time complexity underthe strong exponential-time hypothesis. As a second contribution, wepresent a version that operates on the binary implication graph(BIG) and implement it as a preprocessor in the recently introducedbackbone extractor CadiBack. Experiments on a large number of SATcompetition benchmarks show that our implementation results infaster BIG backbone extraction by an order of magnitude.Additionally, incorporating it as a preprocessor enables CadiBack toidentify up to four times as many backbone literals early on.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
TU Wien Academic Press
Serie:
Conference Series: Formal Methods in Computer-A on Formal Methods inComputer-Aided Design FMCAD 2023
Forschungs-