乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T00:22:26Z","timestamp":1720052546446},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T00:00:00Z","timestamp":1683849600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["J-4361N"],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Discrete Applied Mathematics"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1016\/j.dam.2023.05.003","type":"journal-article","created":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T03:50:26Z","timestamp":1684554626000},"page":"173-184","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Are hitting formulas hard for resolution?"],"prefix":"10.1016","volume":"337","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-7799-1568","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.dam.2023.05.003_b1","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","article-title":"Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas","volume":"43","author":"Aharoni","year":"1986","journal-title":"J. Combin. Theory Ser. A"},{"key":"10.1016\/j.dam.2023.05.003_b2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3152","article-title":"Clause-learning algorithms with many restarts and bounded-width resolution","volume":"40","author":"Atserias","year":"2011","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/j.dam.2023.05.003_b3","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","article-title":"Towards understanding and harnessing the potential of clause learning","volume":"22","author":"Beame","year":"2004","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/j.dam.2023.05.003_b4","series-title":"Graph Theory","volume":"vol. 244","author":"Bondy","year":"2008"},{"issue":"3","key":"10.1016\/j.dam.2023.05.003_b5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. ACM"},{"key":"10.1016\/j.dam.2023.05.003_b6","series-title":"Handbook of Satisfiability","first-page":"3","article-title":"A history of satisfiabilty","author":"Franco","year":"2021"},{"key":"10.1016\/j.dam.2023.05.003_b7","series-title":"SAT 2004 - the Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings","article-title":"Polynomial time SAT decision, hypergraph transversals and the Hermitian rank","author":"Galesi","year":"2004"},{"key":"10.1016\/j.dam.2023.05.003_b8","doi-asserted-by":"crossref","DOI":"10.1016\/j.artint.2021.103460","article-title":"New width parameters for SAT and #SAT","volume":"295","author":"Ganian","year":"2021","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.dam.2023.05.003_b9","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/j.dam.2023.05.003_b10","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1137\/0218026","article-title":"CNF-satisfiability test by counting and polynomial average time","volume":"18","author":"Iwama","year":"1989","journal-title":"SIAM J. Comput."},{"issue":"1\u20133","key":"10.1016\/j.dam.2023.05.003_b11","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0166-218X(00)00245-6","article-title":"On subclasses of minimal unsatisfiable formulas","volume":"107","author":"Kleine B\u00fcning","year":"2000","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/j.dam.2023.05.003_b12","series-title":"Proceedings for the Workshop on Theory and Applications of Satisfiability","article-title":"Satisfiable formulas closed under replacement","volume":"vol. 9","author":"Kleine B\u00fcning","year":"2001"},{"issue":"4","key":"10.1016\/j.dam.2023.05.003_b13","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1023\/A:1016339119669","article-title":"The complexity of read-once resolution","volume":"36","author":"Kleine B\u00fcning","year":"2002","journal-title":"Ann. Math. Artif. Intell."},{"issue":"2","key":"10.1016\/j.dam.2023.05.003_b14","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/S0166-218X(02)00405-5","article-title":"On the structure of some classes of minimal unsatisfiable formulas","volume":"130","author":"Kleine\u00a0B\u00fcning","year":"2003","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/j.dam.2023.05.003_b15","series-title":"Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure - Portofino, Italy, May 5-8, 2003 (SAT 2003)","article-title":"The combinatorics of conflicts between clauses","volume":"vol. 2919","author":"Kullmann","year":"2004"},{"key":"10.1016\/j.dam.2023.05.003_b16","series-title":"Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings","first-page":"352","article-title":"Green-Tao numbers and SAT","volume":"vol. 6175","author":"Kullmann","year":"2010"},{"issue":"1","key":"10.1016\/j.dam.2023.05.003_b17","first-page":"83","article-title":"Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure","volume":"109","author":"Kullmann","year":"2011","journal-title":"Fund. Inform."},{"key":"10.1016\/j.dam.2023.05.003_b18","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/j.tcs.2013.04.020","article-title":"On davis-putnam reductions for minimally unsatisfiable clause-sets","volume":"492","author":"Kullmann","year":"2013","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.dam.2023.05.003_b19","article-title":"Unsatisfiable hitting clause-sets with three more clauses than variables","author":"Kullmann","year":"2016","journal-title":"CoRR"},{"key":"10.1016\/j.dam.2023.05.003_b20","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/j.jsc.2013.09.003","article-title":"Practical graph isomorphism, {ii}","volume":"60","author":"McKay","year":"2014","journal-title":"J. Symbolic Comput."},{"issue":"7\u20138","key":"10.1016\/j.dam.2023.05.003_b21","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/s00236-007-0056-x","article-title":"Solving #sat using vertex covers","volume":"44","author":"Nishimura","year":"2007","journal-title":"Acta Inform."},{"key":"10.1016\/j.dam.2023.05.003_b22","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.tcs.2012.12.039","article-title":"Satisfiability of acyclic and almost acyclic CNF formulas","volume":"481","author":"Ordyniak","year":"2013","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.dam.2023.05.003_b23","series-title":"Saturated Minimally Unsatisfiable Formulas on Up to Ten Clauses","author":"Peitl","year":"2021"},{"key":"10.1016\/j.dam.2023.05.003_b24","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1613\/jair.1.12589","article-title":"Finding the hardest formulas for resolution","volume":"72","author":"Peitl","year":"2021","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/j.dam.2023.05.003_b25","series-title":"Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings","first-page":"654","article-title":"On the power of clause-learning SAT solvers with restarts","volume":"vol. 5732","author":"Pipatsrisawat","year":"2009"},{"issue":"1\u20132","key":"10.1016\/j.dam.2023.05.003_b26","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(94)00092-1","article-title":"On the hardness of approximate reasoning","volume":"82","author":"Roth","year":"1996","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.dam.2023.05.003_b27","series-title":"International Conference on Computer-Aided Design (ICCAD \u201996), November 10-14, 1996, San Jose, CA, USA","first-page":"220","article-title":"GRASP - A new search algorithm for satisfiability","author":"Silva","year":"1996"},{"issue":"1","key":"10.1016\/j.dam.2023.05.003_b28","first-page":"1","article-title":"Disjoint DNF tautologies with conflict bound two","volume":"4","author":"Sz\u00f6r\u00e9nyi","year":"2008","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.1016\/j.dam.2023.05.003_b29","series-title":"SageMath, the sage mathematics software system","author":"The Sage Developers","year":"2022"},{"issue":"1","key":"10.1016\/j.dam.2023.05.003_b30","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","article-title":"Hard examples for resolution","volume":"34","author":"Urquhart","year":"1987","journal-title":"J. ACM"},{"key":"10.1016\/j.dam.2023.05.003_b31","series-title":"Mathematical Logic in Asia","first-page":"302","article-title":"Complexity results on minimal unsatisfiable formulas","author":"Zhao","year":"2006"}],"container-title":["Discrete Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X23001749?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X23001749?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T03:07:06Z","timestamp":1711595226000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0166218X23001749"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10]]},"references-count":31,"alternative-id":["S0166218X23001749"],"URL":"https:\/\/doi.org\/10.1016\/j.dam.2023.05.003","relation":{},"ISSN":["0166-218X"],"issn-type":[{"value":"0166-218X","type":"print"}],"subject":[],"published":{"date-parts":[[2023,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Are hitting formulas hard for resolution?","name":"articletitle","label":"Article Title"},{"value":"Discrete Applied Mathematics","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.dam.2023.05.003","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2023 The Authors. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}