Variable quality checking for backbone computation
Yiyuan Wang, Dantong Ouyang, Liming Zhang · Electronics Letters · 2016
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.