{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:42Z","timestamp":1760202702273,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2015,5,27]],"date-time":"2015-05-27T00:00:00Z","timestamp":1432684800000},"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":[[2015,12,15]]},"abstract":"<jats:p>For some time, the satisfiability formulae that have been the most difficult to solve for their size have been crafted to be unsatisfiable by the use of cardinality constraints. Recent solvers have introduced explicit checking of such constraints, rendering previously difficult formulae trivial to solve. A family of unsatisfiable formulae is described that is derived from the sgen4 family but cannot be solved using cardinality constraints detection and reasoning alone. These formulae were found to be the most difficult during the SAT2014 competition by a significant margin and include the shortest unsolved benchmark in the competition, sgen6-1200-5-1.cnf.<\/jats:p>","DOI":"10.1145\/2746239","type":"journal-article","created":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T15:13:25Z","timestamp":1433258005000},"page":"1-14","source":"Crossref","is-referenced-by-count":4,"title":["Weakening Cardinality Constraints Creates Harder Satisfiability Benchmarks"],"prefix":"10.1145","volume":"20","author":[{"given":"Ivor","family":"Spence","sequence":"first","affiliation":[{"name":"Queen's University Belfast, Belfast, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,5,27]]},"reference":[{"volume-title":"Retrieved","year":"2014","author":"Belov Anton","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"e_1_2_1_5_1","unstructured":"DIMACS. 1993. Satisfiability Suggested Format. www.satlib.org\/Benchmarks\/SAT\/satfomat.ps accessed 7th May 2015.  DIMACS. 1993. Satisfiability Suggested Format. www.satlib.org\/Benchmarks\/SAT\/satfomat.ps accessed 7th May 2015."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_7_1","unstructured":"Edward Hirsch. 2002. Random Generator hgen2 of Satisfiable Formulas in 3-CNF. Retrieved from http:\/\/logic.pdmi.ras.ru\/hirsch\/benchmarks\/.  Edward Hirsch. 2002. Random Generator hgen2 of Satisfiable Formulas in 3-CNF. Retrieved from http:\/\/logic.pdmi.ras.ru\/hirsch\/benchmarks\/."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v33i1.2395"},{"volume-title":"Proceedings of the 17th National Conference on Artificial Intelligence (AAAI'00)","year":"2000","author":"Li Chu Min","key":"e_1_2_1_9_1"},{"volume-title":"Theory and Applications of Satisfiability Testing SAT","year":"2014","author":"Mik\u0161a Mladen","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Richard Ostrowski \u00c9ric Gr\u00e9goire Bertrand Mazure and Lakhdar Sais. 2002. Recovering and exploiting structural knowledge from CNF formulas. In Principles and Practice of Constraint Programming (CP'02) Pascal Van Hentenryck (Ed.). 185--199.   Richard Ostrowski \u00c9ric Gr\u00e9goire Bertrand Mazure and Lakhdar Sais. 2002. Recovering and exploiting structural knowledge from CNF formulas. In Principles and Practice of Constraint Programming (CP'02) Pascal Van Hentenryck (Ed.). 185--199.","DOI":"10.1007\/3-540-46135-3_13"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1671970.1671972"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_37"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6377(98)00052-2"},{"key":"e_1_2_1_15_1","unstructured":"J. Eldon Whitesitt. 1995. Boolean Algebra and Its Applications. Dover Publications Mineola NY.  J. Eldon Whitesitt. 1995. Boolean Algebra and Its Applications. Dover Publications Mineola NY."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_18"}],"container-title":["ACM Journal of Experimental Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2746239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:44Z","timestamp":1750227404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,27]]},"references-count":16,"alternative-id":["10.1145\/2746239"],"URL":"https:\/\/doi.org\/10.1145\/2746239","relation":{},"ISSN":["1084-6654","1084-6654"],"issn-type":[{"type":"print","value":"1084-6654"},{"type":"electronic","value":"1084-6654"}],"subject":[],"published":{"date-parts":[[2015,5,27]]}}}