摘要：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.
