×

Blocked clause elimination for QBF. (English) Zbl 1341.68181

Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 101-115 (2011).
Summary: Quantified Boolean formulas (QBF) provide a powerful framework for encoding problems from various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques, the performance of such a solver usually depends on the way a problem is represented. However, the translation to processable QBF encodings is in general not unique and may either introduce variables and clauses not relevant for the solving process or blur information which could be beneficial for the solving process. To deal with both of these issues, preprocessors have been introduced which rewrite a given QBF before it is passed to a solver.
In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art.
For the entire collection see [Zbl 1218.68006].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B05 Classical propositional logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bacchus, F., Winter, J.: Effective Preprocessing with Hyper-Resolution and Equality Reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2004) · Zbl 1204.68176 · doi:10.1007/978-3-540-24605-3_26
[2] Le Berre, D.: Exploiting the Real Power of Unit Propagation Lookahead. Electronic Notes in Discrete Mathematics 9, 59–80 (2001) · Zbl 0990.90538 · doi:10.1016/S1571-0653(04)00314-2
[3] Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005) · Zbl 1122.68585 · doi:10.1007/11527695_5
[4] Bubeck, U., Kleine Büning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244–257. Springer, Heidelberg (2007) · Zbl 1214.68331 · doi:10.1007/978-3-540-72788-0_24
[5] Büning, H.K., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995) · Zbl 0828.68045 · doi:10.1006/inco.1995.1025
[6] Eén, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463 · doi:10.1007/11499107_5
[7] Giunchiglia, E., Marin, P., Narizzano, M.: QuBE 7.0. JSAT 7, 83–88 (2010)
[8] Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 85–98. Springer, Heidelberg (2010) · Zbl 1306.68157 · doi:10.1007/978-3-642-14186-7_9
[9] Heule, M., Järvisalo, M., Biere, A.: Clause elimination procedures for cnf formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010) · Zbl 1306.68144 · doi:10.1007/978-3-642-16242-8_26
[10] Heule, M., Järvisalo, M., Biere, A.: Covered Clause Elimination. CoRR, abs/1011.5202 (2010); Short paper proceedings LPAR-17
[11] Järvisalo, M., Biere, A., Heule, M.: Blocked Clause Elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010) · Zbl 1284.03208 · doi:10.1007/978-3-642-12002-2_10
[12] Kullmann, O.: On a Generalization of Extended Resolution. Discrete Applied Mathematics 96, 149–176 (1999) · Zbl 0941.68126 · doi:10.1016/S0166-218X(99)00037-2
[13] Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF solving. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 196–210. Springer, Heidelberg (2008) · Zbl 1138.68546 · doi:10.1007/978-3-540-79719-7_19
[14] Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver (System Description). JSAT 7, 71–76 (2010)
[15] Mangassarian, H., Le, B., Goultiaeva, A., Veneris, A.G., Bacchus, F.: Leveraging Dominators for Preprocessing QBF. In: Design, Automation and Test in Europe (DATE 2010), pp. 1695–1700. IEEE, Los Alamitos (2010)
[16] Ostrowski, R., Grgoire, E., Mazure, B., Saïs, L.: Recovering and Exploiting Structural Knowledge from CNF Formulas. In: Proc. of the 8th Int. Conf. on Princ. and Pract. of Constraint Prog (CP 2002), pp. 199–206. Springer, Heidelberg (2006)
[17] Pigorsch, F., Scholl, C.: An AIG-Based QBF-Solver Using SAT for Preprocessing. In: Proc. of the 47th Design Aut. Conf (DAC 2010), pp. 170–175 (2010) · doi:10.1145/1837274.1837318
[18] Plaisted, D.A., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation 2(3), 293–304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1
[19] Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514–529. Springer, Heidelberg (2006) · Zbl 05323497 · doi:10.1007/11889205_37
[20] Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. Studies in Constructive Mathematics and Mathematical Logic 2(115-125), 10–13 (1968)
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.