{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:06Z","timestamp":1760202606210,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T00:00:00Z","timestamp":1267401600000},"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":[[2010,3]]},"abstract":"<jats:p>The satisfiability problem is known to be NP-Complete; therefore, there should be relatively small problem instances that take a very long time to solve. However, most of the smaller benchmarks that were once thought challenging, especially the satisfiable ones, can be processed quickly by modern SAT-solvers. We describe and make available a generator that produces both unsatisfiable and, more significantly, satisfiable formulae that take longer to solve than any others known. At the two most recent international SAT Competitions, the smallest unsolved benchmarks were created by this generator. We analyze the results of all solvers in the most recent competition when applied to these benchmarks and also present our own more focused experiments.<\/jats:p>","DOI":"10.1145\/1671970.1671972","type":"journal-article","created":{"date-parts":[[2010,2,2]],"date-time":"2010-02-02T13:33:51Z","timestamp":1265117631000},"source":"Crossref","is-referenced-by-count":12,"title":["sgen1"],"prefix":"10.1145","volume":"15","author":[{"given":"Ivor","family":"Spence","sequence":"first","affiliation":[{"name":"Queen's University Belfast, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,3,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.816218"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11554844_3"},{"key":"e_1_2_1_3_1","unstructured":"clasp. 2009. A conflict-driven no good learning answer set solver. http:\/\/www.cs.uni-potsdam.de\/clasp\/.  clasp. 2009. A conflict-driven no good learning answer set solver. http:\/\/www.cs.uni-potsdam.de\/clasp\/."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_5_1","unstructured":"Crawford J. M. Kearns M. J. and Shapire R. E. 1994. The minimal disagreement parity problem as a hard satisfiability problem. Tech. rep. Computational Intelligence Research Laboratory and AT&T Bell Labs.  Crawford J. M. Kearns M. J. and Shapire R. E. 1994. The minimal disagreement parity problem as a hard satisfiability problem. Tech. rep. Computational Intelligence Research Laboratory and AT&T Bell Labs."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_8_1","unstructured":"DIMACS. 1993. Satisfiability suggested format. ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/doc\/satformat.tex.  DIMACS. 1993. Satisfiability suggested format. ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/doc\/satformat.tex."},{"volume-title":"Proceedings of the 6th Annual Conference on Theory and Applications of Satisfiability Testing. Springer","author":"E\u00e9n N.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1562164.1562186"},{"key":"e_1_2_1_11_1","first-page":"1","article-title":"Hard satisfiable clause sets for benchmarking equivalence reasoning techniques","volume":"2","author":"Haanp\u00e4\u00e4 H.","year":"2006","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_16"},{"key":"e_1_2_1_13_1","unstructured":"Hirsch E. 2002. Random generator hgen2 of satisfiable formulas in 3-CNF. http:\/\/logic.pdmi.ras.ru\/~hirsch\/benchmarks\/.  Hirsch E. 2002. Random generator hgen2 of satisfiable formulas in 3-CNF. http:\/\/logic.pdmi.ras.ru\/~hirsch\/benchmarks\/."},{"volume-title":"The international conferences on theory and applications of satisfiability testing (sat). http:\/\/www.satisfiability.org.","year":"2009","author":"Hoos H. H.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Kirkpatrick S. Gelatt C. D. and Vecchi M. P. 1983. Optimization by simulated annealing. Science 220 4598 671--680.  Kirkpatrick S. Gelatt C. D. and Vecchi M. P. 1983. Optimization by simulated annealing. Science 220 4598 671--680.","DOI":"10.1126\/science.220.4598.671"},{"volume-title":"Proceedings of the 6th Annual Conference on Principles and Practice of Constraint Programming. Springer","author":"Krishnamachari B.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","unstructured":"le Berre D. 2009. The sat competitions. http:\/\/www.satcompetition.org.  le Berre D. 2009. The sat competitions. http:\/\/www.satcompetition.org."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_12"},{"volume-title":"Proceedings of the 20th Australian Joint Conference on Artificial Intelligence. Springer","author":"Pham D. N.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2006.08.002"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147034"},{"key":"e_1_2_1_22_1","unstructured":"Sinz C. 2008. SAT-Race 2008. http:\/\/baldur.iti.uka.de\/sat-race-2008.  Sinz C. 2008. SAT-Race 2008. http:\/\/baldur.iti.uka.de\/sat-race-2008."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852031"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","first-page":"173","DOI":"10.3233\/SAT190043","article-title":"tts: A SAT-solver for small, difficult instances","volume":"4","author":"Spence I.","year":"2008","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"e_1_2_1_25_1","unstructured":"Whitesitt J. E. 1995. Boolean Algebra and Its Applications. Dover Publications Mineola NY.  Whitesitt J. E. 1995. Boolean Algebra and Its Applications. Dover Publications Mineola NY."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.04.001"},{"volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification. Springer-Verlag","author":"Zhang L.","key":"e_1_2_1_27_1"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1671970.1671972","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1671970.1671972","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:24Z","timestamp":1750278384000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1671970.1671972"}},"subtitle":["A generator of small but difficult satisfiability benchmarks"],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":27,"alternative-id":["10.1145\/1671970.1671972"],"URL":"https:\/\/doi.org\/10.1145\/1671970.1671972","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"type":"print","value":"1084-6654"},{"type":"electronic","value":"1084-6654"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}