© The Institution of Engineering and Technology
Backbones of a propositional theory are those literals, whose assignments are always true in every satisfying assignment, and have been applied for characterising the hardness of decision and optimisation problems. A new strategy called variable quality checking (VQC) is proposed for backbone computation. The VQC strategy to check the variable quality is used to obtain from the level information of variables when a Davis-Putnam-Logemann-Loveland-based satisfiablity problem solver returns satisfiable, and then decide which variable is the next variable to be computed, i.e. to select the most likely or unlikely backbone variable, whereas the previous algorithms randomly select a variable to compute. Furthermore, we use the VQC strategy to improve an efficient backbone algorithm called OTPV (one test per variable) and design a new algorithm for backbone computation, called BVQC (backbone with the VQC). The VQC strategy can also improve the performance of state-of-the-art backbone algorithm core-based with chunking, which calls OTPV to test whether the remaining literals are in the backbone or not. Experimental results show that BVQC significantly outperforms OTPV and gains a 1.30 times on average speed-up, even up to one order of magnitude for some instances.
References
-
-
1)
-
4. Gao, J., Wang, J., Yin, M.: ‘Experimental analyses on phase transitions in compiling satisfiability problems’, Sci. Chin. Inf. Sci., 2015, 58, (3), pp. 1–11 (doi: 10.1007/s11432-014-5154-0).
-
2)
-
5. Zhang, J., Ma, F., Zhang, Z.: ‘Faulty interaction identification via constraint solving and optimization’. Theory and Applications of Satisfiability Testing, SAT, Trento, Italy, June 2012, pp. 186–199.
-
3)
-
9. Wang, Y., Cai, S., Yin, M.: ‘Two efficient local search algorithms for maximum weight clique problem’. AAAI, Phoenix, Arizona, USA, February 2016.
-
4)
-
7. Biere, A.: ‘Picosat essentials’, J. Satisfiability Boolean Model. Comput., 2008, 4, (2-4), pp. 75–97.
-
5)
-
1. Marques-Silva, J., Janota, M., Lynce, I.: ‘On computing backbones of propositional theories’. Proc. of the 2010 Conf. on ECAI, Lisbon, Portugal, August 2010, pp. 15–20.
-
6)
-
8. Jeroslow, R.G., Wang, J.: ‘Solving propositional satisfiability problems’, Ann. Math. Artif. Intell., 1990, 265, (1-4), pp. 167–187 (doi: 10.1007/BF01531077).
-
7)
-
2. Janota, M., Lynce, I., Marques-Silva, J.: ‘Algorithms for computing backbones of propositional formulae’, AI Commun., 2015, 28, (2), pp. 161–177.
-
8)
-
10. Cai, S., Lin, J., Su, K.: ‘Two weighting local search for minimum vertex cover’. AAAI, Buenos Aires, Argentina, July 2015, pp. 1107–1113.
-
9)
-
3. Xu, K., Li, W.: ‘Many hard examples in exact phase transitions’, Theor. Comput. Sci., 2006, 355, (3), pp. 291–302 (doi: 10.1016/j.tcs.2006.01.001).
-
10)
-
6. Slaney, J., Walsh, T.: ‘Backbones in optimization and approximation’. Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, USA, August 2001, pp. 254–259.
http://iet.metastore.ingenta.com/content/journals/10.1049/el.2016.1243
Related content
content/journals/10.1049/el.2016.1243
pub_keyword,iet_inspecKeyword,pub_concept
6
6