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:
Parameterized Compilation Lower Bounds for Restricted CNF-Formulas Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Dependency Schemes for DQBF

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

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

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counter examples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.

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 2QBF: Challenges and Solutions
Nächstes Kapitel Lifting QBF Resolution Calculi to DQBF
Fußnoten
1
In [16] there is an additional constraint ‘the resolvent of \(C_i\) and \(C_{i+1}\) w.r.t. \(l_i\) is non-tautologous’. This constraint has to be removed according to [25, 26]. If it is not removed, resolution path dependencies are not sound.
 
2
The construction does not lead to \((Z'_{x_1} \setminus \{y_1\})\)-paths and thus \((x_1,y_1)\in {{\mathrm{{{\mathrm{qdep}}}^{\mathrm {rp}}}}}(\psi )\) cannot be proven (which is not surprising due to Theorem 2).
 
3
For notational convenience, we use here \(\mathrm {dep}(v_i) = D_{v_i}\) if \(v_i\) is existential and \(\mathrm {dep}(v_i) = \{v_i\}\) if \(v_i\) is universal.
 
4
Our tool and all benchmarks we used are available at https://​projects.​informatik.​uni-freiburg.​de/​projects/​dqbf.
 
Literatur
1.
Ashar, P., Ganai, M.K., Gupta, A., Ivancic, F., Yang, Z.: Efficient SAT-based bounded model checking for software verification. In: Margaria, T., Steffen, B., Philippou, A., Reitenspieß, M. (eds.) International Symposium on Leveraging Applications of Formal Methods (ISoLA). Technical Report, vol. TR-2004-6, pp. 157–164, Department of Computer Science, University of Cyprus, Paphos, Cyprus, October 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.H.R.: Reducing satisfiability and reachability to DQBF, September 2015. Talk at the International Workshop on Quantified Boolean Formulas (QBF)
4.
Biere, A.: Resolve and expand. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)CrossRef
5.
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)CrossRef
6.
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
7.
Bubeck, U.: Model-based transformations for quantified boolean formulas. Ph.D. thesis, University of Paderborn (2010)
8.
Bubeck, U., Büning, H.K.: 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
9.
Bubeck, U., Kleine Büning, H.: Bounded universal expansion for preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244–257. Springer, Heidelberg (2007)CrossRef
10.
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Design 19(1), 7–34 (2001)CrossRefMATH
11.
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 Prog. 38(3–4), 185–202 (2010)CrossRefMATH
12.
Eggersglüß, S., Drechsler, R.: A highly fault-efficient SAT-based ATPG flow. IEEE Des. Test Comput. 29(4), 63–70 (2012)CrossRef
13.
Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243–251. Springer, Heidelberg (2014)
14.
Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: International Workshop on Pragmatics of SAT (POS), Trento, Italy (2012)
15.
16.
Van 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)CrossRef
17.
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, Asheville, October 2013
18.
Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Proceedings of DATE. IEEE, Grenoble, March 2015
19.
Lonsing, F., Biere, A.: Efficiently representing existential dependency sets for expansion-based QBF solvers. ENTCS 251, 83–95 (2009)MATH
20.
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)CrossRef
21.
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
22.
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
23.
24.
Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: ACM/IEEE Design Automation Conference (DAC), pp. 238–243. ACM Press, Las Vegas, June 2001
25.
Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 58–71. Springer, Heidelberg (2012)CrossRef
26.
27.
28.
29.
Metadaten
Titel
Dependency Schemes for DQBF
verfasst von
Ralf Wimmer
Christoph Scholl
Karina Wimmer
Bernd Becker
Copyright-Jahr
2016
Buch
Theory and Applications of Satisfiability Testing – SAT 2016

Print ISBN: 978-3-319-40969-6

Electronic ISBN: 978-3-319-40970-2

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40970-2_29