access icon free Variable quality checking for backbone computation

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.

Inspec keywords: decidability; decision theory; optimisation; computability

Other keywords: propositional theory; Davis-Putnam-Logemann-Loveland-based satisfiability problem; variable quality checking; OTPV algorithm; BVQC algorithm; VQC strategy; decision hardness characterisation; performance improvement; backbone with the VQC algorithm; one test per variable algorithm; optimisation problems; backbone computation; backbone variable selection

Subjects: Formal logic; Programming and algorithm theory

References

    1. 1)
    2. 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. 186199.
    3. 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. 4)
      • 7. Biere, A.: ‘Picosat essentials’, J. Satisfiability Boolean Model. Comput., 2008, 4, (2-4), pp. 7597.
    5. 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. 1520.
    6. 6)
    7. 7)
      • 2. Janota, M., Lynce, I., Marques-Silva, J.: ‘Algorithms for computing backbones of propositional formulae’, AI Commun., 2015, 28, (2), pp. 161177.
    8. 8)
      • 10. Cai, S., Lin, J., Su, K.: ‘Two weighting local search for minimum vertex cover’. AAAI, Buenos Aires, Argentina, July 2015, pp. 11071113.
    9. 9)
    10. 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. 254259.
http://iet.metastore.ingenta.com/content/journals/10.1049/el.2016.1243
Loading

Related content

content/journals/10.1049/el.2016.1243
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading