SAT Modulo Well-Founded Semantics

Abstract

The well-founded semantics (WFS) for logic programs yields a unique three-valued model that serves as an efficient core for skeptical reasoning, but lacks built-in mechanisms for choice and case-based reasoning, limiting its expressiveness for problems such as decision making and planning. Propositional SAT solvers excel at combinatorial problems like the latter but, unlike WFS, do not naturally support reasoning under incomplete information or encoding transitive closure properties. We present an integration of a choice operator into WFS that preserves the suitability of the semantics for scalable, partial-information reasoning. From a propositional perspective, our semantics gracefully captures semantically unassigned atoms and constraints; we illustrate this approach in a setting for reasoning about actions under uncertainty. Furthermore, classical propositional satisfiability can not only be embedded into our framework, but now also be extended with reasoning over transitive closures. In terms of program evaluation, we show that the choice operator can be materialized by a SAT solver while propagating the consequences of choices through an extension of the alternating fixpoint algorithm for WFS with conflicts that are propagated back to the SAT solver. To further increase computational performance, we develop clause learning and syntactic decomposition techniques for logic programs with choices.