Towards backbone computing: a greedy-whitening based approach.(English)Zbl 1462.68177

Summary: 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{BL}}_\downharpoonright (\Phi)$$. Backbone computing is accelerated since SAT testings of literals in $$\overline{\mathsf{BL}}_\downharpoonright (\Phi)$$ are saved. The second step is a Whitening-based algorithm with two heuristic strategies which computes an approximation set of backbone $$\widehat{\mathsf{BL}} (\Phi)$$. Backbone computing is accelerated since more backbone are found at an early stage of the computing by testing the literals in $$\widehat{\mathsf{BL}} (\Phi)$$ 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.

MSC:

 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Walksat; BG-WalkSAT; MiniSat; DIMACS
Full Text:

References:

 [1] A. Belov and J. Marques-Silva, Accelerating MUS extraction with recursive model rotation, in:Formal Methods in Computer-Aided Design (FMCAD), 2011. [2] G. Carpaneto, M. Dell’Amico and P. Toth, Exact solution of large-scale, asymmetric traveling salesman problems,ACM Transactions on Mathematical Software (TOMS)(1995). [3] S. Climer and W. Zhang, Searching for backbones and fat: A limit-crossing approach with applications, in:Proceedings of the Eighteenth National Conference on Artificial Intelligence (AAAI-02) /Proceedings of the Fourteenth Innovative Applications of Artificial Intelligence Conference on Artificial Intelligence (IAAI-02), 2002. [4] J. Culberson and I.P. Gent, Frozen development in graph coloring,Theoretical Computer Science(2001). · Zbl 0983.68145 [5] O. Dubois and G. Dequen, A backbone-search heuristic for efficient solving of hard 3-SAT formulae, in:Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001. [6] N. Eén and N. Sförensson, An extensible SAT-solver, in:International Conference on Theory and Applications of Satisfiability Testing, 2003. [7] M.R. Garey and D.S. Johnson,A Guide to the Theory of NPCompleteness, WH Freemann, New York, 1979. [8] I.P. Gent and T. Walsh, The SAT phase transition, in:Proceedings of European Association for Artificial Intelligence (ECAI), 1994. [9] P. Giorgio, On local equilibrium equations for clustering states, Technique Report cs.cc/0212047, 2003. [10] M. Janota, SAT solving in interactive configuration, 2010. [11] M. Janota, I. Lynce and J. Marques-Silva, Experimental analysis of backbone computation algorithms, in:International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA), 2012. · Zbl 1373.68379 [12] M. Janota, I. Lynce and J. Marques-Silva, Algorithms for computing backbones of propositional formulae,AI Communications(2015). · Zbl 1373.68379 [13] A. Kaiser and W. Kühlin, Detecting inadmissible and necessary variables in large propositional formulae, University of Siena, 2001. [14] P. Kilby, J. Slaney and T. Walsh, The backbone of the travelling salesperson, in:Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI-05), 2005. [15] J. Marques-Silva, M. Janota and I. Lynce, On computing backbones of propositional theories, in:Proceedings of European Association for Artificial Intelligence (ECAI), 2010. · Zbl 1211.68389 [16] J. Marques-Silva and I. Lynce, On improving MUS extraction algorithms, in:International Conference on Theory and Applications of Satisfiability Testing, 2011. · Zbl 1330.68273 [17] M.E.B. Menaı, A two-phase backbone-based search heuristic for partial MAX-SAT - An initial investigation, in:International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems, 2005. [18] M.E.B. Menaı, A backbone-based co-evolutionary heuristic for partial MAX-SAT, in:International Conference on Artificial Evolution (Evolution Artificielle), 2005. [19] C. Mencıa, A. Previti and J. Marques-Silva, Literal-based MCS extraction, in:Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-15), 2015. [20] R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman and L. Troyansky, Determining computational complexity from characteristic phase transitions,Nature(1999). · Zbl 1369.68244 [21] A. Montanari, F. Ricci-Tersenghi and G. Semerjian, Solving constraint satisfaction problems through belief propagationguided decimation, arXiv preprint, 2007,arXiv:0709.1667. [22] B. Selman, H. Kautz and B. Cohen, Local search strategies for satisfiability testing, in:Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 1993. · Zbl 0864.90093 [23] T. Walsh and J. Slaney, Backbones in optimization and approximation, in:Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001. [24] W. Zhang and M. Looks, A novel local search algorithm for the traveling salesman problem that exploits backbones, in:Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI-05), 2005. [25] W. Zhang, A. Rangan and M. Looks, Backbone guided local search for maximum satisfiability, in:Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI-03), 2003. [26] C.S. Zhu, G. Weissenbacher and S. Malik, Post-silicon fault
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.