{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:33:18Z","timestamp":1760016798347},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727873"},{"type":"electronic","value":"9783540727880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72788-0_28","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T12:25:22Z","timestamp":1183033522000},"page":"294-299","source":"Crossref","is-referenced-by-count":114,"title":["A Lightweight Component Caching Scheme for Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Knot","family":"Pipatsrisawat","sequence":"first","affiliation":[]},{"given":"Adnan","family":"Darwiche","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F., Markov, I., Sakallah, K.: Force: a fast and easy-to-implement variable-ordering heuristic. In: Proc. of the 13th ACM Great Lakes Symposium on VLSI 2003, pp. 116\u2013119 (2003)","DOI":"10.1145\/764808.764839"},{"key":"28_CR2","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: AAAI\u201997, Providence, Rhode Island, pp. 203\u2013208 (1997), citeseer.ist.psu.edu\/article\/bayardo97using.html"},{"key":"28_CR3","volume-title":"Proc. of 18th Annual IEEE Conf. on Computational Complexity, Aarhus, Denmark","author":"P. Beame","year":"2003","unstructured":"Beame, P., et al.: Memoization and dpll: Formula caching proof systems. In: Proc. of 18th Annual IEEE Conf. on Computational Complexity, Aarhus, Denmark, IEEE Computer Society Press, Los Alamitos (2003), citeseer.ist.psu.edu\/beame03memoization.html"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Sinz, C.: Decomposing sat problems into connected components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a02 (2006)","DOI":"10.3233\/SAT190022"},{"key":"28_CR5","unstructured":"Darwiche, A.: New advances in compiling CNF to decomposable negational normal form. In: Proc. of European Conference on AI (2004)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/11499107_33","volume-title":"Theory and Applications of Satisfiability Testing","author":"V. Durairaj","year":"2005","unstructured":"Durairaj, V., Kalla, P.: Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 415\u2013422. Springer, Heidelberg (2005)"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"28_CR8","first-page":"25","volume":"1","author":"M.L. Ginsberg","year":"1993","unstructured":"Ginsberg, M.L.: Dynamic backtracking. Jrnl of Artf. Intel. Resrh.\u00a01, 25\u201346 (1993), ftp:\/\/ftp.cirl.uoregon.edu\/pub\/users\/ginsberg\/papers\/dynamic.ps.gz","journal-title":"Jrnl of Artf. Intel. Resrh."},{"key":"28_CR9","unstructured":"Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for sat. In: IJCAI\u201903, Acapulco, Mexico, pp. 1167\u20131172 (2003)"},{"key":"28_CR10","unstructured":"IBM: Ibm formal verification benchmark library, http:\/\/www.research.ibm.com\/haifa\/projects\/verification\/RB_Homepage\/fvbenchmarks.html"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1109\/ICCAD.1996.569607","volume-title":"Proceedings of IEEE\/ACM International Conference on Computer-Aided Design","author":"J.P. Marques-Silva","year":"1996","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of IEEE\/ACM International Conference on Computer-Aided Design, pp. 220\u2013227. IEEE Computer Society Press, Los Alamitos (1996), citeseer.ist.psu.edu\/article\/marques-silva96grasp.html"},{"key":"28_CR12","unstructured":"Pipatsrisawat, K., Darwiche, A.: SAT Solver Description: RSat"},{"key":"28_CR13","first-page":"157","volume-title":"Proc. of the 17th Natl. Conf. on AI","author":"J. Roberto","year":"2000","unstructured":"Roberto, J., Bayardo, J., Pehoushek, J.D.: Counting models using connected components. In: Proc. of the 17th Natl. Conf. on AI, pp. 157\u2013162. AAAI Press, Menlo Park (2000)"},{"key":"28_CR14","unstructured":"Rsat sat solver homepage, http:\/\/reasoning.cs.ucla.edu\/rsat"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"T. Sang","year":"2005","unstructured":"Sang, T., et al.: Combining component caching and clause learning for effective model counting. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, Springer, Heidelberg (2005)"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","first-page":"226","volume-title":"Theory and Applications of Satisfiability Testing","author":"P. Beame","year":"2005","unstructured":"Beame, P., Kautz, H., Sang, T.: Heuristics for Fast Exact Model Counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 226\u2013240. Springer, Heidelberg (2005)"},{"key":"28_CR17","unstructured":"SAT\u201905 Competition Homepage, http:\/\/www.satcompetition.org\/2005\/"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Stallman, R.M., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artf. Intel.\u00a09 (1977)","DOI":"10.1016\/0004-3702(77)90029-7"},{"key":"28_CR19","unstructured":"Velev, M. N.: Sat benchmark lib, www.miroslav-velev.com\/sat_benchmarks.html"},{"key":"28_CR20","unstructured":"Zhang, L., et al.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279\u2013285 (2001), citeseer.ist.psu.edu\/article\/zhang01efficient.html"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72788-0_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:05:09Z","timestamp":1605762309000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_28","relation":{},"subject":[]}}