{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:29:33Z","timestamp":1740547773324,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205890"},{"type":"electronic","value":"9783540245803"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-24580-3_19","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T23:01:46Z","timestamp":1283727706000},"page":"116-130","source":"Crossref","is-referenced-by-count":3,"title":["Heuristic-Based Backtracking for Propositional Satisfiability"],"prefix":"10.1007","author":[{"given":"A.","family":"Bhalla","sequence":"first","affiliation":[]},{"given":"I.","family":"Lynce","sequence":"additional","affiliation":[]},{"given":"J. T.","family":"de Sousa","sequence":"additional","affiliation":[]},{"given":"J.","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-45349-0_36","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"L. Baptista","year":"2000","unstructured":"Baptista, L., Marques-Silva, J.P.: Using randomization and learning to solve hard real-world instances of satisfiability. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 489\u2013494. Springer, Heidelberg (2000)"},{"key":"19_CR2","unstructured":"Bayardo Jr., R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the National Conference on Artificial Intelligence, July 1997, pp. 203\u2013208 (1997)"},{"key":"19_CR3","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theoremproving. Communications of the Association for Computing Machinery\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the Association for Computing Machinery"},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"19_CR5","unstructured":"Gaschnig, J.: Performance Measurement and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Pittsburgh, PA (May 1979)"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1613\/jair.1","volume":"1","author":"M. Ginsberg","year":"1993","unstructured":"Ginsberg, M.: Dynamic backtracking. Journal of Artificial Intelligence Research\u00a01, 25\u201346 (1993)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Ginsberg, M., McAllester, D.: GSAT and dynamic backtracking. In: Proceedings of the International Conference on Principles of Knowledge and Reasoning, pp. 226\u2013237 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50117-2"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust sat-solver. In: Proceedings of the Design and Test in Europe Conference, March 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"19_CR9","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the National Conference on Artificial Intelligence, July 1998, pp. 431\u2013437 (1998)"},{"key":"19_CR10","unstructured":"Lynce, I., Marques-Silva, J.P.: Complete unrestricted backtracking algorithms for satisfiability. In: Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, May 2002, pp. 214\u2013221 (2002)"},{"issue":"5","key":"19_CR11","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP-A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, June 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"19_CR13","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"Prosser, P.: Hybrid algorithms for the constraint satisfaction problems. Computational Intelligence\u00a09(3), 268\u2013299 (1993)","journal-title":"Computational Intelligence"},{"issue":"4","key":"19_CR14","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1023\/A:1006362926464","volume":"24","author":"E.T. Richards","year":"2000","unstructured":"Richards, E.T., Richards, B.: Non-systematic search and no-good learning. Journal of Automated Reasoning\u00a024(4), 483\u2013533 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR15","unstructured":"Selman, B., Kautz, H.: Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In: Proceedings of the International Joint Conference on Artificial Intelligence, August 1993, pp. 290\u2013295 (1993)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. Stallman","year":"1977","unstructured":"Stallman, R.M., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence\u00a09, 135\u2013196 (1977)","journal-title":"Artificial Intelligence"},{"key":"19_CR17","unstructured":"Yokoo, M.: Weak-commitment search for solving satisfaction problems. In: Proceedings of the National Conference on Artificial Intelligence, pp. 313\u2013318 (1994)"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24580-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T15:52:14Z","timestamp":1740498734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24580-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205890","9783540245803"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24580-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}