Canonical logic programs are succinctly incomparable with propositional formulas

Canonical (logic) programs (CP) refer to the class of normal programs (LP) augmented with connective not not, and are equally expressive as propositional formulas (PF). In this paper we address the question of whether CP and PF are succinctly incomparable. Our main result shows that the PARITY problem only has exponential CP representations, while it can be polynomially represented in PF. In other words, PARITY separates PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable when translating a set of PF formulas into a (logically) equivalent CP program (without introducing new variables). Furthermore, since it has been shown by Lifschitz and Razborov that there is also a problem which separates CP from PF (assuming P ⊈ NC1/poly), it follows that the two formalisms are indeed succinctly incomparable.