{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:03:58Z","timestamp":1742634238168},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_15","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"161-180","source":"Crossref","is-referenced-by-count":6,"title":["Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"C.A. Brown, L. Finkelstein, P.W. Purdom. Backtrack searching in the presence of symmetry. In \u201cApplied algebra, algebraic algorithms and error correcting codes\u201d. Sixth international conference, P. 99\u2013110. Springer-Verlag, 1988.","DOI":"10.1007\/3-540-51083-4_51"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"V. Chvatal, E. Szmeredi. Many hard examples for resolution. J. of the ACM,vol. 35, No 4, pp. 759\u2013568.","DOI":"10.1145\/48014.48016"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"W. Cook, C.R. Coullard, G. Turan. On the complexity of cutting planes proofs. Discrete Applied Mathematics, 18, 1987, 25\u201338.","journal-title":"Discrete Applied Mathematics"},{"key":"15_CR4","unstructured":"J. Crawford, M. Ginsberg, E. Luks, A. Roy. Symmetry breaking predicates for search problems. Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201996)."},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, D. Loveland. A Machine program for theorem proving. Communications of the ACM.-1962.-V. 5.-P. 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"E. Goldberg. Proving unsatisfiability of CNFs locally. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing.","DOI":"10.1016\/S1571-0653(04)00316-6"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken. The intractability of resolution. Theor. Comput. Sci. 39 (1985), 297\u2013308.","journal-title":"Theor. Comput. Sci"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"B. Krishnamurthy. Short proofs for tricky formulas. Acta Informatica 22 (1985) 253\u2013275.","journal-title":"Acta Informatica"},{"key":"15_CR9","unstructured":"D. Mitchell, B. Selman, and H.J. Levesque. Hard and easy distributions of SAT problems. Proceedings AAAI-92, San Jose,CA, 459\u2013465."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of DAC-2001.","DOI":"10.1145\/378239.379017"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"C. Papadimitriou. On selecting a satisfying truth assignment. Proceedings of FOC-91.","DOI":"10.1109\/SFCS.1991.185365"},{"key":"15_CR12","unstructured":"A. Roy. Symmetry breaking and fault tolerance in Boolean satisfiability. PhD thesis. Downloadable from http:\/\/www.cs.uoregon.edu\/~aroy\/"},{"key":"15_CR13","unstructured":"B. Selman, H. Kautz, B. Cohen. Noise strategies for improving local search. Proceedings of AAAI-94."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"I. Shlyakhter. Generating effective symmetry breaking predicates for search problems. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0166-218X(99)00039-6","volume":"96\u201397","author":"A. Urquhart","year":"1999","unstructured":"A. Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics 96\u201397(1999):177\u2013193,1999.","journal-title":"Discrete Applied Mathematics"},{"key":"15_CR16","unstructured":"H. Wong-Toi. Private communication."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:56:25Z","timestamp":1556740585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}