2018/09/08 by Stefan Dantchev, Dantchev, Stefan, Nicola Galesi +3
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1809.02843
openalex publication_date 2018/09/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We investigate the size complexity of proofs in Res(s) -- an extension of Resolution working on s-DNFs instead of clauses -- for families of contradictions given in the \em unusual binary encoding. A motivation of our work is size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the k-Clique Principle, whose Resolution complexity is still unknown. Our main result is a nΩ(k) lower bound for the size of refutations of the binary k-Clique Principle in Res(\lfloor (1)/(2)log log n\rfloor). This improves the result of Lauria, Pudlák et al. [24] who proved the lower bound for Resolution, that is Res(1). Our second lower bound proves that in RES(s) for s≤ log(1)/(2-ε)(n), the shortest proofs of the BinPHPmn, requires size 2^n1-δ, for any δ>0. Furthermore we prove that BinPHPmn can be refuted in size 2Θ(n) in treelike Res(1), contrasting with the unary case, where PHPmn requires treelike RES(1) refutations of size 2Ω(n log n) [9,16]. Furthermore we study under what conditions the complexity of refutations in Resolution will not increase significantly (more than a polynomial factor) when shifting between the unary encoding and the binary encoding. We show that this is true, from unary to binary, for propositional encodings of principles expressible as a Π2-formula and involving \em total variable comparisons. We then show that this is true, from binary to unary, when one considers the functional unary encoding. Finally we prove that the binary encoding of the general Ordering principle OP -- with no total ordering constraints -- is polynomially provable in Resolution.