Name
Abstract | ||
|---|---|---|
AbstractA 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1613/jair.1.12589 | Hosted Content |
DocType | Volume | Issue |
Journal | 72 | 1 |
ISSN | Citations | PageRank |
1076-9757 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tomás Peitl | 1 | 6 | 4.82 |
| Stefan Szeider | 2 | 1341 | 99.97 |