Advertisement

A Cube Distribution Approach to QBF Solving and Certificate Minimization

  • Li-Cheng Chen
  • Jie-Hong R. JiangEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11802)

Abstract

Quantified Boolean Formulas (QBFs) are powerful expressions to naturally and concisely encode many decision problems in computer science, such as robotic planning, hardware/software synthesis and verification, among others. Their effective solving and certificate (in terms of model and countermodel) generation play crucial roles to enable practical applications. In this work, we give a new view on QBF solving and certificate generation by the cube distribution interpretation. It provides a largely increased flexibility for QBF reasoning and allows compact certificate derivation with don’t cares. Through this interpretation, we develop a QBF solver based on the prior clause selection framework. Experimental results demonstrate the superiority of our solver in both solving performance and certificate size compared to other state-of-the-art solvers with certificate generation ability.

Keywords

Quantified Boolean formula Certificate Cube distribution 

Notes

Acknowledgment

The authors thank Mikolas Janota for providing the Qesto source code. This work was supported in part by the Ministry of Science and Technology of Taiwan under grants 105-2221-E-002-196-MY3, 105-2923-E-002-016-MY3, and 108-2221-E-002-144-MY3.

References

  1. 1.
    Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41, 45–65 (2012)CrossRefGoogle Scholar
  2. 2.
    Biere, A.: PicoSAT essentials. J. Satisfiability Boolean Model. Comput. 4, 75–97 (2008)zbMATHGoogle Scholar
  3. 3.
    Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101–115. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22438-6_10CrossRefGoogle Scholar
  4. 4.
    Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_5CrossRefGoogle Scholar
  5. 5.
    Dao, A.Q., et al.: Efficient computation of eco patch functions. In: Design Automation Conference (DAC), pp. 51:1–51:6 (2018)Google Scholar
  6. 6.
    Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408–414. Springer, Heidelberg (2005).  https://doi.org/10.1007/11499107_32CrossRefGoogle Scholar
  7. 7.
    Een, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-72788-0_26CrossRefzbMATHGoogle Scholar
  8. 8.
    Fazekas, K., Heule, M.J.H., Seidl, M., Biere, A.: Skolem function continuation for quantified boolean formulas. In: Gabmeyer, S., Johnsen, E.B. (eds.) TAP 2017. LNCS, vol. 10375, pp. 129–138. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-61467-0_8CrossRefGoogle Scholar
  9. 9.
    Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: International Symposium on Games, Automata, Logics, and Formal Verification (GandALF), pp. 88–102 (2018)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Automated Reasoning 58(1), 97–125 (2017)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 325–331 (2015)Google Scholar
  12. 12.
    Jiang, J.H.R., Lin, H.P., Hung, W.L.: Interpolating functions from large Boolean relations. In: International Conference on Computer-Aided Design (ICCAD), pp. 779–784 (2009)Google Scholar
  13. 13.
    Kontchakov, R., et al.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 836–841. AAAI Press (2009)Google Scholar
  14. 14.
    Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver (system description). J. Satisfiability Boolean Model. Comput. 7, 71–76 (2010)Google Scholar
  15. 15.
    Lonsing, F., Egly, U.: Depqbf 6.0: a search-based QBF solver beyond traditional QCDCL. In: International Conference on Automated Deduction (CADE), pp. 371–384 (2017)CrossRefGoogle Scholar
  16. 16.
    Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF - (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430–435. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31612-8_33CrossRefGoogle Scholar
  17. 17.
    Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375–392. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40970-2_23CrossRefGoogle Scholar
  18. 18.
    Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: International Conference on Formal Methods in Computer-aided Design (FMCAD), pp. 136–143 (2015)Google Scholar
  19. 19.
    Rabe, M.N., Tentrup, L., Rasmussen, C., Seshia, S.A.: Understanding and extending incremental determinization for 2QBF. In: International Conference on Computer Aided Verification (CAV), pp. 256–274 (2018)CrossRefGoogle Scholar
  20. 20.
    Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: National Conference on Artificial Intelligence (AAAI), pp. 1045–1050 (2007)Google Scholar
  21. 21.
    Skolem, T.: Über die mathematische Logik. Norsk Mat. Tidsskrift 106, 125–142 (1928). (Translation in From Frege to Gödel, A Source Book in Mathematical Logic, J. van Heijenoort, Harvard Univ. Press, 1967)Google Scholar
  22. 22.
    Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415 (2006)Google Scholar
  23. 23.
    Staber, S., Bloem, R.: Fault localization and correction with QBF. In: International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 355–368 (2007)Google Scholar
  24. 24.
    Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: International Conference on Computer Aided Verification (CAV), pp. 475–494 (2017)CrossRefGoogle Scholar
  25. 25.
    Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre – an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373–390. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_21CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Graduate Institute of Electronics EngineeringNational Taiwan UniversityTaipeiTaiwan
  2. 2.Department of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan

Personalised recommendations