{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T04:33:10Z","timestamp":1772166790871,"version":"3.50.1"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2016,11,4]],"date-time":"2016-11-04T00:00:00Z","timestamp":1478217600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS KAKENHI","award":["26870011"],"award-info":[{"award-number":["26870011"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM J. Exp. Algorithmics"],"published-print":{"date-parts":[[2016,11,4]]},"abstract":"<jats:p>All solutions SAT (AllSAT for short) is a variant of the propositional satisfiability problem. AllSAT has been relatively unexplored compared to other variants despite its significance. We thus survey and discuss major techniques of AllSAT solvers. We accurately implemented them and conducted comprehensive experiments using a large number of instances and various types of solvers including a few publicly available software. The experiments revealed the solvers\u2019 characteristics. We made our implemented solvers publicly available so that other researchers can easily develop their solvers by modifying our code and comparing it with existing methods.<\/jats:p>","DOI":"10.1145\/2975585","type":"journal-article","created":{"date-parts":[[2016,11,4]],"date-time":"2016-11-04T12:49:04Z","timestamp":1478263744000},"page":"1-44","source":"Crossref","is-referenced-by-count":50,"title":["Implementing Efficient All Solutions SAT Solvers"],"prefix":"10.1145","volume":"21","author":[{"given":"Takahisa","family":"Toda","sequence":"first","affiliation":[{"name":"University of Electro-Communications, Tokyo, Japan"}]},{"given":"Takehide","family":"Soh","sequence":"additional","affiliation":[{"name":"Kobe University, Nada Kobe, Japan"}]}],"member":"320","published-online":{"date-parts":[[2016,11,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/170036.170072"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/645920.672836"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"e_1_2_1_4_1","first-page":"1562","article-title":"MINCE: A static global variable-ordering heuristic for SAT search and BDD manipulation","volume":"10","author":"Aloul Fadi A.","year":"2004","journal-title":"J. UCS"},{"key":"e_1_2_1_5_1","volume-title":"Principles and Practice of Constraint Programming--CP","author":"Andersen Henrik Reif","year":"2007"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/946243.946291"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence and 9th Conference on Innovative Applications of Artificial Intelligence (AAAI\u201997\/IAAI\u201997)","author":"Bayardo Roberto J.","year":"1867"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1714450.1714452"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of SAT Competition 2014; Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B","volume":"2","author":"Belov Anton","year":"2014"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.2015.0648"},{"key":"e_1_2_1_11_1","first-page":"2","article-title":"PicoSAT essentials","volume":"4","author":"Biere Armin","year":"2008","journal-title":"JSAT"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_13_1","volume-title":"Handbook of Satisfiability","author":"Biere Armin"},{"key":"e_1_2_1_14_1","volume-title":"In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV","author":"Brauer J\u00f6rg","year":"2011"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2009.5340173"},{"key":"e_1_2_1_17_1","first-page":"1","article-title":"Conflict-directed backjumping revisited","volume":"14","author":"Chen Xinguang","year":"2001","journal-title":"J. Artif. Int. Res."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"e_1_2_1_19_1","volume-title":"Hammer","author":"Crama Yves","year":"2011"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502091"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3000001.3000069"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00120-0"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, (SAT","volume":"2919","author":"E\u00e9n Niklas","year":"2003"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2007.04.017"},{"key":"e_1_2_1_25_1","volume-title":"The minimal hitting set generation problem: Algorithms and computation. CoRR abs\/1601.02939","author":"Gainer-Dewar Andrew","year":"2016"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"e_1_2_1_27_1","volume-title":"In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR","author":"Gebser Martin","year":"2007"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01929-6_7"},{"key":"e_1_2_1_29_1","volume-title":"In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD","author":"Grumberg Orna","year":"2004"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2011.05.002"},{"key":"e_1_2_1_31_1","volume-title":"Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1--3, 2000 Proceedings. Springer Berlin Heidelberg","author":"Gupta Aarti","year":"2000"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10618-006-0059-1"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 4th International Conference on Theory and Applications of Satisfiability Testing (SAT","volume":"63","author":"Holger Hoos H.","year":"2000"},{"key":"e_1_2_1_34_1","volume-title":"In Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR","author":"Hooker John N.","year":"2013"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_13"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622606.1622613"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2013.2288976"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2014.2359114"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/IRI.2014.7051971"},{"key":"e_1_2_1_40_1","volume-title":"In Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA","author":"Jabbour Sa\u00efd","year":"2014"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505515.2505577"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"HoonSang Jin HyoJung Han and Fabio Somenzi. 2005. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). Springer Berlin 287--300. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-31980-1_19  HoonSang Jin HyoJung Han and Fabio Somenzi. 2005. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). Springer Berlin 287--300. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-31980-1_19","DOI":"10.1007\/978-3-540-31980-1_19"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065775"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"David J. Johnson and Michael A. Trick (Eds.). 1996. Cliques Coloring and Satisfiability: Second DIMACS Implementation Challenge 1993. American Mathematical Society Boston MA.  David J. Johnson and Michael A. Trick (Eds.). 1996. Cliques Coloring and Satisfiability: Second DIMACS Implementation Challenge 1993. American Mathematical Society Boston MA.","DOI":"10.1090\/dimacs\/026"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on on Innovative Applications of Artificial Intelligence, 2000","author":"Bayardo Roberto J.","year":"2000"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.841068"},{"key":"e_1_2_1_48_1","volume-title":"The Art of Computer Programming: Combinatorial Algorithms, Part 1","author":"Knuth Donald E.","edition":"1"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Jean-Marie Lagniez and Pierre Marquis. 2016. On preprocessing techniques and their impact on propositional model counting. J. Automat. Reason. (2016) 1--69. DOI:http:\/\/dx.doi.org\/10.1007\/s10817-016-9370-8  Jean-Marie Lagniez and Pierre Marquis. 2016. On preprocessing techniques and their impact on propositional model counting. J. Automat. Reason. (2016) 1--69. DOI:http:\/\/dx.doi.org\/10.1007\/s10817-016-9370-8","DOI":"10.1007\/s10817-016-9370-8"},{"key":"e_1_2_1_50_1","volume-title":"A Symbolic Approach to Predicate Abstraction","author":"Lahiri Shuvendu K."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_39"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 2004 Design, Automation and Test in Europe Conference and Exposition (DATE 2004","author":"Li Bin","year":"2004"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789770.2789805"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (AAAI\u201998)","author":"Stephen","year":"1998"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_2_1_59_1","volume-title":"In Proceedings of the 14th International Conference on Computer Aided Verification (CAV","author":"McMillan Ken L.","year":"2002"},{"key":"e_1_2_1_60_1","volume-title":"Techniques of BDD\/ZDD: Brief history and recent activity. IEICE Transactions on Information and Systems 96-D, 7","year":"2013"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/1105924.1106049"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the 4th International Workshop on Algorithm Engineering and Experiments. Revised Papers. Springer","author":"DoRon"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2014.01.012"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/1768142.1768170"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1993.tb00310.x"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2345792"},{"key":"e_1_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Kavita Ravi and Fabio Somenzi. 2004. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2004). Springer Berlin 31--45. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-24730-2_3  Kavita Ravi and Fabio Somenzi. 2004. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2004). Springer Berlin 31--45. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-24730-2_3","DOI":"10.1007\/978-3-540-24730-2_3"},{"key":"e_1_2_1_70_1","volume-title":"In Proceedings of the 6th International Symposium on Algorithms and Computations (ISAAC\u201995)","author":"Sekine Kyoko","year":"1995"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022826"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_38"},{"key":"e_1_2_1_74_1","volume-title":"In Proceedings of the 12th International Symposium on Experimental Algorithms (SEA","author":"Toda Takahisa","year":"2013"},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Takahisa Toda. 2016. Dualization of boolean functions using ternary decision diagrams. Ann. Math. Artif. Intell. (2016) 1--16. DOI:http:\/\/dx.doi.org\/10.1007\/s10472-016-9520-z  Takahisa Toda. 2016. Dualization of boolean functions using ternary decision diagrams. Ann. Math. Artif. Intell. (2016) 1--16. DOI:http:\/\/dx.doi.org\/10.1007\/s10472-016-9520-z","DOI":"10.1007\/s10472-016-9520-z"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695941"},{"key":"e_1_2_1_77_1","volume-title":"Proceedings of the IEEE ICDM Workshop on Frequent Itemset Mining Implementations (FIMI\u201904)","volume":"126","author":"Uno Takeaki","year":"2004"},{"key":"e_1_2_1_78_1","volume-title":"Handbook of Knowledge Representation","author":"van Harmelen Frank"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2014.22"},{"key":"e_1_2_1_80_1","volume-title":"In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis. Springer","author":"Zhang Shuyuan","year":"2012"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2975585","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2975585","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:18Z","timestamp":1750218618000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2975585"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,4]]},"references-count":76,"alternative-id":["10.1145\/2975585"],"URL":"https:\/\/doi.org\/10.1145\/2975585","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"value":"1084-6654","type":"print"},{"value":"1084-6654","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,4]]}}}