A theorem by Lin and Zhao shows how to turn any nondisjunctive logic program, understood in accordance with the answer set semantics, into an equivalent set of propositional formulas. The set of formulas generated by this process can be significantly larger than the original program. In this note we show (assuming P 6 NC 1 =poly, a conjecture from the theory of computational complexity that is widely believed to be true) that this is inevitable: any equivalent translation from logic programs to propositional formulas involves a significant increase in size.

PS

ACM Transactions on Computational Logic, Vol. 7 (2006), pp. 261-268.

@article{lif04, title={Why Are There So Many Loop Formulas?}, author={Vladimir Lifschitz and Alexander Razborov}, volume={7}, journal={ACM Transactions on Computational Logic}, pages={261-268}, url="http://www.cs.utexas.edu/users/ai-lab?lif04", year={2006} }