Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas

TL;DR

This paper proves that canonical logic programs and propositional formulas are fundamentally different in their succinctness, with the PARITY problem exemplifying an exponential size gap, thus showing they are succinctly incomparable.

Contribution

The paper demonstrates that PARITY can be represented efficiently in propositional formulas but requires exponential size in canonical logic programs, establishing their succinct incomparability.

Findings

PARITY separates PF from CP with exponential size gap

CP and PF are succinctly incomparable due to problem separations

Language in NC^1/poly not representable by polynomial size CP programs

Abstract

\emph{Canonical (logic) programs} (CP) refer to normal logic programs 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 but \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 that separates CP from PF (assuming $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$), it follows that CP and PF are indeed succinctly incomparable. From the view of the theory of computation, the above result may also be considered as the separation of two \emph{models of computation}, i.e., we identify a language in $\mathsf{NC^1/poly}$ which is not in the set of languages computable by polynomial size CP programs.