{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:53Z","timestamp":1750308773167,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2008,6,1]],"date-time":"2008-06-01T00:00:00Z","timestamp":1212278400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM J. Exp. Algorithmics"],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:p>Many important tasks in design automation and artificial intelligence can be performed in practice via reductions to Boolean satisfiability (SAT). However, such reductions often omit application-specific structure, thus handicapping tools in their competition with creative engineers. Successful attempts to represent and utilize additional structure on Boolean variables include recent work on 0-1 integer linear programming (ILP) and symmetries in SAT. Those extensions gracefully accommodate well-known advances in SAT solving, however, no previous work has attempted to combine both extensions. Our work shows (i) how one can detect and use symmetries in instances of 0-1 ILP, and (ii) what benefits this may bring.<\/jats:p>","DOI":"10.1145\/1227161.1278375","type":"journal-article","created":{"date-parts":[[2008,10,8]],"date-time":"2008-10-08T13:57:58Z","timestamp":1223474278000},"page":"1-14","source":"Crossref","is-referenced-by-count":2,"title":["Symmetry breaking for pseudo-Boolean formulas"],"prefix":"10.1145","volume":"12","author":[{"given":"Fadi A.","family":"Aloul","sequence":"first","affiliation":[{"name":"American University of Sharjah, UAE"}]},{"given":"Arathi","family":"Ramani","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI"}]},{"given":"Igor L.","family":"Markov","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI"}]},{"given":"Karem A.","family":"Sakallah","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI"}]}],"member":"320","published-online":{"date-parts":[[2008,6,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774638"},{"volume-title":"Proceedings of the International Workshop on Symmetry on Constraint Satisfaction Problems. 1--12","author":"Aloul F.","key":"e_1_2_1_2_1","unstructured":"Aloul, F., Ramani, A., Markov, I. L., and Sakallah, K. 2003a. Symmetry-breaking for pseudo-Boolean formulas. In Proceedings of the International Workshop on Symmetry on Constraint Satisfaction Problems. 1--12."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.816218"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776042"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776041"},{"volume-title":"Proceedings of the International Conference Principles of Knowledge Representation and Reasoning. 148--159","author":"Crawford J.","key":"e_1_2_1_7_1","unstructured":"Crawford, J., Ginsberg, M., Luks, E., and Roy, A. 1996. Symmetry-breaking predicates for search problems. In Proceedings of the International Conference Principles of Knowledge Representation and Reasoning. 148--159."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/377810"},{"key":"e_1_2_1_9_1","volume-title":"SAUCY: Graph automorphism tool. Available at: http:\/\/www.eecs.umich. edu\/~pdarga\/pub\/auto\/saucy.html","author":"Darga P.","year":"2004","unstructured":"Darga, P. 2004. SAUCY: Graph automorphism tool. Available at: http:\/\/www.eecs.umich. edu\/~pdarga\/pub\/auto\/saucy.html"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_11_1","unstructured":"DIMACS Challenge Benchmarks. Available at: ftp:\/\/Dimacs.rutgers.EDU\/pub\/challenge\/sat\/benchmarks\/cnf"},{"volume-title":"The Theory of Groups. McMillan","author":"Hall M.","key":"e_1_2_1_12_1","unstructured":"Hall Jr. M. 1959. The Theory of Groups. McMillan, New York."},{"key":"e_1_2_1_13_1","unstructured":"ILOG CPLEX Available at: http:\/\/www.ilog.com\/products\/cplex"},{"key":"e_1_2_1_14_1","volume-title":"Congressus Numerantium 30","author":"McKay B.","year":"1981","unstructured":"McKay, B. 1981. Practical graph isomorphism. Congressus Numerantium 30, 45--87."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/369691.369777"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the International Workshop on Symmetry on Constraint Satisfaction Problems.","author":"Preswitch S.","year":"2002","unstructured":"Preswitch, S. 2002. Supersymmetric modelling for local search. In Proceedings of the International Workshop on Symmetry on Constraint Satisfaction Problems."},{"key":"e_1_2_1_19_1","unstructured":"SAT Competition. 2002. Available at: http:\/\/www.satcomp.org"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/199288.178090"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1227161.1278375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1227161.1278375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:37Z","timestamp":1750278157000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1227161.1278375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":18,"alternative-id":["10.1145\/1227161.1278375"],"URL":"https:\/\/doi.org\/10.1145\/1227161.1278375","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"type":"print","value":"1084-6654"},{"type":"electronic","value":"1084-6654"}],"subject":[],"published":{"date-parts":[[2008,6]]}}}