{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T04:41:18Z","timestamp":1711600878935},"reference-count":0,"publisher":"AI Access Foundation","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["jair"],"abstract":"A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper we introduce resolution hardness numbers; they give for m=1,2,... the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest for- mulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.<\/jats:p>","DOI":"10.1613\/jair.1.12589","type":"journal-article","created":{"date-parts":[[2021,9,24]],"date-time":"2021-09-24T00:15:13Z","timestamp":1632442513000},"page":"69-97","source":"Crossref","is-referenced-by-count":1,"title":["Finding the Hardest Formulas for Resolution"],"prefix":"10.1613","volume":"72","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-7799-1568","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8994-1656","authenticated-orcid":false,"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"16860","published-online":{"date-parts":[[2021,9,22]]},"container-title":["Journal of Artificial Intelligence Research"],"original-title":[],"link":[{"URL":"http:\/\/jair.org\/index.php\/jair\/article\/download\/12589\/26717","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/jair.org\/index.php\/jair\/article\/download\/12589\/26717","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,24]],"date-time":"2021-09-24T00:15:13Z","timestamp":1632442513000},"score":1,"resource":{"primary":{"URL":"http:\/\/jair.org\/index.php\/jair\/article\/view\/12589"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,22]]},"references-count":0,"URL":"https:\/\/doi.org\/10.1613\/jair.1.12589","relation":{},"ISSN":["1076-9757"],"issn-type":[{"value":"1076-9757","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,22]]}}}