Clause Elimination for SAT and QSAT

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

Cited by: 60|Bibtex|Views191|Links
EI
Keywords:
Asymmetric blocked clause eliminationstrong exponential time hypothesisart satQSAT-specific variant of BCPelimination procedureMore(26+)
Weibo:
We focused on a specific type of preprocessing techniques, clause elimination procedures that remove clauses from conjunctive normal form and prenex conjunctive normal form formulas based on different polynomial-time checkable redundancy properties

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:

0
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
Tables
  • 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
Download tables as Excel
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.
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • International Conference on Computer Aided Verification (CAV 2011), Vol. 6806 of Lecture Notes in Computer Science, pp. 149–164. Springer.
    Google ScholarLocate open access versionFindings
  • Balint, A., Belov, A., Jarvisalo, M., & Sinz, C. (2015). Overview and analysis of the SAT Challenge 2012 solver competition. Artificial Intelligence, 223, 120–155.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Benedetti, M., & Mangassarian, H. (2008). QBF-based formal verification: Experience and perspectives. Journal of Satisfiability, Boolean Modeling and Computation, 5(1-4), 133–191.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Freeman, J. (1995). Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania.
    Google ScholarFindings
  • Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Impagliazzo, R., Paturi, R., & Zane, F. (2001). Which problems have strongly exponential complexity?. Journal of Computer and System Sciences, 63(4), 512–530.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Jarvisalo, M., Biere, A., & Heule, M. (2012a). Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning, 49(4), 583–619.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Jarvisalo, M., Le Berre, D., Roussel, O., & Simon, L. (2012). The international SAT solver competitions. AI Magazine, 33(1), 89–92.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Jordan, C., & Seidl, M. (2014). QBF Gallery 2014. http://qbf.satisfiability.org/gallery/.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • Kleine Buning, H., Karpinski, M., & Flogel, A. (1995). Resolution for Quantified Boolean Formulas. Information and Computation, 117(1), 12–18.
    Google ScholarLocate open access versionFindings
  • Klieber, W. (2014).
    Google ScholarFindings
  • 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.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • Kullmann, O. (1999). On a generalization of extended resolution. Discrete Applied Mathematics, 96–97, 149–176.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Le Berre, D. (2001). Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics, 9, 59–80.
    Google ScholarLocate open access versionFindings
  • Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203–232.
    Google ScholarLocate open access versionFindings
  • Lonsing, F., & Biere, A. (2010). DepQBF: A dependency-aware QBF solver. Journal of Satisfiability, Boolean Modeling and Computation, 7(2-3), 71–76.
    Google ScholarLocate open access versionFindings
  • Lynce, I., & Marques-Silva, J. (2001). The interaction between simplification and search in propositional satisfiability. In CP’01 Workshop on Modeling and Problem Formulation.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Marin, P., Miller, C., & Becker, B. (2012). Incremental QBF preprocessing for partial design verification - (poster presentation).
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., & Biere, A. (2012). Resolution-based certificate extraction for QBF - (tool presentation).
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23–41.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • SAT Competitions Organizing Committee (2014). The international SAT Competitions web page. http://satcompetition.org/.
    Findings
  • Schaefer, T. J. (1978). On the complexity of some two-person perfect-information games. Journal of Computer and System Sciences, 16(2), 185–225.
    Google ScholarLocate open access versionFindings
  • Seidl, M., & Biere, A. (2015). Bloqqer. http://fmv.jku.at/bloqqer.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • Van Gelder, A. (2005). Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence, 43(1), 239–253.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Best Paper
Best Paper of IJCAI, 2015
Tags
Comments