Advertisement

Constraints

, Volume 21, Issue 2, pp 277–302 | Cite as

Quantified maximum satisfiability

  • Alexey IgnatievEmail author
  • Mikoláš Janota
  • Joao Marques-Silva
Article
First Online:

Abstract

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.

Keywords

Quantified Boolean formula Optimization SAT MaxSAT Smallest MUS/MES 
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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.
  3. 3.
    Ansótegui, C., Bonet, M.L., & Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In SAT (pp. 427–440).Google Scholar
  4. 4.
    Ansótegui, C., Bonet, M.L., & Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In AAAI. Google Scholar
  5. 5.
    Ansótegui, C., Bonet, M.L., & Levy, J. (2013). SAT-based MaxSAT algorithms. Artificial Intelligence, 196, 77–105.CrossRefMathSciNetzbMATHGoogle Scholar
  6. 6.
    Ansotegui, C., Gomes, C.P., & Selman, B. (2005). The Achilles’ heel of QBF. In AAAI (pp. 275–281).Google Scholar
  7. 7.
    Bailey, J., & Stuckey, P.J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL (pp. 174–186).Google Scholar
  8. 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).Google Scholar
  9. 9.
    Balabanov, V., & Jiang, J.H.R. (2012). Unified QBF certification and its applications. Formal Methods in System Design, 41(1), 45–65.CrossRefzbMATHGoogle Scholar
  10. 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.Google Scholar
  11. 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.Google Scholar
  12. 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.CrossRefMathSciNetzbMATHGoogle Scholar
  13. 13.
    Belov, A., Lynce, I., & Marques-Silva, J. (2012). Towards efficient MUS extraction. AI Communication, 25(2), 97–116.MathSciNetzbMATHGoogle Scholar
  14. 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.
  15. 15.
    Benedetti, M., Lallouet, A., & Vautard, J. (2008). Quantified constraint optimization. In CP (pp. 463–477).Google Scholar
  16. 16.
    Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2-3), 59–6.Google Scholar
  17. 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.CrossRefzbMATHGoogle Scholar
  18. 18.
    Chen, H., Janota, M., & Marques-Silva, J. (2012). QBF-based Boolean function bi-decomposition. In DATE (pp. 816–819).Google Scholar
  19. 19.
    Chen, H., & Pál, M. (2004). Optimization, games, and quantified constraint satisfaction. In Mathematical foundations of computer science (pp. 239–250).Google Scholar
  20. 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.CrossRefMathSciNetGoogle Scholar
  21. 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.Google Scholar
  22. 22.
    Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In SAT (pp. 502–518).Google Scholar
  23. 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.Google Scholar
  24. 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.Google Scholar
  25. 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.Google Scholar
  26. 26.
    Goultiaeva, A., & Bacchus, F. (2010). Exploiting QBF duality on a circuit representation. AAAI.Google Scholar
  27. 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.
  28. 28.
    Goultiaeva, A., Seidl, M., & Biere, A. (2013). Bridging the gap between dual propagation and CNF-based QBF solving. In DATE (pp. 811–814).Google Scholar
  29. 29.
    Gupta, A. (2006). Learning abstractions for model checking, Ph.D. thesis, Carnegie Mellon University.Google Scholar
  30. 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.CrossRefGoogle Scholar
  31. 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.Google Scholar
  32. 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).Google Scholar
  33. 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.Google Scholar
  34. 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.
  35. 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.
  36. 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.Google Scholar
  37. 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.Google Scholar
  38. 38.
    Janota, M., & Marques-Silva, J. (2011). Abstraction-based algorithm for 2QBF. In SAT (pp. 230–244).Google Scholar
  39. 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.Google Scholar
  40. 40.
    Kleine Büning, H., Karpinski, M., & Flögel, A. (1995). Resolution for quantified Boolean formulas. Information and Computation, 117(1), 12–18.CrossRefMathSciNetzbMATHGoogle Scholar
  41. 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.CrossRefMathSciNetzbMATHGoogle Scholar
  42. 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.
  43. 43.
    Kullmann, O. (2011). Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure. Fundamental and Information, 109(1), 83–119.MathSciNetzbMATHGoogle Scholar
  44. 44.
    Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203–232.CrossRefMathSciNetzbMATHGoogle Scholar
  45. 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.CrossRefMathSciNetzbMATHGoogle Scholar
  46. 46.
    Liffiton, M.H., & Sakallah, K.A. (2005). On finding all minimally unsatisfiable subformulas. In SAT (pp. 173–186).Google Scholar
  47. 47.
    Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal of Automated Reasoning, 40(1), 1–33.CrossRefMathSciNetzbMATHGoogle Scholar
  48. 48.
    Lonsing, F., & Egly, U. (2014). Incremental QBF solving. In CP (pp. 514–530).Google Scholar
  49. 49.
    Lynce, I., & Marques-Silva, J.P. (2004). On computing minimum unsatisfiable cores. In SAT.Google Scholar
  50. 50.
    Manquinho, V.M., Marques-Silva, J., & Planes, J. (2009). Algorithms for weighted Boolean optimization. In SAT (pp. 495–508).Google Scholar
  51. 51.
    Marques-Silva, J. (2010). Minimal unsatisfiability: models, algorithms and applications (invited paper). In ISMVL (pp. 9–14). IEEE Computer Society.Google Scholar
  52. 52.
    Marques-Silva, J., Heras, F., Janota, M., Previti, A., & Belov, A. (2013). On computing minimal correction subsets. In IJCAI.Google Scholar
  53. 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).Google Scholar
  54. 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. 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.CrossRefMathSciNetGoogle Scholar
  56. 56.
    Narodytska, N., & Bacchus, F. (2014). Maximum satisfiability using core-guided MaxSAT resolution. In AAAI (pp. 2717–2723).Google Scholar
  57. 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.Google Scholar
  58. 58.
    Nöhrer, A., Biere, A., & Egyed, A. (2012). Managing SAT inconsistencies with HUMUS. In VAMOS (pp. 83–91).Google Scholar
  59. 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.CrossRefMathSciNetzbMATHGoogle Scholar
  60. 60.
    Reimer, S., Sauer, M., Marin, P., & Becker, B. (2014). QBF with soft variables. ECEASST 70.Google Scholar
  61. 61.
    Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57–95.CrossRefMathSciNetzbMATHGoogle Scholar
  62. 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.Google Scholar
  63. 63.
    Ryvchin, V., & Strichman, O. (2011). Faster extraction of high-level minimal unsatisfiable cores. In SAT (pp. 174–187).Google Scholar
  64. 64.
    Schaefer, M., & Umans, C. (2002). Completeness in the polynomial-time hierarchy: a compendium. SIGACT News, 33(3), 32–49.CrossRefGoogle Scholar
  65. 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.Google Scholar
  66. 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. 67.
    Stuckey, P.J., Sulzmann, M., & Wazny, J. (2003). Interactive type debugging in Haskell. In ACM SIGPLAN workshop on Haskell (pp. 72–83). ACM.Google Scholar
  68. 68.
    Tseitin, G.S. (1968). On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115–125.Google Scholar
  69. 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.Google Scholar
  70. 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).Google Scholar
  71. 71.
    Zhang, J., Li, S., & Shen, S. (2006). Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In AUS-AI (pp. 847–856).Google Scholar
  72. 72.
    Zhang, L. (2006). Solving QBF by combining conjunctive and disjunctive normal forms. In AAAI (pp. 143–150).Google Scholar
  73. 73.
    Zhang, L., & Malik, S. (2002). Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD (pp. 442–449).Google Scholar
  74. 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.Google Scholar

Copyright information

© Springer Science+Business Media New York 2015

Authors and Affiliations

  • Alexey Ignatiev
    • 1
    • 2
    Email author
  • Mikoláš Janota
    • 1
  • Joao Marques-Silva
    • 1
    • 3
  1. 1.INESC-ID, IST, University of LisbonLisbonPortugal
  2. 2.ISDCT SB RASIrkutskRussia
  3. 3.University College DublinDublinIreland

Personalised recommendations

Cite article

Buy options