# On the Semantics of Hybrid ASP Systems Based on Clingo
## 6 Discussion and Related Work
### Black Box Orientation  
Black box approaches follow somehow similar steps to what happened in SAT with the _SAT modulo theories_ (SMT) [7] variant. SMT is defined as an extension to SAT where some atoms are replaced by formulas from some external theory expressible in first-order logic with equality, but usually without quantifiers (this includes numerical constraints but also covers data structures such as lists or strings). The key point in SMT is that the SAT solver does not really need to inspect the behavior of the external theory, so it can be treated as a black box. It is worth mentioning that, in fact, under the formalization proposed in the current paper, SMT can be seen as a particular case of AMT where all theory atoms are external (and we have no undefined variables) whereas, for each regular atom \(\mathsf{a}\), we include a choice rule such as (13), as we would do when emulating SAT inside ASP. Following similar steps to SMT, the combination of constraint programming (CP) and ASP gave birth to _Constraint Ansver Set Programming_ (CASP). As explained in survey [18], CASP covers a family of approaches whose implementation may rely either on integration of CP inside a native ASP engine or on a translation of CASP programs into SMT or CP instead. From the semantic point of view, most of them treat theory atoms as external. Moreover, a choice for the constraint atom or its complement is usually included in the definitions. Moreover, many approaches only allow constraint atoms in bodies, e.g., in [5; 19], or when they are used in rule heads [9], they just stand for syntactic sugar and can be shifted to bodies, as performed for clingcon-programs. Next, we briefly list some of the existing CASP systems (see [18] for more examples) and their distinctive features with respect to the AMT framework proposed in this paper. Three examples of tools based on translation to non-ASP solvers are dingo [20], mingo [21], and ezsmt [22]. As happens with clingol[dl], system dingo [20] deals with ASP modulo difference logic but is actually based on a translation into SMT. In dingo, theory atoms are not external (they need to be derived), but they do not completely fit into our category of _defined_ either, in the sense that SMT variables cannot be undefined. System ezsmt [22] is also based on a translation into SMT but accepts linear and non-linear constraints over mixed real and integer variables, whereas mingo [21] translates ASP modulo mixed-integer linear programming (MILP) to plain MILP. In these two systems, all theory atoms are external and may only appear in the body. When solvers rely on the integration of constraints into native ASP instead, it is more common to find theory atoms that are defined rather than external. A prototypical example of this is ezcsp [19], where all theory atoms are defined and may only occur in the head, deviating from the standard CASP definition. Another black box approach that extends ASP with external sources is _HEX programs_[23]. One of the main features of HEX programs is that, when consulting an external source, they allow higher-order parameters using the name of a logic program predicate as an argument for the external call. Another important feature is that HEX theory atoms allow for the invention of constants that are provided by the external source and were not originally present in the HEX program. This exceeds the ground-level definition used in the current paper. Yet, if we focus on ground HEX programs, we can observe that theory atoms only occur in rule bodies, and they do not require justification, so they would vaguely correspond to our external atom category. However, there are two important differences. First, it is unclear what the \"complement\" of a HEX theory atom would be or even if such a complement would make sense. Second, the truth of a HEX theory atom depends on the current interpretation handled by the logic program.