×

Trade-offs between time and memory in a tighter model of CDCL SAT solvers. (English) Zbl 1475.68343

Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 160-176 (2016).
Summary: A long line of research has studied the power of conflict-driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgotten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that captures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL without any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.
For the entire collection see [Zbl 1337.68009].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T05 Learning and adaptive systems in artificial intelligence
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Chaff
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM J. Comput. 31(4), 1184–1211 (2002). Preliminary version in STOC 2000 · Zbl 1004.03047 · doi:10.1137/S0097539700366735
[2] Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. SIAM J. Comput. 38(4), 1347–1363 (2008). Preliminary version in FOCS 2001 · Zbl 1169.03044 · doi:10.1137/06066850X
[3] Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40, 353–373 (2011). Preliminary version in SAT 2009 · Zbl 1214.68340
[4] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 399–404, July 2009
[5] Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203–208, July 1997
[6] Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 213–232, May 2012 · Zbl 1286.68180 · doi:10.1145/2213977.2213999
[7] Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2004). Preliminary version in IJCAI 2003 · Zbl 1080.68651
[8] Beame, P., Sabharwal, A.: Non-restarting SAT solvers with simple preprocessing can efficiently simulate resolution. In: Proceedings of the 28th National Conference on Artificial Intelligence (AAAI 2014), pp. 2608–2615. AAAI Press, July 2014
[9] Beck, C., Nordström, J., Tang, B.: Some trade-off results for polynomial calculus. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 813–822, May 2013 · Zbl 1293.03031 · doi:10.1145/2488608.2488711
[10] Ben-Sasson, E., Galesi, N.: Space complexity of random formulae in resolution. Random Struct. Algorithms 23(1), 92–109 (2003). Preliminary version in CCC 2001 · Zbl 1048.03046 · doi:10.1002/rsa.10089
[11] Ben-Sasson, E., Nordström, J.: Understanding space in proof complexity: separations and trade-offs via substitutions. In: Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS 2011). pp. 401–416, January 2011
[12] Ben-Sasson, E., Wigderson, A.: Short proofs are narrow–resolution madesimple. J. ACM 48(2), 149–169 (2001). Preliminary version in STOC 1999 · Zbl 1089.03507 · doi:10.1145/375827.375835
[13] Bennett, P., Bonacina, I., Galesi, N., Huynh, T., Molloy, M., Wollan, P.: Space proof complexity for random 3-CNFs. Technical report arXiv.org:1503.01613 , April 2015 · Zbl 1423.03242
[14] Blake, A.: Canonical Expressions in Boolean Algebra. Ph.D. thesis, University of Chicago (1937) · Zbl 0018.38601
[15] Bonacina, I.: Total space in resolution is at least width squared. In: Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), (to appear, July 2016) · Zbl 1387.03066
[16] Bonacina, I., Galesi, N., Thapen, N.: Total space in resolution. In: Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2014), pp. 641–650, October 2014 · Zbl 1402.03080 · doi:10.1109/FOCS.2014.74
[17] Bonet, M.L., Buss, S., Johannsen, J.: Improved separations of regular resolution from clause learning proof systems. J. Artif. Intell. Res. 49, 669–703 (2014) · Zbl 1361.68185
[18] Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: resolution refinements that characterize DLL-algorithms with clause learning. Logical Meth. Comput. Sci. 4(4:13), 1–28 (2008) · Zbl 1159.03009
[19] Buss, S.R., Kołodziejczyk, L.: Small stone in pool. Logical Meth. Comput. Sci. 10, 1–22 (2014) · Zbl 1336.03019
[20] Chvátal, V., Szemerédi, E.: Many hard examples for resolution. J. ACM 35(4), 759–768 (1988) · Zbl 0712.03008 · doi:10.1145/48014.48016
[21] Cook, S.A., Reckhow, R.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36–50 (1979) · Zbl 0408.03044 · doi:10.2307/2273702
[22] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[23] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[24] Esteban, J.L., Torán, J.: Space bounds for resolution. Inf. Comput. 171(1), 84–97 (2001). Preliminary versions of these results appeared in STACS 1999 and CSL 1999 · Zbl 1005.03009 · doi:10.1006/inco.2001.2921
[25] Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39(2–3), 297–308 (1985) · Zbl 0586.03010 · doi:10.1016/0304-3975(85)90144-6
[26] Hertel, P., Bacchus, F., Pitassi, T., Van Gelder, A.: Clause learning can effectively P-simulate general propositional resolution. In: Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI 2008), pp. 283–290, July 2008
[27] Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999). Preliminary version in ICCAD 1996 · Zbl 01935259 · doi:10.1109/12.769433
[28] 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). pp. 530–535, June 2001 · doi:10.1145/378239.379017
[29] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) · Zbl 1326.68164 · doi:10.1145/1217856.1217859
[30] Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175, 512–525 (2011). Preliminary version in CP 2009 · Zbl 1216.68235 · doi:10.1016/j.artint.2010.10.002
[31] Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209–219 (1987) · Zbl 0639.68093 · doi:10.1145/7531.8928
[32] Van Gelder, A.: Pool resolution and its relation to regular resolution and DPLL with clause learning. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 580–594. Springer, Heidelberg (2005) · Zbl 1143.68582 · doi:10.1007/11591191_40
[33] Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2001), pp. 279–285, November 2001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.