Bound Founded Answer Set Programming
  Answer Set Programming (ASP) is a powerful modelling formalism that is very
efficient in solving combinatorial problems. ASP solvers implement the stable
model semantics that eliminates circular derivations between Boolean variables
from the solutions of a logic program. Due to this, ASP solvers are better
suited than propositional satisfiability (SAT) and Constraint Programming (CP)
solvers to solve a certain class of problems whose specification includes
inductive definitions such as reachability in a graph. On the other hand, ASP
solvers suffer from the grounding bottleneck that occurs due to their inability
to model finite domain variables. Furthermore, the existing stable model
semantics are not sufficient to disallow circular reasoning on the bounds of
numeric variables. An example where this is required is in modelling shortest
paths between nodes in a graph. Just as reachability can be encoded as an
inductive definition with one or more base cases and recursive rules, shortest
paths between nodes can also be modelled with similar base cases and recursive
rules for their upper bounds. This deficiency of stable model semantics
introduces another type of grounding bottleneck in ASP systems that cannot be
removed by naively merging ASP with CP solvers, but requires a theoretical
extension of the semantics from Booleans and normal rules to bounds over
numeric variables and more general rules. In this work, we propose Bound
Founded Answer Set Programming (BFASP) that resolves this issue and
consequently, removes all types of grounding bottleneck inherent in ASP
systems.
