Quantified maximum satisfiability. (English) Zbl 1334.90075
Summary: In recent years, there have been significant improvements in algorithms both for Quantified Boolean Formulas (QBF) and for Maximum Satisfiability (MaxSAT). This paper studies an optimization extension of QBF and considers the problem in a quantified MaxSAT setting. More precisely, the general QMaxSAT problem is defined for QBFs with a set of soft clausal constraints and consists in finding the largest subset of the soft constraints such that the remaining QBF is true. Two approaches are investigated. One is based on relaxing the soft clauses and performing an iterative search on the cost function. The other approach, which is the main contribution of the paper, is inspired by recent work on MaxSAT, and exploits the iterative identification of unsatisfiable cores. The paper investigates the application of these approaches to the two concrete problems of computing smallest minimal unsatisfiable subformulas (SMUS) and smallest minimal equivalent subformulas (SMES), decision versions of which are well-known problems in the second level of the polynomial hierarchy. Experimental results, obtained on representative problem instances, indicate that the core-guided approach for the SMUS and SMES problems outperforms the use of iterative search over the values of the cost function. More significantly, the core-guided approach to SMUS also outperforms the state-of-the-art SMUS extractor Digger.
MSC:
| 90C09 | Boolean programming |
References:
| [1] | Andraus, Z.S., Liffiton, M.H., & Sakallah, K.A. (2006). Refinement strategies for verification methods based on datapath abstraction. In ASP-DAC (pp. 19-24). doi:10.1145/1118299.1118306. |
| [2] | Andraus, Z.S., Liffiton, M.H., & Sakallah, K.A. (2008). Reveal: a formal verification tool for verilog designs. In LPAR (pp. 343-352). doi:10.1007/978-3-540-89439-1_25. · Zbl 1182.68111 |
| [3] | Ansótegui, C., Bonet, M.L., & Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In SAT (pp. 427-440). · Zbl 1247.68242 |
| [4] | Ansótegui, C., Bonet, M.L., & Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In AAAI. · Zbl 1247.68242 |
| [5] | Ansótegui, C., Bonet, M.L., & Levy, J. (2013). SAT-based MaxSAT algorithms. Artificial Intelligence, 196, 77-105. · Zbl 1270.68265 · doi:10.1016/j.artint.2013.01.002 |
| [6] | Ansotegui, C., Gomes, C.P., & Selman, B. (2005). The Achilles’ heel of QBF. In AAAI (pp. 275-281). · Zbl 0828.68045 |
| [7] | Bailey, J., & Stuckey, P.J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL (pp. 174-186). · Zbl 1132.68736 |
| [8] | Balabanov, V., & Jiang, J.H.R. (2011). Resolution proofs and Skolem functions in QBF evaluation and applications. In G. Gopalakrishnan, S. Qadeer (Eds.), CAV (pp. 149-164). |
| [9] | Balabanov, V., & Jiang, J.H.R. (2012). Unified QBF certification and its applications. Formal Methods in System Design, 41(1), 45-65. · Zbl 1284.68516 · doi:10.1007/s10703-012-0152-6 |
| [10] | Balabanov, V., Widl, M., & Jiang, J.H.R. (2014). QBF resolution systems and their proof complexities. In C. Sinz, U. Egly (Eds.), SAT (pp. 154-169). Springer. · Zbl 1423.68406 |
| [11] | Belov, A., Janota, M., Lynce, I., & Marques-Silva, J. (2012). On computing minimal equivalent subformulas. In M. Milano (Ed.), CP (Vol. 7514, pp. 158-174). Springer. · Zbl 1405.68340 |
| [12] | Belov, A., Janota, M., Lynce, I., & Marques-Silva, J. (2014). Algorithms for computing minimal equivalent subformulas. Artificial Intelligence, 216, 309-326. doi:10.1016/j.artint.2014.07.011. · Zbl 1405.68340 · doi:10.1016/j.artint.2014.07.011 |
| [13] | Belov, A., Lynce, I., & Marques-Silva, J. (2012). Towards efficient MUS extraction. AI Communication, 25(2), 97-116. · Zbl 1248.68450 |
| [14] | Belov, A., Morgado, A., & Marques-Silva, J. (2013). SAT-based preprocessing for MaxSAT. In LPAR (pp. 96-111). doi:10.1007/978-3-642-45221-5_7. · Zbl 1406.68108 |
| [15] | Benedetti, M., Lallouet, A., & Vautard, J. (2008). Quantified constraint optimization. In CP (pp. 463-477). |
| [16] | Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2-3), 59-6. |
| [17] | Birnbaum, E., & Lozinskii, E.L. (2003). Consistent subsets of inconsistent systems: structure and behaviour. Journal of Experimental & Theoretical Artificial Intelligence, 15(1), 25-46. · Zbl 1025.68090 · doi:10.1080/0952813021000026795 |
| [18] | Chen, H., Janota, M., & Marques-Silva, J. (2012). QBF-based Boolean function bi-decomposition. In DATE (pp. 816-819). · Zbl 1317.90199 |
| [19] | Chen, H., & Pál, M. (2004). Optimization, games, and quantified constraint satisfaction. In Mathematical foundations of computer science (pp. 239-250). · Zbl 1096.90028 |
| [20] | Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. Journal of ACM, 50(5), 752-794. · Zbl 1325.68145 · doi:10.1145/876638.876643 |
| [21] | Condon, A., Feigenbaum, J., Lund, C., & Shor, P.W. (1995). Probabilistically checkable debate systems and nonapproximability of PSPACE-hard functions. Chicago Journal of Theoretical Computer Science, 1995. · Zbl 0924.68177 |
| [22] | Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In SAT (pp. 502-518). · Zbl 1204.68191 |
| [23] | Egly, U., Lonsing, F., & Widl, M. (2013). Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In K. L. McMillan, A. Middeldorp, A. Voronkov (Eds.), LPAR (Vol. 8312, pp. 291-308). Springer. · Zbl 1406.68106 |
| [24] | Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In A. Biere, C. P. Gomes (Eds.), SAT, lecture notes in computer science (Vol. 4121, pp. 252-265). Springer. · Zbl 1187.68540 |
| [25] | Goldberg, E.I., & Novikov, Y. (2003). Verification of proofs of unsatisfiability for CNF formulas. In DATE (pp. 10,886-10,891). IEEE Computer Society. · Zbl 0643.68122 |
| [26] | Goultiaeva, A., & Bacchus, F. (2010). Exploiting QBF duality on a circuit representation. AAAI. · Zbl 1306.68158 |
| [27] | Goultiaeva, A., & Bacchus, F. (2013). Recovering and utilizing partial duality in QBF. In SAT (pp. 83-99). doi:10.1007/978-3-642-39071-5_8. · Zbl 1390.68573 |
| [28] | Goultiaeva, A., Seidl, M., & Biere, A. (2013). Bridging the gap between dual propagation and CNF-based QBF solving. In DATE (pp. 811-814). |
| [29] | Gupta, A. (2006). Learning abstractions for model checking, Ph.D. thesis, Carnegie Mellon University. |
| [30] | Han, B., & Lee, S.J. (1999). Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics: Part B, 29(2), 281-286. · doi:10.1109/3477.752801 |
| [31] | Heras, F., Morgado, A., & Marques-Silva, J. (2011). Core-guided binary search algorithms for maximum satisfiability. In W. Burgard, D. Roth (Eds.), AAAI. AAAI Press. · Zbl 1273.68357 |
| [32] | Heule, M., Seidl, M., & Biere, A. (2014). A unified proof system for QBF preprocessing. In S. Demri, D. Kapur, C. Weidenbach (Eds.), IJCAR (Vol. 8562, pp. 91-106). · Zbl 1409.68257 |
| [33] | Ignatiev, A., Janota, M., & Marques-Silva, J. (2013). Quantified maximum satisfiability: A core-guided approach. In M. Järvisalo, A. Van Gelder (Eds.), SAT (Vol. 7962, pp. 250-266). Springer. · Zbl 1390.68598 |
| [34] | Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I., & Marques-Silva, J. (2014). Progression in maximum satisfiability. In ECAI (pp. 453-458). doi:10.3233/978-1-61499-419-0-453. · Zbl 1366.68266 |
| [35] | Jain, H., Kroening, D., Sharygina, N., & Clarke, E.M. (2005). Word level predicate abstraction and refinement for verifying RTL verilog. In DAC (pp. 445-450). doi:10.1145/1065579.1065697. · Zbl 1248.68450 |
| [36] | Janota, M., Grigore, R., & Marques-Silva, J. (2013). On QBF proofs and preprocessing. In K.L. McMillan, A. Middeldorp, A. Voronkov (Eds.), LPAR (Vol. 8312, pp. 473-489). Springer. · Zbl 1407.68454 |
| [37] | Janota, M., Klieber, W., Marques-Silva, J., & Clarke, E.M. (2012). Solving QBF with counterexample guided refinement. In A. Cimatti, R. Sebastiani (Eds.), SAT (Vol. 7317, pp. 114-128). Springer. · Zbl 1273.68178 |
| [38] | Janota, M., & Marques-Silva, J. (2011). Abstraction-based algorithm for 2QBF. In SAT (pp. 230-244). · Zbl 1330.68115 |
| [39] | Kleine Büning, H., & Bubeck, U. (2009). Theory of quantified Boolean formulas. In A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of satisfiability, frontiers in artificial intelligence and applications (Vol. 185, pp. 735-760). IOS Press. · Zbl 1247.68237 |
| [40] | Kleine Büning, H., Karpinski, M., & Flögel, A. (1995). Resolution for quantified Boolean formulas. Information and Computation, 117(1), 12-18. · Zbl 0828.68045 · doi:10.1006/inco.1995.1025 |
| [41] | Kleine Büning, H., Subramani, K., & Zhao, X. (2007). Boolean functions as models for quantified Boolean formulas. Journal of Automated Reasoning, 39(1), 49-75. · Zbl 1126.03015 · doi:10.1007/s10817-007-9067-0 |
| [42] | Klieber, W., Sapra, S., Gao, S., & Clarke, E.M. (2010). A non-prenex, non-clausal QBF solver with game-state learning. In SAT (pp. 128-142). doi:10.1007/978-3-642-14186-7_12. · Zbl 1306.68161 |
| [43] | Kullmann, O. (2011). Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure. Fundamental and Information, 109(1), 83-119. · Zbl 1242.68290 |
| [44] | Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203-232. · Zbl 1132.68736 · doi:10.1016/j.artint.2004.11.002 |
| [45] | Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., & Sakallah, K.A. (2009). A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints, 14(4), 415-442. · Zbl 1181.90291 · doi:10.1007/s10601-008-9058-8 |
| [46] | Liffiton, M.H., & Sakallah, K.A. (2005). On finding all minimally unsatisfiable subformulas. In SAT (pp. 173-186). · Zbl 1128.68473 |
| [47] | Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal of Automated Reasoning, 40(1), 1-33. · Zbl 1154.68510 · doi:10.1007/s10817-007-9084-z |
| [48] | Lonsing, F., & Egly, U. (2014). Incremental QBF solving. In CP (pp. 514-530). · Zbl 1434.68547 |
| [49] | Lynce, I., & Marques-Silva, J.P. (2004). On computing minimum unsatisfiable cores. In SAT. |
| [50] | Manquinho, V.M., Marques-Silva, J., & Planes, J. (2009). Algorithms for weighted Boolean optimization. In SAT (pp. 495-508). · Zbl 1247.68258 |
| [51] | Marques-Silva, J. (2010). Minimal unsatisfiability: models, algorithms and applications (invited paper). In ISMVL (pp. 9-14). IEEE Computer Society. |
| [52] | Marques-Silva, J., Heras, F., Janota, M., Previti, A., & Belov, A. (2013). On computing minimal correction subsets. In IJCAI. |
| [53] | Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J.P., & Sakallah, K.A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In SAT (pp. 467-474). · Zbl 1128.68477 |
| [54] | Morgado, A., Dodaro, C., & Marques-Silva, J. (2014). Core-guided MaxSAT with soft cardinality constraints. In CP (pp. 564-573). doi:10.1007/978-3-319-10428-7_41. |
| [55] | Morgado, A., Heras, F., Liffiton, M.H., Planes, J., & Marques-Silva, J. (2013). Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints, 18 (4), 478-534. · Zbl 1317.90199 · doi:10.1007/s10601-013-9146-2 |
| [56] | Narodytska, N., & Bacchus, F. (2014). Maximum satisfiability using core-guided MaxSAT resolution. In AAAI (pp. 2717-2723). |
| [57] | Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., & Biere, A. (2012). Resolution-based certificate extraction for QBF - (tool presentation). In A. Cimatti, R. Sebastiani (Eds.), SAT (Vol. 7317, pp. 430-435). Springer. |
| [58] | Nöhrer, A., Biere, A., & Egyed, A. (2012). Managing SAT inconsistencies with HUMUS. In VAMOS (pp. 83-91). |
| [59] | Plaisted, D.A., & Greenbaum, S. (1986). A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3), 293-304. doi:10.1016/S0747-7171(86)80028-1. · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1 |
| [60] | Reimer, S., Sauer, M., Marin, P., & Becker, B. (2014). QBF with soft variables. ECEASST 70. |
| [61] | Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57-95. · Zbl 0643.68122 · doi:10.1016/0004-3702(87)90062-2 |
| [62] | Roussel, O., & Manquinho, V. (2009). Pseudo-Boolean and cardinality constraints. In A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of satisfiability, frontiers in artificial intelligence and applications (Vol. 185, pp. 695-733). IOS Press. · Zbl 1183.68568 |
| [63] | Ryvchin, V., & Strichman, O. (2011). Faster extraction of high-level minimal unsatisfiable cores. In SAT (pp. 174-187). · Zbl 1331.68211 |
| [64] | Schaefer, M., & Umans, C. (2002). Completeness in the polynomial-time hierarchy: a compendium. SIGACT News, 33(3), 32-49. · doi:10.1145/582475.582484 |
| [65] | Sinz, C., Kaiser, A., & Küchlin, W. (2003). Formal methods for the validation of automotive product configuration data. AI EDAM, 17(1), 75-97. |
| [66] | Stuckey, P.J. (2013). There are no CNF problems. In SAT (pp. 19-21). doi:10.1007/978-3-642-39071-5_3. |
| [67] | Stuckey, P.J., Sulzmann, M., & Wazny, J. (2003). Interactive type debugging in Haskell. In ACM SIGPLAN workshop on Haskell (pp. 72-83). ACM. |
| [68] | Tseitin, G.S. (1968). On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115-125. · Zbl 1248.68450 |
| [69] | Van Gelder, A. (2012). Contributions to the theory of practical quantified Boolean formula solving. In M. Milano (Ed.), CP (Vol. 7514, pp. 647-663). Springer. · Zbl 1390.68585 |
| [70] | Yu, Y., & Malik, S. (2005). Validating the result of a quantified Boolean formula (QBF) solver: theory and practice. In ASP-DAC (pp. 1047-1051). · Zbl 1405.68340 |
| [71] | Zhang, J., Li, S., & Shen, S. (2006). Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In AUS-AI (pp. 847-856). |
| [72] | Zhang, L. (2006). Solving QBF by combining conjunctive and disjunctive normal forms. In AAAI (pp. 143-150). |
| [73] | Zhang, L., & Malik, S. (2002). Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD (pp. 442-449). · Zbl 0828.68045 |
| [74] | Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In DATE (pp. 10,880-10,885). IEEE Computer Society. · Zbl 0636.68119 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
