{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:38:09Z","timestamp":1750307889155,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,5,19]],"date-time":"2010-05-19T00:00:00Z","timestamp":1274227200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,5,19]]},"DOI":"10.1145\/1822327.1822333","type":"proceedings-article","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T14:35:31Z","timestamp":1279722931000},"page":"43-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Scalable formula decomposition for propositional satisfiability"],"prefix":"10.1145","author":[{"given":"Anthony","family":"Monnet","sequence":"first","affiliation":[{"name":"Universit\u00e9 du Qu\u00e9bec \u00e0 Montr\u00e9al, Montr\u00e9al, Canada"}]},{"given":"Roger","family":"Villemaire","sequence":"additional","affiliation":[{"name":"Universit\u00e9 du Qu\u00e9bec \u00e0 Montr\u00e9al, Montr\u00e9al, Canada"}]}],"member":"320","published-online":{"date-parts":[[2010,5,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"E.\n      Amir\n     and \n      S.\n      McIlraith\n    .\n  Solving satisfiability using decomposition and the most constrained subproblem (preliminary report)\n  . In H. Krautz and B. Selman editors LICS \n  2001\n   - Workshop on Theory and Applications of Satisfiability Testing (SAT 2001) volume \n  9\n   of \n  Electronic Notes in Discrete Mathematics pages \n  329\n  --\n  343\n  . \n  Elsevier 2001.  E. Amir and S. McIlraith. Solving satisfiability using decomposition and the most constrained subproblem (preliminary report). In H. Krautz and B. Selman editors LICS 2001 - Workshop on Theory and Applications of Satisfiability Testing (SAT 2001) volume 9 of Electronic Notes in Discrete Mathematics pages 329--343. Elsevier 2001.","DOI":"10.1016\/S1571-0653(04)00331-2"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/0608024"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(89)90031-0"},{"key":"e_1_3_2_1_4_1","first-page":"366","volume-title":"Computer Aided Verification, 19<sup>th<\/sup> International Conference, number 4590 in Lecture Notes in Computer Science","author":"Babi\u0107 D.","year":"2007","unstructured":"D. Babi\u0107 and A. J. Hu . Structural abstraction of software verification conditions . In W. Damm and H. Hermanns, editors, Computer Aided Verification, 19<sup>th<\/sup> International Conference, number 4590 in Lecture Notes in Computer Science , pages 366 -- 378 . Springer , 2007 . D. Babi\u0107 and A. J. Hu. Structural abstraction of software verification conditions. In W. Damm and H. Hermanns, editors, Computer Aided Verification, 19<sup>th<\/sup> International Conference, number 4590 in Lecture Notes in Computer Science, pages 366--378. Springer, 2007."},{"key":"e_1_3_2_1_5_1","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"Barrett C. W.","year":"2009","unstructured":"C. W. Barrett , R. Sebastiani , S. A. Seshia , and C. Tinelli . Satisfiability modulo theories . In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications , chapter 26, pages 825 -- 885 . IOS Press , 2009 . C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 26, pages 825--885. IOS Press, 2009."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_5"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 5<sup>th<\/sup> International Conference (TACAS '99)","author":"Biere A.","year":"1999","unstructured":"A. Biere , A. Cimatti , E. M. Clarke , and Y. Zhu . Symbolic model checking without BDDs . In R. Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5<sup>th<\/sup> International Conference (TACAS '99) , volume 1579 of Lecture Notes in Computer Science , pages 193 -- 207 . Springer , 1999 . A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In R. Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5<sup>th<\/sup> International Conference (TACAS '99), volume 1579 of Lecture Notes in Computer Science, pages 193--207. Springer, 1999."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/SAT190022","article-title":"Decomposing SAT problems into connected components. Journal On Satisfiability","volume":"2","author":"Biere A.","year":"2006","unstructured":"A. Biere and C. Sinz . Decomposing SAT problems into connected components. Journal On Satisfiability , Boolean Modeling and Computation , 2 : 201 -- 208 , 2006 . A. Biere and C. Sinz. Decomposing SAT problems into connected components. Journal On Satisfiability, Boolean Modeling and Computation, 2:201--208, 2006.","journal-title":"Boolean Modeling and Computation"},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Computer Science","first-page":"315","volume-title":"Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT","author":"Bjesse P.","year":"2003","unstructured":"P. Bjesse , J. H. Kukula , R. F. Damiano , T. Stanion , and Y. Zhu . Guiding SAT diagnosis with tree decompositions . In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT 2003 , volume 2919 of Lecture Notes in Computer Science , pages 315 -- 329 . Springer , 2004. P. Bjesse, J. H. Kukula, R. F. Damiano, T. Stanion, and Y. Zhu. Guiding SAT diagnosis with tree decompositions. In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT 2003, volume 2919 of Lecture Notes in Computer Science, pages 315--329. Springer, 2004."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00069-2"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(89)90037-4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88636-5_1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2004.1431257"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","first-page":"502","volume-title":"Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT","author":"E\u00e9n N.","year":"2003","unstructured":"N. E\u00e9n and N. S\u00f6rensson . An extensible sat-solver . In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT 2003 , volume 2919 of Lecture Notes in Computer Science , pages 502 -- 518 . Springer , 2004. N. E\u00e9n and N. S\u00f6rensson. An extensible sat-solver. In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing - 6<sup>th<\/sup> International Conference, SAT 2003, volume 2919 of Lecture Notes in Computer Science, pages 502--518. Springer, 2004."},{"key":"e_1_3_2_1_17_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-540-79719-7_7","volume-title":"Theory and Applications of Satisfiability Testing - SAT","author":"Eibach T.","year":"2008","unstructured":"T. Eibach , E. Pilz , and G. V\u00f6lkel . Attacking bivium using SAT solvers . In H. K. B\u00fcning and X. Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008 , 11<sup>th<\/sup> International Conference, volume 4996 of Lecture Notes in Computer Science , pages 63 -- 76 . Springer , 2008. T. Eibach, E. Pilz, and G. V\u00f6lkel. Attacking bivium using SAT solvers. In H. K. B\u00fcning and X. Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008, 11<sup>th<\/sup> International Conference, volume 4996 of Lecture Notes in Computer Science, pages 63--76. Springer, 2008."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/367072.367111"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00078-3"},{"key":"e_1_3_2_1_21_1","first-page":"305","volume-title":"Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence","author":"Grastien A.","year":"2007","unstructured":"A. Grastien , Anbulagan, J. Rintanen , and E. Kelareva . Diagnosis of discrete-event systems using satisfiability algorithms . In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence , pages 305 -- 310 . AAAI Press , 2007 . A. Grastien, Anbulagan, J. Rintanen, and E. Kelareva. Diagnosis of discrete-event systems using satisfiability algorithms. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, pages 305--310. AAAI Press, 2007."},{"key":"e_1_3_2_1_23_1","first-page":"1167","volume-title":"Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence","author":"Huang J.","year":"2003","unstructured":"J. Huang and A. Darwiche . A structure-based variable ordering heuristic for SAT. In G. Gottlob and T. Walsh, editors, IJCAI-03 , Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence , pages 1167 -- 1172 . Morgan Kaufmann , 2003 . J. Huang and A. Darwiche. A structure-based variable ordering heuristic for SAT. In G. Gottlob and T. Walsh, editors, IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, pages 1167--1172. Morgan Kaufmann, 2003."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00400-9"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.748202"},{"key":"e_1_3_2_1_26_1","first-page":"359","volume-title":"Planning as satisfiability","author":"Kautz H. A.","year":"1992","unstructured":"H. A. Kautz and B. Selman . Planning as satisfiability . In B. Neumann, editor, 10<sup>th<\/sup> European Conference on Artificial Intelligence, pages 359 -- 363 . Wiley , 1992 . H. A. Kautz and B. Selman. Planning as satisfiability. In B. Neumann, editor, 10<sup>th<\/sup> European Conference on Artificial Intelligence, pages 359--363. Wiley, 1992."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2004.67"},{"key":"e_1_3_2_1_28_1","first-page":"92","volume-title":"Proceedings of The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference","author":"Lin Z.","year":"2006","unstructured":"Z. Lin , Y. Zhang , and H. Hernandez . Fast SAT-based answet set solver . In Proceedings of The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference , pages 92 -- 97 . AAAI Press , 2006 . Z. Lin, Y. Zhang, and H. Hernandez. Fast SAT-based answet set solver. In Proceedings of The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, pages 92--97. AAAI Press, 2006."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213008003935"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_31_1","first-page":"395","volume-title":"VLSI in Computers and Processors","author":"Memik S. O.","year":"2002","unstructured":"S. O. Memik and F. Fallah . Accelerated SAT-based scheduling of control\/data flow graphs. In 20<sup>th<\/sup> International Conference on Computer Design , VLSI in Computers and Processors , pages 395 -- 400 . IEEE Computer Society , 2002 . S. O. Memik and F. Fallah. Accelerated SAT-based scheduling of control\/data flow graphs. In 20<sup>th<\/sup> International Conference on Computer Design, VLSI in Computers and Processors, pages 395--400. IEEE Computer Society, 2002."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_13"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.5.703"},{"key":"e_1_3_2_1_35_1","first-page":"574","volume-title":"Satisfiability-based detailed FPGA routing. In 12<sup>th<\/sup> International Conference on VLSI Design (VLSI Design","author":"Nam G.-J.","year":"1999","unstructured":"G.-J. Nam , K. A. Sakallah , and R. A. Rutenbar . Satisfiability-based detailed FPGA routing. In 12<sup>th<\/sup> International Conference on VLSI Design (VLSI Design 1999 ), pages 574 -- 577 . IEEE Computer Society , 1999. G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar. Satisfiability-based detailed FPGA routing. In 12<sup>th<\/sup> International Conference on VLSI Design (VLSI Design 1999), pages 574--577. IEEE Computer Society, 1999."},{"key":"e_1_3_2_1_36_1","first-page":"155","volume-title":"Proceedings of the 19<sup>th<\/sup> Conference on Systems Administration (LISA 2005","author":"Narain S.","year":"2005","unstructured":"S. Narain . Network configuration management via model finding . In Proceedings of the 19<sup>th<\/sup> Conference on Systems Administration (LISA 2005 ), pages 155 -- 168 . USENIX, 2005 . S. Narain. Network configuration management via model finding. In Proceedings of the 19<sup>th<\/sup> Conference on Systems Administration (LISA 2005), pages 155--168. USENIX, 2005."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(86)90023-4"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02906-6_57"},{"key":"e_1_3_2_1_39_1","unstructured":"The international SAT Competitions web page. http:\/\/www.satcompetition.org.  The international SAT Competitions web page. http:\/\/www.satcompetition.org."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0121-x"},{"key":"e_1_3_2_1_41_1","series-title":"Lecture Notes in Computer Science","first-page":"249","volume-title":"Parallel Processing and Applied Mathematics, 7<sup>th<\/sup> International Conference (PPAM","author":"Singer D.","year":"2007","unstructured":"D. Singer and A. Monnet . JaCk-SAT: A new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check . In R. Wyrzykowski, J. Dongarra, K. Karczewski, and J. Wasniewski, editors, Parallel Processing and Applied Mathematics, 7<sup>th<\/sup> International Conference (PPAM 2007 ), volume 4967 of Lecture Notes in Computer Science , pages 249 -- 258 . Springer , 2008. D. Singer and A. Monnet. JaCk-SAT: A new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check. In R. Wyrzykowski, J. Dongarra, K. Karczewski, and J. Wasniewski, editors, Parallel Processing and Applied Mathematics, 7<sup>th<\/sup> International Conference (PPAM 2007), volume 4967 of Lecture Notes in Computer Science, pages 249--258. Springer, 2008."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_23"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.536723"},{"key":"e_1_3_2_1_44_1","volume-title":"Automation of reasoning, Classical papers on computational logic","author":"Tseitin G. S.","year":"1983","unstructured":"G. S. Tseitin . On the complexity of proofs in propositional logics . In J. H. Siekmann and G. Wrightson, editors, Automation of reasoning, Classical papers on computational logic , volume 2 . Springer , 1983 . G. S. Tseitin. On the complexity of proofs in propositional logics. In J. H. Siekmann and G. Wrightson, editors, Automation of reasoning, Classical papers on computational logic, volume 2. Springer, 1983."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(02)00091-3"}],"event":{"name":"C3S2E '10: C* Conference on Computer Science & Software Engineering","sponsor":["ACM Association for Computing Machinery","BytePress","Concordia University Concordia University"],"location":"Montr\u00e9al Quebec Canada","acronym":"C3S2E '10"},"container-title":["Proceedings of the Third C* Conference on Computer Science and Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1822327.1822333","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1822327.1822333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:16Z","timestamp":1750258036000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1822327.1822333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,19]]},"references-count":44,"alternative-id":["10.1145\/1822327.1822333","10.1145\/1822327"],"URL":"https:\/\/doi.org\/10.1145\/1822327.1822333","relation":{},"subject":[],"published":{"date-parts":[[2010,5,19]]},"assertion":[{"value":"2010-05-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}