Towards backbone computing: A Greedy-Whitening based approach

Abstract

Backbone is the set of literals that are true in all formula’s models. Computing a part of backbone efficiently could guide the following searching in SAT solving and accelerate the process, which is widely used in fault localization, product configuration, and formula simplification. Specifically, iterative SAT testings among literals are the most time consumer in backbone computing. We propose a Greedy-Whitening based algorithm in order to accelerate backbone computing. On the one hand, we try to reduce the number of SAT testings as many as possible. On the other hand, we make every inventible SAT testing more efficient. The proposed approach consists of three steps. The first step is a Greedy-based algorithm which computes an under-approximation of non-backbone ${\overline{\mathsf{\text{BL}}}}_{\downharpoonright }\mathrm{(}\mathrm{\Phi }\mathrm{)}$ . Backbone computing is accelerated since SAT testings of literals in ${\overline{\mathsf{\text{BL}}}}_{\downharpoonright }\mathrm{(}\mathrm{\Phi }\mathrm{)}$ are saved. The second step is a Whitening-based algorithm with two heuristic strategies which computes an approximation set of backbone $\widehat{\mathsf{\text{BL}}}\mathrm{(}\mathrm{\Phi }\mathrm{)}$ . Backbone computing is accelerated since more backbone are found at an early stage of the computing by testing the literals in $\widehat{\mathsf{\text{BL}}}\mathrm{(}\mathrm{\Phi }\mathrm{)}$ first, which makes every individual SAT testing more efficient. The exact backbone is computed in the third step which applies iterative backbone testing on the approximations. We implemented our approach in a tool Bone and conducted experiments on instances from Industrial tracks of SAT Competitions between 2002 and 2016. Empirical results show that Bone is more efficient in industrial and crafted formulas.