Name
Abstract | ||
|---|---|---|
A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. The resolution hardness numbers give for \\(m=1,2,\\dots \\) 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. We achieve this by a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for formulas and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-58475-7_30 | CP |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tomás Peitl | 1 | 6 | 4.82 |
| Stefan Szeider | 2 | 1341 | 99.97 |