FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

Technical Summary of "flingo — Instilling ASP Expressiveness into Linear Integer Constraints"

Problem Statement
Constraint Answer Set Programming (CASP) is a hybrid paradigm designed to handle numerical computations that exceed the scalability of standard Answer Set Programming (ASP) tools. While standard ASP relies on a grounding phase followed by solving, CASP delegates numerical constraints to a backend solver (typically following Satisfiability Modulo Theory principles) to avoid the grounding blow-up caused by large numerical domains. However, current CASP solvers, such as clingcon, suffer from a significant modeling gap: the specification of constraint atoms often aligns with the operational requirements of the numerical backend rather than the high-level declarative features of the ASP paradigm.

Specifically, when numerical attributes are represented as constraint variables in existing systems, several core ASP features are lost or become difficult to express:

1. Undefinedness: The ability to leave attributes undefined (as opposed to assigning a default value).
2. Default Values: The ability to declare default values that can be overridden by exceptions.
3. Non-deterministic Assignments: The ability to make non-deterministic choices regarding attribute values via choice rules.
4. Aggregates: The ability to use aggregates (e.g., sums, minimums) over constraint variables, particularly when those variables might be undefined.

Existing approaches, such as the logic of Here-and-There with constraints (HTc), have laid semantic foundations for undefinedness and aggregates, but lacked a comprehensive language definition and tool implementation that fully integrates these features into a standard CASP workflow.

Methodology
The authors introduce flingo, a new CASP system and language that extends clingo to incorporate the aforementioned ASP expressiveness directly into linear integer constraints. The methodology is grounded in the following components:

1. Semantic Foundation (HTc): The semantics of flingo are formalized using the Logic of Here-and-There with constraints (HTc). This framework allows for a distinction between "Here" (current knowledge) and "There" (potential knowledge), enabling the representation of undefined variables.

   • Undefinedness: Integer variables are undefined by default. A variable is only defined if it is "founded" (derived) through the rules of the program.
   • Strict vs. Non-Strict Aggregates: The language distinguishes between strict (&sus) and non-strict (&sum) operations.
     • &sus (Strict Sum): Requires all terms to be defined. If any variable is undefined, the constraint atom evaluates to false.
     • &sum (Non-Strict Sum): Discards undefined terms from the calculation (treating them as the neutral element, 0), mimicking standard ASP aggregate behavior.
   • Conditional Terms: flingo supports conditional terms of the form s : l1, ..., ln, where a product term s is used if the conjunction of literals holds, otherwise a default term (context-dependent) is used.

2. Syntax and Features:

   • Constraint Atoms: Supports &sum, &sus, &min, &max, and &df (defined) atoms.
   • Assignment Rules: Introduces rules of the form &fun{t1; ...; tn} =: s :- l1, ..., lm, which define the variable s based on the terms t1...tn only when the conditions are met and the source variables are defined.
   • Choice Rules for Integers: Supports range-based choice rules (e.g., &in{s1..s2} =: x) allowing non-deterministic assignment of integer variables.

3. Implementation and Translation:

   • The flingo solver is implemented as an extension of clingo using its theory interface.
   • Crucially, flingo uses clingcon as a backend. To achieve this, the system performs a series of eight linear-time rewriting transformations to translate flingo programs into standard clingcon programs.
   • This translation involves:
     • Replacing conditional terms with propositional atoms and auxiliary rules.
     • Converting &sum (non-strict) operations into &sus (strict) operations combined with rules that handle undefined variables by assigning them a neutral value (0) only when necessary for the backend.
     • Encoding &min and &max operations using &sus and auxiliary propositional atoms.
     • Ensuring that undefined variables in flingo do not result in multiple stable models in the backend by explicitly handling the "undefined" state.

Key Contributions

1. Language Design: The introduction of flingo, a language that unifies the declarative features of ASP (defaults, undefinedness, choice, aggregates) with the efficiency of numerical constraint solving.
2. Semantic Formalization: A rigorous definition of flingo semantics based on HTc, specifically addressing the handling of undefined integer variables and the distinction between strict and non-strict aggregates.
3. Translation Mechanism: A proven translation from flingo syntax to clingcon input format, demonstrating that the enhanced expressiveness can be realized using existing high-performance CASP backends.
4. Theoretical Properties: The paper establishes propositions showing the relationship between flingo and clingcon models. Notably, it demonstrates that flingo allows for non-monotonic reasoning over integer variables (e.g., a rule x = 1 :- &sus{y} = 1 yields an undefined x if y is undefined, whereas adding the fact &sus{y} = 1 makes x defined), a feature not possible in standard clingcon.

Results and Evaluation
The paper provides illustrative examples to demonstrate the utility of flingo:

• Tariff Example: Revisits a problem involving default tariffs and exceptions. flingo allows for a natural encoding where default values are assigned unless specific exceptions (e.g., steel) are defined, and tax income is calculated using non-strict sums that ignore undefined tariffs.
• Bike Configuration: A configuration problem involving a frame and an optional bag with price calculations. The example shows how flingo handles optional components, default price ranges, and the aggregation of prices, all while maintaining the "look and feel" of standard ASP.
• Empirical Claim: The authors state that flingo has been used to model configuration problems in the Coom configuration language. In these cases, flingo significantly outperforms clingo (without constraints) on problems with numeric attributes featuring large domains.

Significance
The paper claims that flingo bridges the gap between high-level ASP modeling and the operational requirements of numeric constraint solving. Its significance lies in:

• Preserving ASP Paradigm: It allows users to retain standard ASP modeling features (like defaults and aggregates) even when working with numerical constraints, avoiding the need to adapt models to the limitations of the constraint backend.
• Handling Undefinedness: It formally supports the concept of undefined variables in a constraint setting, which is crucial for modeling incomplete information and defaults.
• Practical Implementation: By translating to clingcon, it leverages the efficiency of state-of-the-art CASP solvers without requiring a completely new solver architecture, making the approach immediately applicable.

The authors note that while the current implementation relies on clingo's theory grammar, future work will focus on refining the input language and optimizing the translation process to further enhance scalability. The system is publicly available.