nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths

verfasst von : Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2020

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any DQBF proof system. We further explore the power of DQBF resolution systems parameterised by dependency schemes and show that our new scheme results in exponentially shorter proofs in comparison to the reflexive resolution path dependency scheme when used in the expansion DQBF system \(\mathsf {\forall {Exp{\text{+ }}Res}}\).

On QBFs, we demonstrate that our new scheme is exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency scheme known to date.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Nächstes Kapitel Short Q-Resolution Proofs with Homomorphisms

The standard input for solvers is a prenex QBF.

A different notion of monotonicity for dependency schemes is defined in [29].

This holds for all known DQBF proof systems.

Azhar, S., Peterson, G., Reif, J.: Lower bounds for multiplayer non-cooperative games of incomplete information. J. Comput. Math. Appl. 41, 957–992 (2001)MATH

Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)MATH

Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_12MATHCrossRef

Beyersdorff, O., Blinkhorn, J.: Dependency schemes in qbf calculi: semantics and soundness. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 96–112. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44953-1_7CrossRef

Beyersdorff, O., Blinkhorn, J.: Genuine lower bounds for QBF expansion. In: Niedermeier, R., Vallée, B. (eds.) International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 96, pp. 12:1–12:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Beyersdorff, O., Blinkhorn, J.: Dynamic QBF dependencies in reduction and expansion. ACM Trans. Comput. Logic 21(2), 1–27 (2019)MathSciNetMATH

Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R.A., Suda, M.: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. J. Autom. Reason. 63(3), 597–623 (2019)MathSciNetMATH

Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Logical Methods Comput. Sci. 15(1), (2019)

Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Sudan, M. (ed.) ACM Conference on Innovations in Theoretical Computer Science (ITCS), pp. 249–260. ACM (2016)

10.

Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1–26:42 (2019)MathSciNetMATH

11.

Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculito DQBF. In: Creignou and Berre [16], pp. 490-499

12.

Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theory 12(2), 10:1–10:27 (2020)MathSciNet

13.

Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 263–280. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_17CrossRef

14.

Chen, H.: Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Trans. Comput. Theory 9(3), 15:1–15:20 (2017)MathSciNetMATH

15.

Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbol. Logic 44(1), 36–50 (1979)MathSciNetMATH

16.

Creignou, N., Le Berre, D. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT). LNCS, vol. 9710. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2

17.

Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21–45 (2017)MathSciNetMATH

18.

Henkin, L.: Some remarks on infinitely long formulas. Infinitistic Methods, pp. 167–183 (1961)

19.

Hooker, J. (ed.): International Conference on Principles and Practice of Constraint Programming (CP). LNCS, vol. 11008. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98334-9

20.

Hoos, H.H., Peitl, T., Slivovsky, F., Szeider, S.: portfolio-based algorithm selection for circuit QBFs. In: Hooker [19], pp. 195–209

21.

Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25–42 (2015)MathSciNetMATH

22.

Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)MathSciNetMATH

23.

Kontchakov, R., et al.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: Boutilier, C. (ed.) International Joint Conference on Artificial Intelligence (IJCAI), pp. 836–841. AAAI Press (2009)

24.

Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371–384. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_23CrossRef

25.

Lonsing, F., Egly, U.: Evaluating QBF solvers: Quantifier alternations matter. In: Hooker [19], pp. 276–294

26.

Mangassarian, H., Veneris, A.G., Benedetti, M.: Robust QBF encodings for sequential circuits with applications to verification, debug, and test. IEEE Trans. Comput. 59(7), 981–994 (2010)MathSciNetMATH

27.

Peitl, T., Slivovsky, F., Szeider, S.: Combining resolution-path dependencies with dependency learning. In: International Conference on Theory and Practice of Satisfiability Testing (SAT), pp. 306–318 (2019)

28.

Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 181–208 (2019)MathSciNetMATH

29.

Peitl, T., Slivovsky, F., Szeider, S.: Long-distance Q-resolution with dependency schemes. J. Autom. Reason. 63(1), 127–155 (2019)MathSciNetMATH

30.

Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). Artif. Intell. 274, 224–248 (2019)MathSciNetMATH

31.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)MathSciNetMATH

32.

Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77–97 (2009)MathSciNetMATH

33.

Scholl, C., Wimmer, R.: Dependency quantified boolean formulas: an overview of solution methods and applications. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 3–16. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_1CrossRef

34.

Slivovsky, F.: Structure in \(\#\)SAT and QBF. Ph.D. thesis, Vienna University of Technology (2015)

35.

Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83–101 (2016)MathSciNetMATH

36.

Vardi, M.Y.: Boolean satisfiability: theory and engineering. Commun. ACM 57(3), 5 (2014)

37.

Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou and Berre [16], pp. 473–489

Titel: Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths
verfasst von: Olaf Beyersdorff
Joshua Blinkhorn
Tomáš Peitl
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

Electronic ISBN: 978-3-030-51825-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51825-7_28

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"