# Clause Elimination for SAT and QSAT

J. Artif. Intell. Res., pp. 127-168, 2015.

EI

Keywords:

Asymmetric blocked clause eliminationstrong exponential time hypothesisart satQSAT-specific variant of BCPelimination procedureMore(26+)

Weibo:

Abstract:

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative progra...

Code:

Data:

Introduction

- Boolean satisfiability (SAT) is the problem of determining whether a given propositional logic formula has a solution.
- SAT has become an important declarative approach to formulate and solve various NP-hard problems—a general coverage of modern satisfiability research is provided by Biere, Heule, van Maaren, and Walsh (2009).
- As SAT is the archetypical problem for NP, the quantified Boolean satisfiability (QSAT) problem of evaluating quantified Boolean formulas (QBF), the well-known extension of SAT, is archetypical for PSPACE, offering a powerful framework for modelling a very large range of important computational problems in artificial intelligence, knowledge representation, verification, and synthesis (Benedetti & Mangassarian, 2008).
- A major part of this quest is to lift techniques proven effective in SAT solving to the more general framework of QSAT solving and to analyze their impact

Highlights

- Boolean satisfiability (SAT) is the problem of determining whether a given propositional logic formula has a solution
- We empirically investigate the impact of prenex conjunctive normal form (PCNF)-level clause elimination procedures when applied as preprocessing in quantified Boolean satisfiability (QSAT)
- We focused on a specific type of preprocessing techniques, clause elimination procedures that remove clauses from conjunctive normal form (CNF) and PCNF formulas based on different polynomial-time checkable redundancy properties
- We introduced novel clause elimination procedures for both CNF and PCNF formulas as asymmetric variants of the known techniques of tautology, subsumption, and blocked clause elimination procedures, and developed a novel family of so-called covered clause elimination procedures
- Complementing the more theoretical analysis, we presented results of an empirical evaluation on the practical effectiveness of the procedures in speeding-up the overall solving runtime of state-of-the-art SAT and QSAT solvers on real-world benchmark instances
- The results show that, while the effects on the SAT-level are modest, applying the clause elimination procedures is clearly beneficial in the context of QSAT solving

Results

- For the QBFLib track benchmarks, the application of BLOQQER drastically decreases the number of clauses.

Conclusion

- Preprocessing and inprocessing techniques have proven important in speeding up state-of-the-art SAT and QSAT solving.
- The authors analyzed all of the variants from various perspectives—relative effectiveness, BCP-preserving, confluence, logical equivalence—highlighting intricate differences between the procedures.
- This resulted in a relative power hierarchy, reflecting the relative strengths of the procedures in removing clauses.
- The results show that, while the effects on the SAT-level are modest, applying the clause elimination procedures is clearly beneficial in the context of QSAT solving

Summary

## Introduction:

Boolean satisfiability (SAT) is the problem of determining whether a given propositional logic formula has a solution.- SAT has become an important declarative approach to formulate and solve various NP-hard problems—a general coverage of modern satisfiability research is provided by Biere, Heule, van Maaren, and Walsh (2009).
- As SAT is the archetypical problem for NP, the quantified Boolean satisfiability (QSAT) problem of evaluating quantified Boolean formulas (QBF), the well-known extension of SAT, is archetypical for PSPACE, offering a powerful framework for modelling a very large range of important computational problems in artificial intelligence, knowledge representation, verification, and synthesis (Benedetti & Mangassarian, 2008).
- A major part of this quest is to lift techniques proven effective in SAT solving to the more general framework of QSAT solving and to analyze their impact
## Results:

For the QBFLib track benchmarks, the application of BLOQQER drastically decreases the number of clauses.## Conclusion:

Preprocessing and inprocessing techniques have proven important in speeding up state-of-the-art SAT and QSAT solving.- The authors analyzed all of the variants from various perspectives—relative effectiveness, BCP-preserving, confluence, logical equivalence—highlighting intricate differences between the procedures.
- This resulted in a relative power hierarchy, reflecting the relative strengths of the procedures in removing clauses.
- The results show that, while the effects on the SAT-level are modest, applying the clause elimination procedures is clearly beneficial in the context of QSAT solving

