{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:29Z","timestamp":1725512009033},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_11","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"119-132","source":"Crossref","is-referenced-by-count":5,"title":["A Decision-Making Procedure for Resolution-Based SAT-Solvers"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Advances in computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking (a book chapter). In: Zelkovitz, M. (ed.) Advances in computers, vol.\u00a058, Elsevier, Amsterdam (2003)"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Longemann, G., Loveland, D.: A Machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","first-page":"503","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 503\u2013518. Springer, Heidelberg (2004)"},{"key":"11_CR4","unstructured":"Fang, H., Ruml, W.: Complete Local Search for Propositional Satisfiability. In: Proc. of 19th National Conference on Artificial Intelligence, pp. 161\u2013166 (2004)"},{"issue":"2","key":"11_CR5","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1023\/A:1006143621319","volume":"23","author":"A.V. Gelder","year":"1999","unstructured":"Gelder, A.V.: Autarky pruning in propositional model elimination reduces failure redundancy. J. of Autom. Reasoning\u00a023(2), 137\u2013193 (1999)","journal-title":"J. of Autom. Reasoning"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11814948_11","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"E. Goldberg","year":"2006","unstructured":"Goldberg, E.: Determinization of resolution by an algorithm operating on complete assignments. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 90\u201395. Springer, Heidelberg (2006)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-Solver. In: DATE 2002, Paris, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"11_CR8","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proc. AAAI 1998 (1998)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Habet, D., Li, C.M., Devendeville, L., Vasquez, M.: A hybrid approach for SAT. In: Int. Conf. on Principles and Practice of Constraint Programming, pp. 172\u2013184 (2002)","DOI":"10.1007\/3-540-46135-3_12"},{"issue":"1-4","key":"11_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10472-004-9421-4","volume":"43","author":"E.A. Hirsch","year":"2005","unstructured":"Hirsch, E.A., Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Annals of Math. and Artif. Intell.\u00a043(1-4), 91\u2013111 (2005)","journal-title":"Annals of Math. and Artif. Intell."},{"key":"11_CR11","volume-title":"Stochastic Local Search: Foundations and Applications","author":"H. Hoos","year":"2004","unstructured":"Hoos, H., Stutzle, T.: Stochastic Local Search: Foundations and Applications. Morgan Kaufmann, San Francisco (CA) (2004)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Katz, J., Hanna, Z., Dershowitz, N.: Space-efficient Bounded Model Checking. In: DATE 2005, pp. 686\u2013687 (2005)","DOI":"10.1109\/DATE.2005.276"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","volume":"107","author":"O. Kullmann","year":"2000","unstructured":"Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics\u00a0107, 99\u2013137 (2000)","journal-title":"Discrete Applied Mathematics"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S0020-0190(99)00088-5","volume":"71","author":"C.M. Li","year":"1999","unstructured":"Li, C.M.: A constrained-based approach to narrow search trees for satisfiability. Information processing letters\u00a071, 75\u201380 (1999)","journal-title":"Information processing letters"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"Mazure, B., Sais, L., Gregoire, R.: Boosting complete techniques thanks to local search methods. Annals of Math. and Artif. Intell.\u00a022, 319\u2013331 (1998)","journal-title":"Annals of Math. and Artif. Intell."},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"Monien, B., Speckenmeyer, E.: Solving satisfiability in less than $\\mathit{2^n}$ steps. Discrete Applied Mathematics\u00a010, 287\u2013295 (1985)","journal-title":"Discrete Applied Mathematics"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"11_CR18","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M. Prasad","year":"2005","unstructured":"Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT\u00a07(2), 16\u2013173 (2005)","journal-title":"STTT"},{"key":"11_CR19","unstructured":"Prestwich, S.: Local search and backtracking vs. non-systematic backtracking. In: AAAI Fall Symposium on Using Uncertainty Within Computation, North Falmouth, Cape Cod, MA, November 2-4, 2001, pp. 109\u2013115 (2001)"},{"key":"11_CR20","unstructured":"Selman, B., Levesque, H., Mitchell, D.: A New Method for Solving Hard Satisfiability Problems. In: AAAI 1992, pp. 440\u2013446 (1992)"},{"key":"11_CR21","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: AAAI 1994, Seattle, pp. 337\u2013343 (1994)"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P.M. Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions of Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions of Computers"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: ICCAD 2001 (2001)","DOI":"10.1145\/774572.774637"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: International Conference on Automated Deduction, July 1997, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:08Z","timestamp":1619522948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_11","relation":{},"subject":[]}}