                     Search       Algorithms for computing backbones of propositional formulae
Janota M., Lynce I., Marques-Silva J.  AI Communications 28 (2): 161-177, 2015. Type: Article Date Reviewed: Oct 27 2016        The backbone (also called “necessary variables” or “fixed assignments”) of a propositional formula φ is the set of literals that are true in all models of the formula. Put another way, the backbone is the intersection of all implicants of φ. Since SAT is NP-complete, deciding if a given literal is in the backbone is co-NP-complete, and computing the backbone is NP-equivalent. Nevertheless, we should no more give up on computing the backbone than we give up on the general SAT problem. The authors present various known algorithms for computing the backbone, either by crossing out literals that don’t occur in all implications (Algorithm 1), or by adding x if φ ∪ x is unsatisfiable (Algorithm 2), or a combination (Algorithms 3, 4). They bound the number of calls to SAT that these algorithms make, but point out that, while Algorithm 4 does well on this measure, it performs badly in practice due to generating difficult SAT problems. Prior measurements have shown Algorithm 3 to be the best. Their Algorithm 5 sits partway between Algorithms 3 and 4, negating a chunk of K literals, whereas Algorithm 3 negates one, and Algorithm 4 as many as possible. If we assume that our SAT algorithm can return an “UNSAT core” ψ, that is, a subset of φ that is still unsatisfiable, then we may be able to use this. Of course, the solver might return the whole of φ, and solvers do not guarantee that φ is minimal, so the authors have to allow for the case when ψ is unhelpful. This gives Algorithm 6, a variant of Algorithm 4 using ψ, and then a chunked variant, Algorithm 7, analogous to Algorithm 5. Using ψ in Algorithm 3 doesn’t change the algorithm. So what should K be? Increasing K gives fewer, harder, SAT calls. The authors experiment, using MiniSAT2.2 (with its incremental interface) as the underlying solver. K = 30 or K = 100 allows Algorithm 5 to solve 667 problems, rather than Algorithm 3’s 666, but Algorithm 3 is faster more often (282 times rather than 232 or 200, but being within one second of the fastest is also deemed to be a win). Algorithm 7 with K = 100 solves most problems (718), but K = 30 is fastest slightly more often (434 versus 431). The conclusion is that using an UNSAT core definitely helps, but chunking is required as well. Reviewer:  J. H. Davenport Review #: CR144878 (1702-0160)           Would you recommend this review?  yes  no          E-Mail This  Printer-Friendly                Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2021 ThinkLoud, Inc.         