Top

Published in:

2020 | OriginalPaper | Chapter

Four Flavors of Entailment

Authors : Sibylle Möhle, Roberto Sebastiani, Armin Biere

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

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a novel approach for enumerating partial models of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples. We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Trail Saving on Backtrack

next chapter Designing New Phase Selection Heuristics

Bernasconi, A., Ciriani, V., Luccio, F., Pagli, L.: Compact DSOP and partial DSOP forms. Theory Comput. Syst. 53(4), 583–608 (2013). https://doi.org/10.1007/s00224-013-9447-2MathSciNetMATHCrossRef

Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14CrossRef

Biere, A., Hölldobler, S., Möhle, S.: An abstract dual propositional model counter. In: YSIP, CEUR Workshop Proceedings, vol. 1837, pp. 17–26. CEUR-WS.org (2017)

Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 191–207. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_17CrossRef

Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)MathSciNetMATHCrossRef

Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)MathSciNetMATHCrossRef

Galindo, J.A., Acher, M., Tirado, J.M., Vidal, C., Baudry, B., Benavides, D.: Exploiting the enumeration of all feature model configurations: a new perspective with distributed computing. In: SPLC, pp. 74–78. ACM (2016)

Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 260–265. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72200-7_23CrossRef

Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions SAT solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 275–289. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30494-4_20CrossRef

10.

Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 391–408. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-40922-X_22CrossRef

11.

Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D’ Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177–192. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_16

12.

Lagniez, J., Marquis, P.: A recursive algorithm for projected model counting. In: AAAI. pp. 1536–1543. AAAI Press (2019)

13.

Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_39CrossRef

14.

Li, B., Hsiao, M.S., Sheng, S.: A novel SAT all-solutions solver for efficient preimage computation. In: DATE, pp. 272–279. IEEE Computer Society (2004)

15.

Lonsing, F., Egly, U.: Incremental QBF solving. In: O’ Sullivan, Barry (ed.) CP 2014. LNCS, vol. 8656, pp. 514–530. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_38

16.

Marques-Silva, J.: Computing with SAT oracles: past, present and future. In: Manea, F., Miller, R.G., Nowotka, D. (eds.) CiE 2018. LNCS, vol. 10936, pp. 264–276. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94418-0_27CrossRef

17.

Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetMATHCrossRef

18.

McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_19CrossRef

19.

Möhle, S., Biere, A.: Dualizing projected model counting. In: Tsoukalas, L.H., Grégoire, É., Alamaniotis, M. (eds.) ICTAI 2018, pp. 702–709. IEEE (2018)

20.

Möhle, S., Biere, A.: Backing backtracking. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 250–266. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_18CrossRef

21.

Möhle, S., Biere, A.: Combining conflict-driven clause learning and chronological backtracking for propositional model counting. In: GCAI, EPiC Series in Computing, vol. 65, pp. 113–126. EasyChair (2019)

22.

Morettin, P., Passerini, A., Sebastiani, R.: Efficient weighted model integration via SMT-based predicate abstraction. In: IJCAI, pp. 720–728. ijcai.org (2017)

23.

Morettin, P., Passerini, A., Sebastiani, R.: Advanced SMT techniques for weighted model integration. Artif. Intell. 275, 1–27 (2019)MathSciNetMATHCrossRef

24.

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC, pp. 530–535. ACM (2001)

25.

Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_7CrossRef

26.

Oztok, U., Darwiche, A.: An exhaustive DPLL algorithm for model counting. J. Artif. Intell. Res. 62, 1–32 (2018)MathSciNetMATHCrossRef

27.

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

28.

Sebastiani, R.: Are you satisfied by this partial assignment? https://arxiv.org/abs/2003.04225

29.

Sebastiani, R.: Lazy satisfiability modulo theories. JSAT 3(3–4), 141–224 (2007)MathSciNetMATH

30.

Sheng, S., Hsiao, M.S.: Efficient preimage computation using a novel success-driven ATPG. In: DATE, pp. 10822–10827. IEEE Computer Society (2003)

31.

Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_36CrossRef

32.

Tibebu, A.T., Fey, G.: Augmenting all solution SAT solving for circuits with structural information. In: DDECS, pp. 117–122. IEEE (2018)

33.

Toda, T., Soh, T.: Implementing efficient all solutions SAT solvers, ACM J. Exp. Algorithmics, 21(1), 1.12:1–1.12:44 (2016)

34.

Zengler, C., Küchlin, W.: Boolean quantifier elimination for automotive configuration – a case study. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 48–62. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41010-9_4CrossRef

Title: Four Flavors of Entailment
Authors: Sibylle Möhle
Roberto Sebastiani
Armin Biere
Publisher: Springer International Publishing
Book: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner