Constraint Answer Set Programming Without Grounding

tags

s(CASP)

Notes

ASP systems usually carry out an initial grounding phase where variables (and, therefore, the constraints linking them) disappear. Several approaches have been devised to work around this issue. However, since constraints need to be grounded as well, these approaches limit the range of admissible constraint domains

NOTER_PAGE: (1 . 0.755387303436226)

restore this integration by incorporating constraints into the s(ASP)

NOTER_PAGE: (2 . 0.20267909143855561)

s(CASP) inherits and generalizes the execution model of s(ASP) while remaining parametric w.r.t. the constraint solver.

NOTER_PAGE: (2 . 0.31217239370995925)

Due to the requirement to ground the program, causing a loss of communication from elimi- nation of variables, the execution methods for CASP systems are complex

NOTER_PAGE: (2 . 0.7705299941758882)

We have validated the s(CASP) approach with an implementation in Ciao Prolog

NOTER_PAGE: (2 . 0.8654630168899243)

s(CASP) system has been used to solve a series of problems that would cause infinite recursion in other top-down systems, but which in s(CASP) finitely finish, as well as others that require constraints over dense and/or unbound domains. Thus, s(CASP) is able to solve problems that cannot be straightforwardly solved in other systems.

NOTER_PAGE: (3 . 0.18695398951659872)

A difference between ASP and Prolog-style (i.e., SLD resolution-based) languages is the treat- ment of negated literals.

NOTER_PAGE: (3 . 0.6528829353523588)

SLDNF has to be restricted to ground calls, as a successful negated goal cannot return bindings. However, SLDNF increases the cases of non-termination w.r.t. SLD.

NOTER_PAGE: (3 . 0.714618520675597)

top-down evaluation makes the grounding phase unnecessary.

NOTER_PAGE: (3 . 0.7769365171811299)

most ASP systems are not able to compute its stable model (not even an empty one), be- cause the global constraint is unsafe. On the other hand, s(ASP) is able to compute queries to programs with unsafe rules by assuming that the unsafe variables take values in an ex- tended Herbrand Universe, and not just that of the terms which can be constructed from the symbols in the program.

NOTER_PAGE: (4 . 0.2603377984857309)

s(ASP) resolves negated atoms not li against dual rules of the program (Section 2.1), instead of using negation as failure.

NOTER_PAGE: (4 . 0.4239953407105417)

the dual program is not interpreted under SLD semantics

NOTER_PAGE: (4 . 0.47175305765870706)

The dual of a predicate p/1 is another predicate that returns the X such that p(X) is not true.

NOTER_PAGE: (4 . 0.5610486891385768)

Unlike Prolog’s negation as failure, disequality in s(ASP), denoted by “\=” , represents the constructive negation of the unification

NOTER_PAGE: (5 . 0.6948165404775772)

X \= a means that X can be any term not unifiable with a

NOTER_PAGE: (5 . 0.726266744321491)

a variable can only be disequality-constrained against ground terms

NOTER_PAGE: (5 . 0.7430711610486892)

express constraints more compactly and naturally

NOTER_PAGE: (12 . 0.7577169481654048)

s(CASP) can use structures / functors directly

NOTER_PAGE: (12 . 0.7891671520093186)

possible to use direct algorithms and to reduce the search space

NOTER_PAGE: (12 . 0.8316831683168318)