nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Speeding Up Assumption-Based SAT

verfasst von : Randy Hickey, Fahiem Bacchus

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

Assumption based SAT solving is an essential tool in many applications of SAT solving, especially in incremental SAT solving. For example, assumption based SAT solving is used when solving MaxSat, when computing minimal unsatisfiable subsets and minimal correction sets, and in various inductive verification applications. The MiniSat SAT solver introduced a simple technique for extending a SAT solver to allow it to handle assumptions by forcing the SAT solver to make the assumed literals its initial decisions. This approach persists in almost all current SAT solvers making it the most commonly used technique for handling assumptions. In this paper we explain some deficiencies in this approach that can hinder its efficiency, and provide a very simple modification that fixes these deficiencies. We show that our modification makes a non-trivial difference in practice, e.g., allowing two tested state of the art MaxSat solvers to solve 50+ new instances. This improvement is particularly useful since our modification is extremely simple to implement. We also examine the issue of repeated work when the solver backtracks over the assumptions, e.g., on restarts or when a new unit clause is learnt, and develop a new method for avoiding this repeated work that addresses some deficiencies of prior approaches.

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 Local Search for Fast Matrix Multiplication

Nächstes Kapitel Simplifying CDCL Clause Database Reduction

Quick checks to determine if C is already satisfied can be made first by checking data in the watch data structure (the blocking literal) and checking if the clause’s other watch is \( true \).

This description follows the MiniSat and Glucose schemes for watch literals, but this particular type of implementation is not necessary. Scanning \(O(n^2)\) literals in the clause down a single branch occurs with any implementation that stores no information about the previous scan [17].

It is not clear if this third technique is an improvement outside of the context of MUS extraction.

We save a reference to the reason clause, so before checking to see if the reason is still unit we must ensure that the references haven’t been changed by garbage collection, and that the implied literal is still at position zero in the reason clause (this is a MiniSat invariant for reason clauses).

Maxsat evaluation series: 2006–2016 http://www.maxsat.udl.cat/, 2017–2018 https://maxsat-evaluations.github.io/

Alviano, M., Dodaro, C., Ricca, F.: A MaxSat algorithm using cardinality constraints of bounded size. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 2677–2683 (2015). http://ijcai.org/Abstract/15/379

Ansótegui, C., Didier, F., Gabàs, J.: Exploiting the structure of unsatisfiable cores in MaxSat. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 283–289 (2015). http://ijcai.org/Abstract/15/046

Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_23CrossRefMATH

Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 27–31 July 2014, Québec City, Québec, Canada, pp. 835–841 (2014). http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8618

Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 70–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_5CrossRef

Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012). https://doi.org/10.3233/AIC-2012-0523MathSciNetCrossRefMATH

Belov, A., Marques-Silva, J.: Muser2: an efficient MUS extractor. JSAT 8(3/4), 123–128 (2012). https://satassociation.org/jsat/index.php/jsat/article/view/101MATH

Biere, A.: Cadical, Lingeling, Plingeling, Treengeling and YalSAT entering the sat competition 2018. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT COMPETITION 2018 Solver and Benchmark Descriptions. University of Helsinki (2018)

10.

Cabodi, G., Lavagno, L., Murciano, M., Kondratyev, A., Watanabe, Y.: Speeding-up heuristic allocation, scheduling and binding with sat-based abstraction/refinement techniques. ACM Trans. Design Autom. Electr. Syst. 15(2), 121–1234 (2010). https://doi.org/10.1145/1698759.1698762CrossRef

11.

Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, 22–25 October 2012, pp. 52–59 (2012). http://ieeexplore.ieee.org/document/6462555/

12.

Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Proceedings Principles and Practice of Constraint Programming - CP 2011–17th International Conference, CP 2011, Perugia, Italy, 12–16 September 2011, pp. 225–239 (2011). https://doi.org/10.1007/978-3-642-23786-7_19CrossRef

13.

Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Proceedings of the Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, 16–20 September 2013, pp. 247–262 (2013). https://doi.org/10.1007/978-3-642-40627-0_21

14.

Eén, N., Mishchenko, A., Amla, N.: A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, 20–23 October, pp. 181–188 (2010).http://ieeexplore.ieee.org/document/5770948/

15.

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). https://doi.org/10.1007/978-3-540-24605-3_37CrossRef

16.

Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003). https://doi.org/10.1016/S1571-0661(05)82542-3CrossRefMATH

17.

Gent, I.P.: Optimal implementation of watched literals and more general techniques. J. Artif. Intell. Res. 48, 231–251 (2013). https://doi.org/10.1613/jair.4016MathSciNetCrossRefMATH

18.

Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: a python-based MaxSat solver. In: Bacchus, F., Järvisalo, M., Martins, R. (eds.) MaxSAT Evaluation 2018 Solver and Benchmark Descriptions. University of Helsinki (2018)

19.

Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276–292. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_21CrossRef

20.

Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016). https://doi.org/10.1007/s10601-015-9183-0MathSciNetCrossRefMATH

21.

Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver^,. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_33CrossRef

22.

Mencía, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 1973–1979 (2015). http://ijcai.org/Abstract/15/280

23.

Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: Proceedings of the Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, 8–12 September 2014, pp. 564–573 (2014). https://doi.org/10.1007/978-3-319-10428-7_41

24.

Nadel, A., Ryvchin, V.: Efficient SAT Solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242–255. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_19CrossRefMATH

25.

Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 206–218. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_16CrossRefMATH

26.

Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSat resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, Québec City, Québec, Canada, 27–31 July 2014, pp. 2717–2723 (2014). http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8513

27.

Previti, A., Mencía, C., Järvisalo, M., Marques-Silva, J.: Improving MCS enumeration via caching. In: Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017–20th International Conference, Melbourne, VIC, Australia, 28 August–1 September 2017, pp. 184–194 (2017). https://doi.org/10.1007/978-3-319-66263-3_12CrossRef

28.

Saikko, P., Berg, J., Järvisalo, M.: LMHS: A SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539–546. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_34CrossRefMATH

29.

Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131–153. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-131

30.

Soos, M.: The cryptominisat 5.5 set of solvers at the sat competition 2018. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT COMPETITION 2018 Solver and Benchmark Descriptions. University of Helsinki (2018)

31.

van der Tak, P., Ramos, A., Heule, M.: Reusing the assignment trail in CDCL solvers. JSAT 7(4), 133–138 (2011). https://satassociation.org/jsat/index.php/jsat/article/view/89MathSciNetMATH

Titel: Speeding Up Assumption-Based SAT
verfasst von: Randy Hickey
Fahiem Bacchus
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_11

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