nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Combining Resolution-Path Dependencies with Dependency Learning

verfasst von : Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider

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

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 present the first practical implementation of the reflexive resolution-path dependency scheme in a QBF solver. Unlike in DepQBF, which uses the less general standard dependency scheme, we do not compute the dependency relation upfront, but instead query relevant dependencies on demand during dependency conflicts, when the solver is about to learn a missing dependency. Thus, our approach is fundamentally tied to dependency learning, and shows that the two techniques for dependency analysis can be fruitfully combined. As a byproduct, we propose a quasilinear-time algorithm to compute all resolution-path dependencies of a given variable. Experimental results on the QBF library confirm the viability of our technique and identify families of formulas where the speedup is particularly promising.

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 DRAT-based Bit-Vector Proofs in CVC4

Nächstes Kapitel Proof Complexity of Fragments of Long-Distance Q-Resolution

This is the case regardless of the quantifier type of the pivot, the issue is that different targets in the set of blocking variables can be reached using different connecting variables.

http://www.qbflib.org/.

https://projects.informatik.uni-freiburg.de/users/4.

https://www.react.uni-saarland.de/tools/caqe.

https://github.com/lonsing/depqbf.

http://sat.inesc-id.pt/~mikolas/sw/qesto.

https://github.com/perebor/qute.

http://sat.inesc-id.pt/~mikolas/sw/areqs.

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

Lonsing, F., Biere, A.: Integrating Dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_14CrossRef

Lonsing, F., Biere, A.: A compact representation for syntactic dependencies in QBFs. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 398–411. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_37CrossRef

Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 291–308. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_21CrossRefMATH

Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2005). www.qbflib.org

Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res. 26, 371–416 (2006)MathSciNetCrossRef

Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_10CrossRef

Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 325–331. AAAI Press (2015)

Kaibel, V., Peinhardt, M.: On the bottleneck shortest path problem. Zib-report 06–22, Zuse Institute Berlin (2006)

10.

Büning, H.K., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Information and Computation 17(1), 12–18 (1995)MathSciNetCrossRef

11.

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

12.

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

13.

Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design - FMCAD 2015, pp. 136–143. IEEE Computer Society (2015)

14.

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

15.

Slivovsky, F., Szeider, S.: Quantifier reordering for QBF. J. Autom. Reason. 56(4), 459–477 (2016)MathSciNetCrossRef

16.

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

17.

Gelder, A.: Variable Independence and resolution paths for quantified Boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789–803. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_59CrossRef

18.

Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre – an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373–390. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_21CrossRef

19.

Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Pileggi, L.T., Kuehlmann, A. (eds.) Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, San Jose, California, USA, 10–14 November 2002, pp. 442–449. ACM/IEEE Computer Society (2002)

Titel: Combining Resolution-Path Dependencies with Dependency Learning
verfasst von: Tomáš Peitl
Friedrich Slivovsky
Stefan Szeider
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2019
Print ISBN: 978-3-030-24257-2

Electronic ISBN: 978-3-030-24258-9

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-24258-9_22

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"

Premium Partner