Homepage

Constraint (Logic) Programming with Sets

LSET is a constraint language for expressing and solving quantifier-free first-order formulas over a universe of finite sets.

It was initially defined as part of the Constraint Logic Programming language CLP(SET) [1].

Basically, LSET provides a very general form of extensional sets, namely untyped hereditarily finite hybrid sets, where one or more set elements can be variables. Hereditarily finite sets are sets whose elements can be other hereditarily finite sets; while hybrid sets are sets whose elements can be non-set objects of any type. Sets can be manipulated through the usual set-theoretical operators (e.g., set equality, membership, union, inclusion, etc) which are provided in the form of (set) constraints. In particular, set equality among sets is implemented by set unification [2]. Constraint satisfiability is checked by a complete constraint solver (actually, a decision procedure for LSET formulas).

Over the years, LSET has been extended with various new features, leading to new
versions of the original constraint language:

  • LSET+FD: adding intervals and FD-constraints (i.e., integer arithmetic over Finite
    Domains) [3]
  • LBR: adding binary relations and partial functions [4]
  • LCP: adding Cartesian products [5]
  • LRIS: adding restricted intensional sets [6].

LSET, along with all its extensions, has been implemented in two distinct tools:

  – {log} (pronounced ‘setlog’), a Prolog library and interactive interpreter for  a CLP language extending Prolog  ({log} home page)

  – JSetL, a Java library supporting declarative (constraint) programming in  O-O programming (JSetL home page).

Main papers related to LSET (for more specific papers about {log} and JSetL visit their respective web pages)

  1. A. Dovier, C. Piazza, E. Pontelli, and G. Rossi.
    Sets and Constraint Logic Programming.
    ACM Transaction on Programming Language and Systems, Vol. 22 (5), Sept. 2000,
    861-931.
  2. A. Dovier, E. Pontelli, and G. Rossi.
    Set Unification.
    Theory and Practice of Logic Programming (ISSN: 1471-0684), 6(6):645-701, 2006
  3. A. Dal Palu’, A. Dovier, E. Pontelli, and G. Rossi.
    Integrating Finite Domain Constraints and CLP with Sets.
    In D. Miller, ed., Fifth ACM-SIGPLAN Conference on Principles and Practice of
    Declarative Programming, ACM Press (ISBN/ISSN: 1-58113-705-2), 2003, 219-229.
  4. Maximiliano Cristiá, Gianfranco Rossi.
    Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary
    Relations.
    Journal of Automated Reasoning. In press. 2019.
  5. Maximiliano Cristiá, Gianfranco Rossi
    A Set Solver for Finite Set Relation Algebra.
    In: J. Desharnais, W. Guttmann, S. Joosten (Eds),
    Relational and Algebraic Methods in Computer Science (RAMICS 2018).
    Lecture Notes in Computer Science, Vol. 11194, Springer International
    Publishing (ISSN: 0302-9743), 333-349, 2018.
  6. Maximiliano Cristiá, Gianfranco Rossi
    A Decision Procedure for Restricted Intensional Sets.
    In: L. de Moura (Ed.), Automated Deduction – CADE 26,
    Lecture Notes in Artificial Intelligence, Vol. 10395,
    Springer International Publishing ( ISSN: 0302-9743), 186-201, 2017

Rewrite rules for constraint solving

The following documents list in an abstract compact way all the rewrite rules used in the constraint solver for:

   – LBR formulas (here)

   – LRIS formulas (here)