nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications

Extended Abstract

verfasst von : Christoph Scholl, Ralf Wimmer

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

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

Dependency quantified Boolean formulas (DQBFs) as a generalization of quantified Boolean formulas (QBFs) have received considerable attention in research during the last years. Here we give an overview of the solution methods developed for DQBF so far. The exposition is complemented with the discussion of various applications that can be handled with DQBF solving.

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

Nächstes Kapitel Approximately Propagation Complete and Conflict Propagating Constraint Encodings

Abramovici, M., Breuer, M.A., Friedman, A.D.: Digital Systems Testing and Testable Design. Computer Science Press, New York (1990)

Ayari, A., Basin, D.: Qubos: deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X_12CrossRef

Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theoret. Comput. Sci. 523, 86–100 (2014). https://doi.org/10.1016/j.tcs.2013.12.020MathSciNetCrossRefMATH

Beineke, L.W., Little, C.H.C.: Cycles in bipartite tournaments. J. Comb. Theory Ser. B 32(2), 140–145 (1982). https://doi.org/10.1016/0095-8956(82)90029-6MathSciNetCrossRefMATH

Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 490–499. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_30CrossRef

Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005). https://doi.org/10.1007/11527695_5CrossRefMATH

Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101–115. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_10CrossRef

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). https://doi.org/10.1007/978-3-642-54013-4_1CrossRef

Bubeck, U.: Model-based transformations for quantified Boolean formulas. Ph.D. thesis, University of Paderborn, Germany (2010)

10.

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). https://doi.org/10.1007/11814948_21CrossRefMATH

11.

Cai, M., Deng, X., Zang, W.: A min-max theorem on feedback vertex sets. Math. Oper. Res. 27(2), 361–371 (2002). https://doi.org/10.1287/moor.27.2.361.328MathSciNetCrossRefMATH

12.

Chatterjee, K., Henzinger, T.A., Otop, J., Pavlogiannis, A.: Distributed synthesis for LTL fragments. In: FMCAD 2013, pp. 18–25. IEEE, October 2013. https://doi.org/10.1109/FMCAD.2013.6679386

13.

Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). https://doi.org/10.1007/11499107_5CrossRefMATH

14.

Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243–251. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_19CrossRef

15.

Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: International Workshop on Pragmatics of SAT (POS) 2012, Trento, Italy (2012)

16.

Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Le Berre, D. (ed.) International Workshop on Pragmatics of SAT (POS) 2014. EPiC Series, vol. 27, pp. 103–116. EasyChair, Vienna (2014)

17.

Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified Boolean formulae. In: ICCD 2013, Asheville, NC, USA, pp. 396–403. IEEE CS, October 2013. https://doi.org/10.1109/ICCD.2013.6657071

18.

Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: DATE 2015, Grenoble, France. IEEE, March 2015. https://doi.org/10.7873/date.2015.0098

19.

Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 85–98. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_9CrossRef

20.

Guo, J., Hüffner, F., Moser, H.: Feedback arc set in bipartite tournaments is NP-complete. Inf. Process. Lett. 102(2–3), 62–65 (2007). https://doi.org/10.1016/j.ipl.2006.11.016MathSciNetCrossRefMATH

21.

Henkin, L.: Some remarks on infinitely long formulas. In: Infinitistic Methods: Proceedings of the 1959 Symposium on Foundations of Mathematics, Warsaw, Panstwowe, pp. 167–183. Pergamon Press, September 1961

22.

Jain, A., Boppana, V., Mukherjee, R., Jain, J., Fujita, M., Hsiao, M.S.: Testing, verification, and diagnosis in the presence of unknowns. In: IEEE VLSI Test Symposium (VTS) 2000, Montreal, Canada, pp. 263–270. IEEE Computer Society (2000). https://doi.org/10.1109/VTEST.2000.843854

23.

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

24.

Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, Buenos Aires, Argentina, pp. 325–331. AAAI Press (2015). http://ijcai.org/Abstract/15/052

25.

Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2–3), 71–76 (2010)

26.

Lonsing, F., Egly, U.: Incremental QBF solving by DepQBF. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 307–314. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44199-2_48CrossRef

27.

Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_34CrossRef

28.

Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time: preliminary report. In: STOC 1973, pp. 1–9. ACM Press (1973). https://doi.org/10.1145/800125.804029

29.

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). https://doi.org/10.1016/S0898-1221(00)00333-3MathSciNetCrossRefMATH

30.

Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: Annual Symposium on Foundations of Computer Science (FOCS), San Juan, Puerto Rico, pp. 348–363. IEEE Computer Society, October 1979. https://doi.org/10.1109/SFCS.1979.25

31.

Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Annual Symposium on Foundations of Computer Science 1990, St. Louis, Missouri, USA, pp. 746–757. IEEE Computer Society, October 1990. https://doi.org/10.1109/FSCS.1990.89597

32.

Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 314–325. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_20CrossRef

33.

Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: DAC 2001, Las Vegas, NV, USA, pp. 238–243. ACM Press, June 2001. https://doi.org/10.1145/378239.378471

34.

Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999). https://doi.org/10.1109/12.769433MathSciNetCrossRef

35.

Wimmer, K., Wimmer, R., Scholl, C., Becker, B.: Skolem functions for DQBF. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 395–411. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_25CrossRefMATH

36.

Wimmer, R., Gitina, K., Nist, J., Scholl, C., Becker, B.: Preprocessing for DQBF. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 173–190. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_13CrossRef

37.

Wimmer, R., Karrenbauer, A., Becker, R., Scholl, C., Becker, B.: From DQBF to QBF by dependency elimination. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 326–343. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_21CrossRef

38.

Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 473–489. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_29CrossRef

39.

Wimmer, R., Wimmer, K., Scholl, C., Becker, B.: Analysis of incomplete circuits using dependency quantified Boolean formulas. In: Reis, A.I., Drechsler, R. (eds.) Advanced Logic Synthesis, pp. 151–168. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-67295-3_7CrossRef

40.

Wolsey, L.A.: Integer Programming. Wiley-Interscience, New York (1998)MATH

Titel: Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
verfasst von: Christoph Scholl
Ralf Wimmer
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2018
Print ISBN: 978-3-319-94143-1

Electronic ISBN: 978-3-319-94144-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94144-8_1

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"