{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T17:57:01Z","timestamp":1773511021056,"version":"3.50.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2020,5,3]],"date-time":"2020-05-03T00:00:00Z","timestamp":1588464000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001602","name":"Science Foundation Ireland","doi-asserted-by":"publisher","award":["12\/RC\/2289-P2"],"award-info":[{"award-number":["12\/RC\/2289-P2"]}],"id":[{"id":"10.13039\/501100001602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["12\/RC\/2289-P2"],"award-info":[{"award-number":["12\/RC\/2289-P2"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM J. Exp. Algorithmics"],"published-print":{"date-parts":[[2020,12,6]]},"abstract":"<jats:p>\n            When creating benchmarks for satisfiability (SAT) solvers, we need Conjunctive Normal Form (CNF) instances that are easy to build but hard to solve. A recent development in the search for such methods has led to the Balanced SAT algorithm, which can create\n            <jats:italic>k<\/jats:italic>\n            -CNF instances with\n            <jats:italic>m<\/jats:italic>\n            clauses of high difficulty, for arbitrary\n            <jats:italic>k<\/jats:italic>\n            and\n            <jats:italic>m<\/jats:italic>\n            . In this article, we introduce the No-Triangle CNF algorithm, a CNF instance generator based on the cluster coefficient graph statistic. We empirically compare the two algorithms by fixing the arity and the number of variables, but varying the number of clauses. We find that the hardest instances produced by each method belong to different constrainedness regions. In the 3-CNF case, for example, hard No-Triangle CNF instances reside in the highly-constrained region (many clauses), while Balanced SAT instances obtained from the same parameters are easy to solve. This allows us to generate difficult instances where existing algorithms fail to do so.\n          <\/jats:p>","DOI":"10.1145\/3385651","type":"journal-article","created":{"date-parts":[[2020,5,4]],"date-time":"2020-05-04T18:55:08Z","timestamp":1588618508000},"page":"1-12","source":"Crossref","is-referenced-by-count":1,"title":["Generating Difficult CNF Instances in Unexplored Constrainedness Regions"],"prefix":"10.1145","volume":"25","author":[{"given":"Guillaume","family":"Escamocher","sequence":"first","affiliation":[{"name":"Insight Centre for Data Analytics, School of Computer Science 8 IT, University College Cork, Ireland"}]},{"given":"Barry","family":"O'Sullivan","sequence":"additional","affiliation":[{"name":"Insight Centre for Data Analytics, School of Computer Science 8 IT, University College Cork, Ireland"}]},{"given":"Steven David","family":"Prestwich","sequence":"additional","affiliation":[{"name":"Insight Centre for Data Analytics, School of Computer Science 8 IT, University College Cork, Ireland"}]}],"member":"320","published-online":{"date-parts":[[2020,5,3]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications","author":"Achlioptas Dimitris","unstructured":"Dimitris Achlioptas . 2009. Random satisfiability . In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications , Vol. 185 . IOS Press , 245--270. DOI:https:\/\/doi.org\/10.3233\/978-1-58603-929-5-245 10.3233\/978-1-58603-929-5-245 Dimitris Achlioptas. 2009. Random satisfiability. In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 245--270. DOI:https:\/\/doi.org\/10.3233\/978-1-58603-929-5-245"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/75"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213018400018"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.)","volume":"1","author":"Balint Adrian","year":"2018","unstructured":"Adrian Balint . 2018 . Random k-SAT q-planted solutions . In Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.) , Vol. B-2018- 1 . University of Helsinki, 64. Adrian Balint. 2018. Random k-SAT q-planted solutions. In Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.), Vol. B-2018-1. University of Helsinki, 64."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 11th International Symposium on Combinatorial Search, SOCS 2018","author":"Balyo Tom\u00e1s","year":"2018","unstructured":"Tom\u00e1s Balyo and Luk\u00e1s Chrpa . 2018 . Using algorithm configuration tools to generate hard SAT benchmarks . In Proceedings of the 11th International Symposium on Combinatorial Search, SOCS 2018 , Stockholm, Sweden\u201414- -15 July 2018, Vadim Bulitko and Sabine Storandt (Eds.). AAAI Press, 133--137. https:\/\/aaai.org\/ocs\/index.php\/SOCS\/SOCS18\/paper\/view\/17952. Tom\u00e1s Balyo and Luk\u00e1s Chrpa. 2018. Using algorithm configuration tools to generate hard SAT benchmarks. In Proceedings of the 11th International Symposium on Combinatorial Search, SOCS 2018, Stockholm, Sweden\u201414--15 July 2018, Vadim Bulitko and Sabine Storandt (Eds.). AAAI Press, 133--137. https:\/\/aaai.org\/ocs\/index.php\/SOCS\/SOCS18\/paper\/view\/17952."},{"key":"e_1_2_1_6_1","volume-title":"Treengeling and YalSAT entering the SAT competition","author":"Biere Armin","year":"2018","unstructured":"Armin Biere . 2018. CaDiCaL, Lingeling, Plingeling , Treengeling and YalSAT entering the SAT competition 2018 . In Proc. of SAT Competition 2018\u2014Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.), Vol. B-2018- 1 . University of Helsinki , 13--14. Armin Biere. 2018. CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In Proc. of SAT Competition 2018\u2014Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.), Vol. B-2018-1. University of Helsinki, 13--14."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence","author":"Cheeseman Peter C.","year":"1991","unstructured":"Peter C. Cheeseman , Bob Kanefsky , and William M. Taylor . 1991. Where the really hard problems are . In Proceedings of the 12th International Joint Conference on Artificial Intelligence . Sydney, Australia, August 24--30 , 1991 , John Mylopoulos and Raymond Reiter (Eds.). Morgan Kaufmann, 331--340. http:\/\/ijcai.org\/Proceedings\/91-1\/Papers\/052.pdf. Peter C. Cheeseman, Bob Kanefsky, and William M. Taylor. 1991. Where the really hard problems are. In Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24--30, 1991, John Mylopoulos and Raymond Reiter (Eds.). Morgan Kaufmann, 331--340. http:\/\/ijcai.org\/Proceedings\/91-1\/Papers\/052.pdf."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_9_1","volume-title":"Cooper and Stanislav Zivny","author":"Martin","year":"2011","unstructured":"Martin C. Cooper and Stanislav Zivny . 2011 . Tractable triangles. In Proceedings of the 17th International Conference of Principles and Practice of Constraint Programming,CP 2011, Perugia, Italy, September 12--16, 2011. (Lecture Notes in Computer Science), Jimmy Ho-Man Lee (Ed.), Vol. 6876 . Springer , 195--209. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23786-7_17 10.1007\/978-3-642-23786-7_17 Martin C. Cooper and Stanislav Zivny. 2011. Tractable triangles. In Proceedings of the 17th International Conference of Principles and Practice of Constraint Programming,CP 2011, Perugia, Italy, September 12--16, 2011. (Lecture Notes in Computer Science), Jimmy Ho-Man Lee (Ed.), Vol. 6876. Springer, 195--209. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23786-7_17"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(95)00046-1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v33i1.2395"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622591.1622594"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"e_1_2_1_14_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald E.","unstructured":"Donald E. Knuth . 2015. The Art of Computer Programming , Volume 4 , Fascicle 6: Satisfiability (1st ed.). Addison-Wesley Professional . Donald E. Knuth. 2015. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability (1st ed.). Addison-Wesley Professional."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1122667.1122669"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 10th National Conference on Artificial Intelligence","author":"Mitchell David G.","year":"1992","unstructured":"David G. Mitchell , Bart Selman , and Hector J. Levesque . 1992. Hard and easy distributions of SAT problems . In Proceedings of the 10th National Conference on Artificial Intelligence , San Jose, CA, July 12--16 , 1992 , William R. Swartout (Ed.). AAAI Press\/The MIT Press, 459--465. http:\/\/www.aaai.org\/Library\/AAAI\/1992\/aaai92-071.php. David G. Mitchell, Bart Selman, and Hector J. Levesque. 1992. Hard and easy distributions of SAT problems. In Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, July 12--16, 1992, William R. Swartout (Ed.). AAAI Press\/The MIT Press, 459--465. http:\/\/www.aaai.org\/Library\/AAAI\/1992\/aaai92-071.php."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_7"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/800133.804350"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of SAT Competition 2017 -- Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.)","volume":"1","author":"Spence Ivor","year":"2017","unstructured":"Ivor Spence . 2017 . Balanced random SAT benchmarks . In Proceedings of SAT Competition 2017 -- Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.) , Vol. B-2017- 1 . University of Helsinki, 53--54. Ivor Spence. 2017. Balanced random SAT benchmarks. In Proceedings of SAT Competition 2017 -- Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.), Vol. B-2017-1. University of Helsinki, 53--54."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746239"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1038\/30918"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385651","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:49Z","timestamp":1750199569000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385651"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,3]]},"references-count":21,"alternative-id":["10.1145\/3385651"],"URL":"https:\/\/doi.org\/10.1145\/3385651","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"value":"1084-6654","type":"print"},{"value":"1084-6654","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5,3]]}}}