Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Skolem Functions for DQBF

verfasst von : Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don’t-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.

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 Efficient Verification of Program Fragments: Eager POR
Nächstes Kapitel STL Model Checking of Continuous and Hybrid Systems
Fußnoten
1
If the inner-most quantifier block is universal, it can be removed by universal reduction.
 
2
A recent binary of HQS, all DQBF benchmarks we used as well as our proof checker are available at https://​projects.​informatik.​uni-freiburg.​de/​projects/​dqbf.
 
3
Of course, the semantical support could also be checked by a series of SAT calls.
 
4
However, this case never occurred in our experiments.
 
6
The DQBF-variant we consider is called S-form DQBF in [2]. Its negation yields a so-called H-form DQBF, which does not support the computation of Skolem functions.
 
Literatur
1.
Ashar, P., Ganai, M.K., Gupta, A., Ivancic, F., Yang, Z.: Efficient SAT-based bounded model checking for software verification. In: Proceedings of ISoLA. Technical report, vol. TR-2004-6, pp. 157–164. University of Cyprus (2004)
2.
Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86–100 (2014)MathSciNetCrossRefMATH
3.
Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)CrossRefMATH
4.
Balabanov, V., Jiang, J.H.R.: Reducing satisfiability and reachability to DQBF (2015). Talk at the International Workshop on Quantified Boolean Formulas (QBF)
5.
Benedetti, M.: Evaluating QBFs via symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 285–300. Springer, Heidelberg (2005)CrossRef
6.
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)CrossRef
7.
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1–20. Springer, Heidelberg (2014)CrossRef
8.
Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010)CrossRef
9.
Bubeck, U., Kleine Büning, H.: Dependency quantified horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 198–211. Springer, Heidelberg (2006)CrossRef
10.
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of STOC, pp. 151–158. ACM Press (1971)
11.
12.
Czutro, A., Polian, I., Lewis, M.D.T., Engelke, P., Reddy, S.M., Becker, B.: Thread-parallel integrated test pattern generator utilizing satisfiability analysis. Int. J. Parallel Programm. 38(3–4), 185–202 (2010)CrossRefMATH
13.
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRef
14.
Eggersglüß, S., Drechsler, R.: A highly fault-efficient SAT-based ATPG flow. IEEE Des. Test Comput. 29(4), 63–70 (2012)CrossRef
15.
Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243–251. Springer, Heidelberg (2014)
16.
Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: International Workshop on Pragmatics of SAT (POS) (2012)
17.
Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: International Workshop on Pragmatics of SAT (POS). EPiC Series, vol. 27, pp. 103–116. EasyChair (2014)
18.
Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: Proceedings of ICCD, pp. 396–403. IEEE CS (2013)
19.
Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Proceedings of DATE. IEEE (2015)
20.
Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Proceedings of IJCAI, pp. 546–553. IJCAI/AAAI (2011)
21.
Henkin, L.: Some remarks on infinitely long formulas. In: Infinitistic Methods: Proceedings of the 1959 Symposium on Foundations of Mathematics, pp. 167–183. Pergamon Press, Warsaw (1961)
22.
Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127–168 (2015)MathSciNetMATH
23.
Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Proceedings of FMCAD, pp. 107–114. IEEE (2014)
24.
Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 383–397. Springer, Heidelberg (2009)CrossRef
25.
Jussila, T., Biere, A., Sinz, C., Kroning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201–214. Springer, Heidelberg (2007)CrossRef
26.
Kilby, P., Slaney, J.K., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proceedings of NAI/IAAI, pp. 1368–1373. AAAI Press/The MIT Press (2005)
27.
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. CAD Integr. Circ. Syst. 21(12), 1377–1394 (2002)CrossRef
28.
Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-basedQBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 418–433. Springer, Heidelberg (2015)CrossRef
29.
Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisfiability Boolean Modell. Comput. 7(2–3), 71–76 (2010)
30.
McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005)CrossRef
31.
Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430–435. Springer, Heidelberg (2012)CrossRef
32.
Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer non-cooperative games of incomplete information. Comput. Math. Appl. 41(7–8), 957–992 (2001)MathSciNetCrossRefMATH
33.
Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver. In: Proceedings of DATE, pp. 1596–1601. IEEE (2009)
34.
Pigorsch, F., Scholl, C.: An AIG-based QBF-solver using SAT for preprocessing. In: Proceedings of DAC, pp. 170–175. ACM Press (2010)
35.
Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symbolic Logic 62(3), 981–998 (1997)MathSciNetCrossRefMATH
36.
Rintanen, J., Heljanko, K., Niemelä, I.: Planning as satisfiability: parallel plans and algorithms for plan search. Artif. Intell. 170(12–13), 1031–1080 (2006)MathSciNetCrossRefMATH
37.
Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of DAC, pp. 238–243. ACM Press (2001)
38.
Tentrup, L., Rabe, M.N.: CAQE: a certifying QBF solver. In: Proceedings of FMCAD, pp. 136–143. IEEE (2015)
39.
Wegener, I.: Branching Programs and Binary Decision Diagrams. Discrete Mathematics and Applications. SIAM, SIAM Monographs on Philadelphia (2000)CrossRefMATH
40.
Wimmer, K., Wimmer, R., Scholl, C., Becker, B.: Skolem functions for DQBF (extended version). Technical report, FreiDok plus, Universitätsbibliothek Freiburg, Freiburg im Breisgau, Germany, June 2016. https://​www.​freidok.​uni-freiburg.​de
41.
Metadaten
Titel
Skolem Functions for DQBF
verfasst von
Karina Wimmer
Ralf Wimmer
Christoph Scholl
Bernd Becker
Copyright-Jahr
2016
Buch
Automated Technology for Verification and Analysis

Print ISBN: 978-3-319-46519-7

Electronic ISBN: 978-3-319-46520-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46520-3_25