- Table1: Properties of clause elimination procedures for SAT. Preserves logical eq BCP-preserving Confluent
- Table2: LINGELING configurations on application instances from SAT Competition 2013
- Table3: Different BLOQQER configurations with solver DEPQBF on QBFLib benchmarks
- Table4: Different BLOQQER configurations with solver DEPQBF on Application benchmarks

Funding

- The authors gratefully acknowledge financial support from DARPA contract number N66001-102-4087 (MH); Academy of Finland under grants 251170 COIN Centre of Excellence in Computational Inference Research, 276412, and 284591 (MJ); Austrian Science Foundation (FWF) NFN Grants S11408-N23 RiSE (AB) and S11409-N23 RiSE (FL); and Vienna Science and Technology Fund (WWTF) under grant ICT10-018 (MS)

Study subjects and analysis

cases: 3

The rest follows from lifting the implication over the conjunction that defines the semantics of universal quantification if quant(Q1) = ∀, and, respectively, over the disjunction that defines the semantics of the existential quantification if quant(Q1) = ∃. Three cases have to be considered for showing that C[h] is a blocked clause or removed in F [h]. 1. h ∈ C

participants: 4

If the preprocessor does not terminate after 900 seconds, then preprocessing is aborted and the formula is considered to be unsolved. We consider four participants of the QBF Gallery, which are publicly available: the CDCL-based solver DEPQBF (Lonsing & Biere, 2010; Egly, Lonsing, & Widl, 2013); the CEGAR-based solver RAREQS (Janota, Klieber, Marques-Silva, & Clarke, 2012); the GHOSTQ solver (Klieber et al, 2010; Klieber, 2014) implementing a CEGAR-based approach in combination with so-called ghost variables, allowing for duality-aware reasoning on the CNF level; and the solver QUBE that includes the preprocessor SQUEEZEBF (Giunchiglia et al, 2010). This

Reference

