Open AccessVariable quality checking for backbone computation
Author(s) -
Wang Yiyuan,
Ouyang Dantong,
Zhang Liming
Publication year - 2016
Publication title -
electronics letters
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.375
H-Index - 146
eISSN - 1350-911X
pISSN - 0013-5194
DOI - 10.1049/el.2016.1243
Subject(s) - variable (mathematics) , variable elimination , computation , solver , algorithm , quality (philosophy) , computer science , mathematics , chunking (psychology) , satisfiability , mathematical optimization , artificial intelligence , mathematical analysis , philosophy , epistemology , inference
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.