Representing normal programs with clauses
Tomi Janhunen · 2004
Similar problems are solvable by formulating them as classical satisfiability (SAT) problems and using SAT solvers. However, such formulations tend to be more difficult and less concise. E.g., formulating an AI planning problem is much easier as a normal logic program [6] than as a set of clauses [12]. This indicates of a real difference in expressive power which can be established formally by showing that normal programs cannot be translated into sets of clauses in a faithful and modular way [20, 10, 11]. In spite of these intranslatability results, we develop a faithful and non-modular, but still fairly systematic, translation from normal programs into sets of clauses. Using a novel characterization of stable models based on level numberings, the time complexity remains sub-quadratic.