nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Clause Size Reduction with all-UIP Learning

verfasst von : Nick Feng, Fahiem Bacchus

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

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

Almost all CDCL SAT solvers use the 1-UIP clause learning scheme for learning new clauses from conflicts, and our current understanding of SAT solving provides good reasons for using that scheme. In particular, the 1-UIP scheme yields asserting clauses, and these asserting clauses have minimum LBD among all possible asserting clauses. As a result of these advantages, other clause learning schemes, like i-UIP and all-UIP, that were proposed in early work are not used in modern solvers. In this paper, we propose a new technique for exploiting the all-UIP clause learning scheme. Our technique is to employ all-UIP learning under the constraint that the learnt clause’s LBD does not increase (over the minimum established by the 1-UIP clause). Our method can learn clauses that are significantly smaller than the 1-UIP clause while preserving the minimum LBD. Unlike previous clause minimization methods, our technique is not limited to learning a sub-clause of the 1-UIP clause. We show empirically that our method can improve the performance of state of the art solvers.

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 Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving

Nächstes Kapitel Trail Saving on Backtrack

The idea of UIP clauses was first mentioned in [19], and 1-UIP clauses along with other UIP clauses were learnt and used in the earlier GRASP SAT solver.

In this example, the fourth clause on \(\lnot d\)’s watch list subsumes the third clause. But it is not difficult to construct more elaborate examples where there are no subsumed clauses and we still obtain learnt clauses that are duplicates of clauses already in the formula.

Knuth in his sat13 CDCL solver [7] uses an all-decision clause when the 1-UIP clause is too large. In this context an all-UIP clause could also be used as it would be no larger than the all decision clause.

Since the sole remaining literal \(u\in L_i\) is at a lower trail index than all of the other literals there is no point in trying to resolve away u—either it will be the decision literal for level i having no reason, or its reason will contain at least one other literal at level i.

Other more powerful minimization techniques could still be applied.

So extra techniques used by the underlying solver, like reason side rate and locality [8], were kept intact.

Applying DRAT-trim multiple times can further reduce the proof size until a fix-point. However, the full optimization is too time consuming for our experiments.

Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, 11–17 July 2009, pp. 399–404 (2009). http://ijcai.org/Proceedings/09/Papers/074.pdf

Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2004). https://doi.org/10.1613/jair.1410MathSciNetCrossRefMATH

Biere, A.: CADICAL at the SAT race 2019. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2019 Solver and Benchmark Descriptions. University of Helsinki (2019). http://hdl.handle.net/10138/306988

Biere, A.: Cadical SAT solver (2019). https://github.com/arminbiere/cadical

Bayardo Jr, R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, 27–31 July 1997, Providence, Rhode Island, USA, pp. 203–208. AAAI Press/The MIT Press (1997). http://www.aaai.org/Library/AAAI/1997/aaai97-032.php

Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 343–356. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_27CrossRefMATH

Knuth, D.E.: Implementation of algorithm 7.2.2.2c (conflict-driven clause learning SAT solver). https://www-cs-faculty.stanford.edu/~knuth/programs/sat13.w

Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_9CrossRefMATH

Liang, J.H., Oh, C., Ganesh, V., Czarnecki, K., Poupart, P.: Maple-COMSPS, MapleCOMSPS\_LRB, MapleCOMSPS\_CHB. In: Balyo, T., Heule, M.J.H., Järvisalo, M.J. (eds.) Proceedings of SAT Competition 2016 Solver and Benchmark Descriptions. University of Helsinki (2016). http://hdl.handle.net/10138/164630

10.

Luo, M., Li, C., Xiao, F., Manyà, F., Lü, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19–25 August 2017, pp. 703–711 (2017). ijcai.org, https://doi.org/10.24963/ijcai.2017/98

11.

Chowdhury, M.S., Müller, M., You, J.H.: Four CDCL SAT solvers based on exploration and glue variable bumping. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2019 Solver and Benchmark Descriptions. University of Helsinki (2019). http://hdl.handle.net/10138/306988

12.

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

13.

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18–22 June 2001, pp. 530–535. ACM (2001). https://doi.org/10.1145/378239.379017

14.

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

15.

Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011). https://doi.org/10.1016/j.artint.2010.10.002MathSciNetCrossRefMATH

16.

Ryvchin, V., Nadel, A.: Maple\_LCM\_Dist ChronoBT: featuring chronological backtracking. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2018 Solver and Benchmark Descriptions. University of Helsinki (2018). https://hdl.handle.net/10138/237063

17.

Sabharwal, A., Samulowitz, H., Sellmann, M.: Learning back-clauses in SAT. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 498–499. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_53CrossRef

18.

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

19.

Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, 10–14 November 1996, pp. 220–227. IEEE Computer Society/ACM (1996). https://doi.org/10.1109/ICCAD.1996.569607

20.

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.769433MathSciNetCrossRefMATH

21.

Sörensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 237–243. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_23CrossRef

22.

Kochemazov, S., Zaikin, O., Kondratiev, V., Semenov, A.: MapleLCMDistchronoBT-DL, duplicate learnts heuristic-aided solvers at the SAT race 2019. In: Heule, M.J.H., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2019 Solver and Benchmark Descriptions. University of Helsinki (2019). http://hdl.handle.net/10138/306988

23.

Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_31CrossRefMATH

24.

Wieringa, S., Heljanko, K.: Concurrent clause strengthening. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 116–132. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_10CrossRefMATH

25.

Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Ernst, R. (ed.) Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, 4–8 November 2001, pp. 279–285. IEEE Computer Society (2001). https://doi.org/10.1109/ICCAD.2001.968634

Titel: Clause Size Reduction with all-UIP Learning
verfasst von: Nick Feng
Fahiem Bacchus
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

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

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

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"