Cardinality constraint programs

Abstract

We define the class of cardinality constraint logic programs and provide a formal stable model semantics for them. The class extends normal logic programs by allowing the use of cardinality constraints and conditional literals. We identify a decidable subset, omega-restricted programs, of the class. We show how the formal semantics can be extended to allow the use of evaluated function symbols, such as arithmetic builtin operators. The omega-restricted cardinality constraint programs have been implemented in the Smodels system.