Finite-Choice Logic Programming

TL;DR

This paper introduces finite-choice logic programming, a new formalism that uses choice instead of negation to generate multiple solutions, providing a more direct semantics and efficient exploration of solution spaces.

Contribution

It proposes finite-choice logic programming, offering a least-fixed-point semantics, an exploration algorithm, and a practical implementation that outperforms existing answer set solvers.

Findings

The formalism captures all stable model semantics.

The algorithm correctly explores the solution space.

The Dusa language shows competitive performance.

Abstract

Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size.