{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T03:44:40Z","timestamp":1774928680473,"version":"3.50.1"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,9,1]],"date-time":"2009-09-01T00:00:00Z","timestamp":1251763200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1007\/s10472-010-9173-2","type":"journal-article","created":{"date-parts":[[2010,2,24]],"date-time":"2010-02-24T11:10:45Z","timestamp":1267009845000},"page":"59-73","source":"Crossref","is-referenced-by-count":5,"title":["Dynamic symmetry-breaking for Boolean satisfiability"],"prefix":"10.1007","volume":"57","author":[{"given":"Fadi A.","family":"Aloul","sequence":"first","affiliation":[]},{"given":"Arathi","family":"Ramani","sequence":"additional","affiliation":[]},{"given":"Igor L.","family":"Markov","sequence":"additional","affiliation":[]},{"given":"Karem A.","family":"Sakallah","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,25]]},"reference":[{"issue":"9","key":"9173_CR1","doi-asserted-by":"crossref","first-page":"1117","DOI":"10.1109\/TCAD.2003.816218","volume":"22","author":"FA Aloul","year":"2003","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult sat instances in the presence of symmetry. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. (TCAD) 22(9), 1117\u20131137 (2003)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. (TCAD)"},{"key":"9173_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Generic ILP versus specialized 0\u20131 ILP: an update. In: Proc. Intl. Conf. on Computer-Aided Design (ICCAD), pp. 450\u2013457","DOI":"10.1145\/774572.774638"},{"key":"9173_CR3","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for Boolean satisfiability. In: Proc. Intl. Joint Conf. on AI, pp. 271\u2013282 (2003)","DOI":"10.1145\/775832.776042"},{"key":"9173_CR4","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Symmetry-breaking for pseudo-Boolean formulas. In: Proc. Asia-South Pacific Design Automation Conf., pp. 884\u2013887 (2004)","DOI":"10.1109\/ASPDAC.2004.1337720"},{"key":"9173_CR5","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. In: Proc. Design Automation Conf., pp. 830\u2013835 (2003)","DOI":"10.1145\/775832.776041"},{"key":"9173_CR6","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proc. of the Intl. Conf. on Principles of Knowledge Representation and Reasoning, pp. 148\u2013159 (1996)"},{"key":"9173_CR7","unstructured":"Darga, P.: SAUCY: graph automorphism tool. http:\/\/vlsicad.eecs.umich.edu\/BK\/SAUCY"},{"key":"9173_CR8","unstructured":"DIMACS SAT benchmarks: ftp:\/\/Dimacs.rutgers.EDU\/pub\/challenge\/sat\/benchmarks\/cnf"},{"key":"9173_CR9","doi-asserted-by":"crossref","unstructured":"Gent, I., Kelsey, T., Linton, S., McDonald, I., Miguel, I., Smith, B.: Conditional symmetry breaking. In: Proc. of Principles and Practice of Constraint Programming (CP), pp. 256\u2013270 (2005)","DOI":"10.1007\/11564751_21"},{"key":"9173_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust sat-solver. In: Proc. Design Automation and Test In Europe, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"9173_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proc. Design Automation Conf., pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9173_CR12","doi-asserted-by":"crossref","unstructured":"Nam, G., Aloul, F., Sakallah, K., Rutenbar, R.: A comparative study of two Boolean formulations of FPGA detailed routing constraints. In: Proc. Intl. Symposium on Physical Design (ISPD), pp. 222\u2013227 (2001)","DOI":"10.1145\/369691.369777"},{"key":"9173_CR13","unstructured":"Petrie, K., Smith, B., Yorke-Smith, N.: Dynamic symmetry breaking in constraint programming and linear programming hybrids. In: Proc. of STAIRS, the 2nd European Starting AI Researchers Symposium, pp. 96\u2013106 (2004)"},{"issue":"5","key":"9173_CR14","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: a new search algorithm for satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9173_CR15","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of Boolean sat procedures in the formal verification of superscalar and VLIW microprocessors. In: Proc. Design Automation Conf. (DAC), pp. 226\u2013231 (2001)","DOI":"10.1145\/378239.378469"},{"key":"9173_CR16","unstructured":"Zhang, L., Malik, S.: XOR-chain SAT benchmarks, SAT 2002 competition: http:\/\/www.satcompetition.org\/"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9173-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-010-9173-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9173-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T21:40:42Z","timestamp":1739914842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-010-9173-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["9173"],"URL":"https:\/\/doi.org\/10.1007\/s10472-010-9173-2","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9]]}}}