TY - GEN
T1 - BIG Backbones
AU - Froleyks, Nils
AU - Yu, Zhengqi
AU - Biere, Armin
PY - 2023/10
Y1 - 2023/10
N2 - 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.
AB - 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.
UR - https://repositum.tuwien.at/handle/20.500.12708/188823
UR - https://www.scopus.com/pages/publications/85180376263
U2 - 10.34727/2023/isbn.978-3-85448-060-0_24
DO - 10.34727/2023/isbn.978-3-85448-060-0_24
M3 - Conference proceedings
SN - 978-3-85448-060-0
T3 - Conference Series: Formal Methods in Computer-A on Formal Methods inComputer-Aided Design FMCAD 2023
SP - 162
EP - 167
BT - Proceedings of the 23rd Conference on Formal Methods inComputer-Aided Design FMCAD 2023
A2 - Nadel, Alexander
A2 - Rozier, Kristin Yvonne
A2 - Hunt, Warren A.
A2 - Weissenbacher, Georg
PB - TU Wien Academic Press
ER -