{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:58:25Z","timestamp":1760061505516,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_22","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"223-236","source":"Crossref","is-referenced-by-count":18,"title":["Dynamic Symmetry Breaking by Simulating Zykov Contraction"],"prefix":"10.1007","author":[{"given":"Bas","family":"Schaafsma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"van Maaren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient Symmetry Breaking for Boolean Satisfiability. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 271\u2013282 (2003)"},{"issue":"1-4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10472-007-9062-5","volume":"49","author":"C. Ans\u00f3tegui","year":"2007","unstructured":"Ans\u00f3tegui, C., Larrubia, J., Li, C.M., Many\u00e0, F.: Exploiting multivalued knowledge in variable selection heuristics for SAT solvers. Annals of Mathematics and Artificial Intelligence\u00a049(1-4), 191\u2013205 (2007)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"4","key":"22_CR3","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"S.A. Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeonhole principle using extended resolution. SIGACT News\u00a08(4), 28\u201332 (1976)","journal-title":"SIGACT News"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: Feasibly constructive proofs and the propositional calculus. In: Proceedings of STOC 1975, pp. 83\u201397 (1975)","DOI":"10.1145\/800116.803756"},{"issue":"7","key":"22_CR5","doi-asserted-by":"publisher","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 theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"22_CR6","doi-asserted-by":"publisher","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 ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","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, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"22_CR8","unstructured":"Gent, I.P.: Arc Consistency in SAT. In: Proceedings of the Fifteenth European Conference on Artificial Intelligence, ECAI 2002 (2002)"},{"key":"22_CR9","unstructured":"Gomes, C.P., Shmoys, D.B.: Completing Quasigroups or Latin Squares: A Structured Graph Coloring Problem. In: Proceedings of the Computational Symposium on Graph Coloring and Generalizations, Ithaca, USA, pp. 22\u201339 (2002)"},{"key":"22_CR10","unstructured":"Keur, A., Stevens, C., Voortman, M.: Symmetry Breaking Options in Conflict Driven SAT Solving. TU-delft technical report, http:\/\/www.st.ewi.tudelft.nl\/sat\/reports.php"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP \u2013 a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F.: Chaff: engineering an efficient SAT solve. In: Proceedings of DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"22_CR13","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","first-page":"26","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Prestwich","year":"2005","unstructured":"Prestwich, S.: Local Search on SAT-Encoded Colouring Problems. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 26\u201329. Springer, Heidelberg (2005)"},{"key":"22_CR15","unstructured":"Sakallah, K.A.: Symmetry and Satisfiability. In: Handbook of Satisfiability, ch. 10, pp. 289\u2013338 (2009)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C. Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended Resolution Proofs for Conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 600\u2013611. Springer, Heidelberg (2006)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Mathematics and Mathematical Logic, Part II, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"Journal of the ACM"},{"issue":"2","key":"22_CR19","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.dam.2006.07.016","volume":"156","author":"A. Gelder Van","year":"2008","unstructured":"Van Gelder, A.: Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics\u00a0156(2), 230\u2013243 (2008)","journal-title":"Discrete Applied Mathematics"},{"key":"22_CR20","first-page":"81","volume":"79","author":"A.A. Zykov","year":"1952","unstructured":"Zykov, A.A.: On some properties of linear complexes. Amer. Math. Soc. Translations\u00a079, 81 (1952)","journal-title":"Amer. Math. Soc. Translations"},{"key":"22_CR21","unstructured":"http:\/\/mat.gsia.cmu.edu\/COLOR\/solvers\/trick.c"},{"key":"22_CR22","unstructured":"Computational Series: Graph Coloring and Its Generalizations, http:\/\/mat.gsia.cmu.edu\/COLOR04"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T11:13:15Z","timestamp":1739185995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}