Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas

ABSTRACT. Canonical (logic) programs} (CP) refer to \emph{normal} programs (LP) augmented with connective $not\ not$. In this paper we address the question of whether CP are \emph{succinctly incomparable} with \emph{propositional formulas} (PF). Our main result shows that the PARITY problem, which can be polynomially represented in PF, \emph{only} has exponential representations in CP. In other words, PARITY \emph{separates} PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable when translating a set of formulas in PF into an equivalent program in CP (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 $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$), it follows that the two formalisms are indeed succinctly incomparable. In addition, we show that PARITY separates logic programs with \emph{cardinality constraints} and \emph{choice rules} (CC) from CP. Moreover, assuming $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$, CP and \emph{definite causal theories} (DT) are succinctly incomparable, \emph{two-valued} programs (TV) are strictly more succinct than CP and DT.