Properties and Applications of Programs with Monotone and Convex Constraints

TL;DR

This paper explores the properties of programs with monotone and convex constraints, extending logic programming concepts to improve understanding and computation of stable models, especially for aggregate-based programs.

Contribution

It introduces formal properties and characterizations for programs with monotone and convex constraints, enabling more efficient computation of stable models using existing solvers.

Findings

Provides characterizations of strong and uniform equivalence.

Extends Fages Lemma and program completion to these formalisms.

Enables faster stable model computation for lparse programs.

Abstract

We study properties of programs with monotone and convex constraints. We extend to these formalisms concepts and results from normal logic programming. They include the notions of strong and uniform equivalence with their characterizations, tight programs and Fages Lemma, program completion and loop formulas. Our results provide an abstract account of properties of some recent extensions of logic programming with aggregates, especially the formalism of lparse programs. They imply a method to compute stable models of lparse programs by means of off-the-shelf solvers of pseudo-boolean constraints, which is often much faster than the smodels system.