SAT Modulo Well-Founded Semantics: Extended Abstract

EasyChair Preprint 16031

Abstract

The well-founded semantics (WFS) yields a unique three-valued model for logic programs 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 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, as well as an efficient solving procedure.

Keyphrases: Least Fixpoint Computation, SAT, well-founded semantics

@booklet{EasyChair:16031,
  author    = {Thomas Eiter and Tobias Nießen and Davide Soldà},
  title     = {SAT Modulo Well-Founded Semantics: Extended Abstract},
  howpublished = {EasyChair Preprint 16031},
  year      = {EasyChair, 2026}}