- Bacchus, F. (2002). Enhancing Davis Putnam with extended binary clause reasoning. In Dechter, R., & Sutton, R. S. (Eds.), Proceedings of the 18th National Conference on Artificial Intelligence (AAAI 2002), pp. 613–619. AAAI Press.
- Balabanov, V., & Jiang, J.-H. R. (2011). Resolution proofs and Skolem functions in QBF evaluation and applications. In Gopalakrishnan, G., & Qadeer, S. (Eds.), Proceedings of the 23rd
- International Conference on Computer Aided Verification (CAV 2011), Vol. 6806 of Lecture Notes in Computer Science, pp. 149–164. Springer.
- Balint, A., Belov, A., Jarvisalo, M., & Sinz, C. (2015). Overview and analysis of the SAT Challenge 2012 solver competition. Artificial Intelligence, 223, 120–155.
- Belov, A., Jarvisalo, M., & Marques-Silva, J. (2013a). Formula preprocessing in MUS extraction. In Piterman, N., & Smolka, S. A. (Eds.), Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Vol. 7795 of Lecture Notes in Computer Science, pp. 108–123. Springer.
- Belov, A., Morgado, A., & Marques-Silva, J. (2013b). SAT-based preprocessing for MaxSAT. In McMillan, K. L., Middeldorp, A., & Voronkov, A. (Eds.), Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR19), Vol. 8312 of Lecture Notes in Computer Science, pp. 96–111. Springer.
- Benedetti, M. (2005a). Extracting certificates from quantified boolean formulas. In Kaelbling, L. P., & Saffiotti, A. (Eds.), Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 47–53. Professional Book Center.
- Benedetti, M. (2005b). sKizzo: A Suite to Evaluate and Certify QBFs. In Nieuwenhuis, R. (Ed.), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Vol. 3632 of Lecture Notes in Computer Science, pp. 369–376. Springer.
- Benedetti, M., & Mangassarian, H. (2008). QBF-based formal verification: Experience and perspectives. Journal of Satisfiability, Boolean Modeling and Computation, 5(1-4), 133–191.
- Berg, J., Saikko, P., & Jarvisalo, M. (2015). Improving the effectiveness of SAT-based preprocessing for MaxSAT. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). AAAI Press.
- Biere, A. (2005). Resolve and expand. In Hoos, H. H., & Mitchell, D. G. (Eds.), Revised Selected Papers of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vol. 3542 of Lecture Notes in Computer Science, pp. 59–70. Springer.
- Biere, A. (2013). Lingeling, Plingeling and Treengeling entering the SAT Competition 2013. In Balint, A., Belov, A., Heule, M., & Jarvisalo, M. (Eds.), Proceedings of SAT Competition 2013, Vol. B-2013-1 of Department of Computer Science Series of Publications B, pp. 51– 52. University of Helsinki.
- Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). Handbook of Satisfiability, Vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press.
- Biere, A., Lonsing, F., & Seidl, M. (2011). Blocked clause elimination for QBF. In Bjørner, N., & Sofronie-Stokkermans, V. (Eds.), Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Vol. 6803 of Lecture Notes in Computer Science, pp. 101–115. Springer.
- Brafman, R. I. (2004). A simplifier for propositional formulas with many binary clauses. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 34(1), 52–59.
- Bubeck, U., & Kleine Buning, H. (2007). Bounded universal expansion for preprocessing QBF. In Marques-Silva, J., & Sakallah, K. A. (Eds.), Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Vol. 4501 of Lecture Notes in Computer Science, pp. 244–257. Springer.
- Cadoli, M., Giovanardi, A., & Schaerf, M. (1998). An algorithm to evaluate quantified boolean formulae. In Mostow, J., & Rich, C. (Eds.), Proceedings of the 15th National Conference on Artificial Intelligence (AAAI 1998), pp. 262–267. AAAI Press / The MIT Press.
- Calabro, C., Impagliazzo, R., & Paturi, R. (2009). The complexity of satisfiability of small depth circuits. In Chen, J., & Fomin, F. V. (Eds.), Revised Selected Paper of the 4th International Workshop on Parameterized and Exact Computation (IWPEC 2009), Vol. 5917 of Lecture Notes in Computer Science, pp. 75–85. Springer.
- Claessen, K., Een, N., Sheeran, M., & Sorensson, N. (2008). SAT-solving in practice. In Proceedings of the 9th International Workshop on Discrete Event Systems (WODES 2008), pp. 61–67. IEEE.
- Cook, S. A. (1971). The complexity of theorem-proving procedures. In Harrison, M. A., Banerji, R. B., & Ullman, J. D. (Eds.), Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151–158. ACM.
- Een, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In Bacchus, F., & Walsh, T. (Eds.), Proceedings of 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), Vol. 3569 of Lecture Notes in Computer Science, pp. 61–75. Springer.
- Egly, U., Lonsing, F., & Widl, M. (2013). Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In McMillan, K., Middeldorp, A., & Voronkov, A. (Eds.), Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013), Vol. 8312 of Lecture Notes in Computer Science, pp. 291–308. Springer.
- Fourdrinoy, O., Gregoire, E., Mazure, B., & Saıs, L. (2007a). Eliminating redundant clauses in SAT instances. In Hentenryck, P. V., & Wolsey, L. A. (Eds.), Proceedings of the 4th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2007), Vol. 4510 of Lecture Notes in Computer Science, pp. 71–83. Springer.
- Fourdrinoy, O., Gregoire, E., Mazure, B., & Saıs, L. (2007b). Reducing hard SAT instances to polynomial ones. In Proceedings of the 8th IEEE International Conference on Information Reuse and Integration (IRI 2007), pp. 18–23. IEEE.
- Freeman, J. (1995). Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania.
- Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman.
- Gershman, R., & Strichman, O. (2005). Cost-effective hyper-resolution for preprocessing CNF formulas. In Bacchus, F., & Walsh, T. (Eds.), Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), Vol. 3569 of Lecture Notes in Computer Science, pp. 423–429. Springer.
- Giunchiglia, E., Marin, P., & Narizzano, M. (2010). sQueezeBF: An effective preprocessor for QBFs based on equivalence reasoning. In Strichman, O., & Szeider, S. (Eds.), Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), Vol. 6175 of Lecture Notes in Computer Science, pp. 85–98. Springer.
- Goultiaeva, A., & Bacchus, F. (2013). Recovering and utilizing partial duality in QBF. In Jarvisalo, M., & Gelder, A. V. (Eds.), Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Vol. 7962 of Lecture Notes in Computer Science, pp. 83–99. Springer.
- Goultiaeva, A., Seidl, M., & Biere, A. (2013). Bridging the gap between dual propagation and CNF-based QBF solving. In Macii, E. (Ed.), Proceedings of Design, Automation and Test in Europe Conference & Exhibition (DATE 2013), pp. 811–814. EDA Consortium / ACM DL.
- Goultiaeva, A., Van Gelder, A., & Bacchus, F. (2011). A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Walsh, T. (Ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 546–553. IJCAI/AAAI Press.
- Han, H., & Somenzi, F. (2007). Alembic: An efficient algorithm for CNF preprocessing. In Proceedings of the 44th Design Automation Conference (DAC 2007), pp. 582–587. IEEE.
- Han, H., & Somenzi, F. (2009). On-the-fly clause improvement. In Kullmann, O. (Ed.), Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), Vol. 5584 of Lecture Notes in Computer Science, pp. 209–222. Springer.
- Heule, M., Jarvisalo, M., & Biere, A. (2010). Clause elimination procedures for CNF formulas. In Fermuller, C., & Voronkov, A. (Eds.), Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17), Vol. 6397 of Lecture Notes in Computer Science, pp. 357–371. Springer.
- Heule, M., Jarvisalo, M., & Biere, A. (2013a). Covered clause elimination. In Fermuller, C., & Voronkov, A. (Eds.), Short Paper Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17), Vol. 13 of EasyChair Proceedings in Computing, pp. 41–46.
- Heule, M., Jarvisalo, M., & Biere, A. (2013b). Revisiting hyper binary resolution. In Gomes, C. P., & Sellmann, M. (Eds.), Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2013), Vol. 7874 of Lecture Notes in Computer Science, pp. 77–93. Springer.
- Heule, M., Seidl, M., & Biere, A. (2014a). A Unified Proof System for QBF Preprocessing. In Demri, S., Kapur, D., & Weidenbach, C. (Eds.), Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Vol. 8562 of Lecture Notes in Computer Science, pp. 91–106. Springer.
- Heule, M., Seidl, M., & Biere, A. (2014b). Efficient extraction of Skolem functions from QRAT proofs. In Claessen, K., & Kuncak, V. (Eds.), Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2014), pp. 107–114. IEEE.
- Heyman, T., Smith, D., Mahajan, Y., Leong, L., & Abu-Haimed, H. (2014). Dominant controllability check using QBF-solver and netlist optimizer. In Sinz, C., & Egly, U. (Eds.), Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vol. 8561 of Lecture Notes in Computer Science, pp. 227–242. Springer.
- Impagliazzo, R., Paturi, R., & Zane, F. (2001). Which problems have strongly exponential complexity?. Journal of Computer and System Sciences, 63(4), 512–530.
- Janota, M., Grigore, R., & Marques-Silva, J. (2013). On QBF proofs and preprocessing. In McMillan, K. L., Middeldorp, A., & Voronkov, A. (Eds.), Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), Vol. 8312 of Lecture Notes in Computer Science, pp. 473–489. Springer.
- Janota, M., Klieber, W., Marques-Silva, J., & Clarke, E. (2012). Solving QBF with counterexample guided refinement. In Cimatti, A., & Sebastiani, R. (Eds.), Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Vol. 7317 of Lecture Notes in Computer Science, pp. 114–128. Springer.
- Jarvisalo, M., & Biere, A. (2010). Reconstructing solutions after blocked clause elimination. In Strichman, O., & Szeider, S. (Eds.), Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), Vol. 6175 of Lecture Notes in Computer Science, pp. 340–345. Springer.
- Jarvisalo, M., Biere, A., & Heule, M. (2010). Blocked clause elimination. In Esparza, J., & Majumdar, R. (Eds.), Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010), Vol. 6015 of Lecture Notes in Computer Science, pp. 129–1Springer.
- Jarvisalo, M., Biere, A., & Heule, M. (2012a). Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning, 49(4), 583–619.
- Jarvisalo, M., Heule, M., & Biere, A. (2012b). Inprocessing rules. In Gramlich, B., Miller, D., & Sattler, U. (Eds.), Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), Vol. 7364 of Lecture Notes in Computer Science, pp. 355–370. Springer.
- Jarvisalo, M., & Korhonen, J. H. (2014). Conditional lower bounds for failed literals and related techniques. In Sinz, C., & Egly, U. (Eds.), Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vol. 8561 of Lecture Notes in Computer Science, pp. 75–84. Springer.
- Jarvisalo, M., Le Berre, D., Roussel, O., & Simon, L. (2012). The international SAT solver competitions. AI Magazine, 33(1), 89–92.
- Jin, H., & Somenzi, F. (2005). An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science, 119(2), 51–65.
- Jordan, C., & Seidl, M. (2014). QBF Gallery 2014. http://qbf.satisfiability.org/gallery/.
- Kleine Buning, H., & Bubeck, U. (2009). Theory of quantified Boolean formulas. In Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.), Handbook of Satisfiability, Vol. 185 of Frontiers in Artificial Intelligence and Applications, pp. 735–760. IOS Press.
- Kleine Buning, H., Karpinski, M., & Flogel, A. (1995). Resolution for Quantified Boolean Formulas. Information and Computation, 117(1), 12–18.
- Klieber, W. (2014).
- Formal Verification Using Quantified Boolean Formulas (QBF). Ph.D. thesis, Carnegie Mellon University, available at http://reportsarchive.adm.cs.cmu.edu/anon/2014/CMU-CS-14-117.pdf.
- Klieber, W., Sapra, S., Gao, S., & Clarke, E. M. (2010). A non-prenex, non-clausal QBF solver with game-state learning. In Strichman, O., & Szeider, S. (Eds.), Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), Vol. 6175 of Lecture Notes in Computer Science, pp. 128–142. Springer.
- Kullmann, O. (1999). On a generalization of extended resolution. Discrete Applied Mathematics, 96–97, 149–176.
- Kupferschmid, S., Lewis, M. D. T., Schubert, T., & Becker, B. (2011). Incremental preprocessing methods for use in BMC. Formal Methods in System Design, 39(2), 185–204.
- Le Berre, D. (2001). Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics, 9, 59–80.
- Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203–232.
- Lonsing, F., & Biere, A. (2010). DepQBF: A dependency-aware QBF solver. Journal of Satisfiability, Boolean Modeling and Computation, 7(2-3), 71–76.
- Lynce, I., & Marques-Silva, J. (2001). The interaction between simplification and search in propositional satisfiability. In CP’01 Workshop on Modeling and Problem Formulation.
- Mangassarian, H., Le, B., Goultiaeva, A., Veneris, A. G., & Bacchus, F. (2010). Leveraging dominators for preprocessing QBF. In Design, Automation and Test in Europe (DATE 2010), pp. 1695–1700. IEEE.
- Manthey, N., Heule, M., & Biere, A. (2013). Automated reencoding of boolean formulas. In Biere, A., Nahir, A., & Vos, T. E. J. (Eds.), Revised Selected Papers of the 8th International Haifa Verification Conference (HVC 2012), Vol. 7857 of Lecture Notes in Computer Science, pp. 102–117. Springer.
- Marin, P., Miller, C., & Becker, B. (2012). Incremental QBF preprocessing for partial design verification - (poster presentation).
- In Cimatti, A., & Sebastiani, R. (Eds.), Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Vol. 7317 of Lecture Notes in Computer Science, pp. 473–474. Springer.
- Marques-Silva, J. (2008). Practical applications of Boolean satisfiability. In Proceedings of the 9th International Workshop on Discrete Event Systems (WODES 2008), pp. 74–80. IEEE.
- Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., & Biere, A. (2012). Resolution-based certificate extraction for QBF - (tool presentation).
- In Cimatti, A., & Sebastiani, R. (Eds.), Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Vol. 7317 of Lecture Notes in Computer Science, pp. 430–435. Springer.
- Ostrowski, R., Gregoire, E., Mazure, B., & Saıs, L. (2002). Recovering and exploiting structural knowledge from CNF formulas. In Hentenryck, P. V. (Ed.), Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP 2002), Vol. 2470 of Lecture Notes in Computer Science, pp. 185–199. Springer.
- Piette, C., Hamadi, Y., & Saıs, L. (2008). Vivifying propositional clausal formulae. In Ghallab, M., Spyropoulos, C. D., Fakotakis, N., & Avouris, N. M. (Eds.), Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), Vol. 178 of Frontiers in Artificial Intelligence and Applications, pp. 525–529. IOS Press.
- Pigorsch, F., & Scholl, C. (2010). An AIG-based QBF-solver using SAT for preprocessing. In Sapatnekar, S. S. (Ed.), Proceedings of the 47th Design Automation Conference (DAC 2010), pp. 170–175. ACM.
- Pulina, L., & Tacchella, A. (2009). A structural approach to reasoning with quantified boolean formulas. In Boutilier, C. (Ed.), Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 596–602.
- Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23–41.
- Sabharwal, A., Ansotegui, C., Gomes, C. P., Hart, J. W., & Selman, B. (2006). QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. In Biere, A., & Gomes, C. P. (Eds.), Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), Vol. 4121 of Lecture Notes in Computer Science, pp. 382–395. Springer.
- Samer, M. (2008). Variable dependencies of quantified CSPs. In Cervesato, I., Veith, H., & Voronkov, A. (Eds.), Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Vol. 5330 of Lecture Notes in Computer Science, pp. 512–527. Springer.
- Samulowitz, H., Davies, J., & Bacchus, F. (2006). Preprocessing QBF. In Benhamou, F. (Ed.), Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), Vol. 4204 of Lecture Notes in Computer Science, pp. 514–529. Springer.
- SAT Competitions Organizing Committee (2014). The international SAT Competitions web page. http://satcompetition.org/.
- Schaefer, T. J. (1978). On the complexity of some two-person perfect-information games. Journal of Computer and System Sciences, 16(2), 185–225.
- Seidl, M., & Biere, A. (2015). Bloqqer. http://fmv.jku.at/bloqqer.
- Seidl, M., & Konighofer, R. (2014). Partial witnesses from preprocessed quantified Boolean formulas. In Proceedings of Design, Automation & Test in Europe Conference & Exhibition (DATE 2014), pp. 1–6. IEEE. Subbarayan, S., & Pradhan, D. K. (2005). NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In Hoos, H. H., & Mitchell, D. G. (Eds.), Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vol. 3542 of Lecture Notes in Computer Science, pp. 276–291. Springer.
- Van Gelder, A. (2005). Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence, 43(1), 239–253.
- Van Gelder, A., Wood, S. B., & Lonsing, F. (2012). Extended failed-literal preprocessing for quantified boolean formulas. In Cimatti, A., & Sebastiani, R. (Eds.), Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Vol. 7317 of Lecture Notes in Computer Science, pp. 86–99. Springer.
- Zhang, L. (2006). Solving QBF by combining conjunctive and disjunctive normal forms. In Gil, Y., & Mooney, R. J. (Eds.), Proceedings of the 21st National Conference on Artificial Intelligence (AAAI 2006), pp. 143–150. AAAI Press.

Best Paper

Best Paper of IJCAI, 2015

Tags

Comments