×

Unified QBF certification and its applications. (English) Zbl 1284.68516

Summary: Quantified Boolean formulae (QBF) allow compact encoding of many decision problems. Their importance motivated the development of fast QBF solvers. Certifying the results of a QBF solver not only ensures correctness, but also enables certain synthesis and verification tasks. To date the certificate of a true formula can be in the form of either a syntactic cube-resolution proof or a semantic Skolem-function model whereas that of a false formula is only in the form of a syntactic clause-resolution proof. The semantic certificate for a false QBF is missing, and the syntactic and semantic certificates are somewhat unrelated. This paper identifies the missing Herbrand-function countermodel for false QBF, and strengthens the connection between syntactic and semantic certificates by showing that, given a true QBF, its Skolem-function model is derivable from its cube-resolution proof of satisfiability as well as from its clause-resolution proof of unsatisfiability under formula negation. Consequently Skolem-function derivation can be decoupled from special Skolemization-based solvers and computed from standard search-based ones. Experimental results show strong benefits of the new method.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T27 Logic in artificial intelligence

Software:

MiniSat; ABC ; Quaffle
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Benedetti M (2004) Evaluating QBFs via symbolic skolemization. In: Proc int’l conf on logic for programming, artificial intelligence and reasoning (LPAR)
[2] Benedetti M (2005) Extracting certificates from quantified Boolean formulas. In: Proc int’l joint conf on artificial intelligence (IJCAI)
[3] Bloem R, Galler S, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M (2007) Automatic hardware synthesis from specifications: a case study. In: Proc. design automation and test in Europe (DATE)
[4] Balabanov V, Jiang J-HR (2011) Resolution proofs and Skolem functions in QBF evaluation and applications. In: Proc int’l conf on computer aided verification (CAV), pp 149–164
[5] Berkeley Logic Synthesis and Verification Group. ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/\(\sim\)alanmi/abc/
[6] Cadoli M, Schaerf M, Giovanardi A, Giovanardi M (2002) An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J Autom Reason 28(2):101–142 · Zbl 1002.68165
[7] Dershowitz N, Hanna Z, Katz J (2005) Bounded model checking with QBF. In: Proc int’l conf on theory and applications of satisfiability testing (SAT) · Zbl 1128.68366
[8] Eén N, Sörensson N (2003) An extensible SAT-solver. In: Proc int’l conf on theory and applications of satisfiability testing (SAT), pp 502–518 · Zbl 1204.68191
[9] Giunchiglia E, Narizzano M, Tacchella A (2006) Clause-term resolution and learning in quantified Boolean logic satisfiability. Artif Intell Res 26:371–416 · Zbl 1183.68475
[10] Jussila T, Biere A, Sinz C, Kröning D, Wintersteiger C (2007) A first step towards a unified proof checker for QBF. In: Proc int’l conf on theory and applications of satisfiability testing (SAT), pp 201–214 · Zbl 1214.68334
[11] Jiang J-HR, Lin H-P, Hung W-L (2009) Interpolating functions from large Boolean relations. In: Proc int’l conf on computer-aided design (ICCAD), pp 779–784
[12] Kleine-Büning H, Karpinski M, Flögel A (1995) Resolution for quantified Boolean formulas. Inf Comput 117(1):12–18 · Zbl 0828.68045
[13] Narizzano M, Peschiera C, Pulina L, Tacchella A (2009) Evaluating and certifying QBFs: a comparison of state-of-the-art tools. In: AI communications · Zbl 1186.68440
[14] Papadimitriou CH (1994) Computational complexity. Addison-Wesley, Reading · Zbl 0833.68049
[15] QBF solver evaluation portal. http://www.qbflib.org/qbfeval/
[16] Rintanen J (1999) Constructing conditional plans by a theorem-prover. J Artif Intell Res 10:323–352 · Zbl 0916.68139
[17] Skolem Th (1928) Über die Mathematische Logik. Nor Mat Tidsskr 10:125–142 [Translation in From Frege to Gödel, a source book in mathematical logic, J van Heijenoort, Harvard Univ Press, 1967] · JFM 54.0058.01
[18] Staber S, Bloem R (2007) Fault localization and correction with QBF. In: Proc. int’l conf. on theory and applications of satisfiability testing (SAT), pp 355–368 · Zbl 1214.94086
[19] Solar-Lezama A, Tancau L, Bodík R, Seshia S, Saraswat V (2006) Combinatorial sketching for finite programs. In: Proc int’l conf on architectural support for programming languages and operating systems (ASPLOS), pp 404–415
[20] Tseitin G (1970) On the complexity of derivation in propositional calculus. In: Studies in constructive mathematics and mathematical logic, pp 466–483
[21] Yu Y, Malik S (2005) Validating the result of a quantified Boolean formula (QBF) solvers: theory and practice. In: Proc Asia and South Pacific design automation conference (ASP-DAC)
[22] Zhang L, Malik S (2002) Conflict driven learning in a quantified Boolean satisfiability solver. In: Proc int’l conf on computer-aided design (ICCAD), pp 442–449
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.