Conflict-Driven Constraint Answer Set Solving with Lazy Nogood Generation

Drescher and Walsh, to satisfiability modulo theories, the key idea is to incorporate 2010). Then, constraint answer sets of the resulting program theory-specific predicates into propositional formulas, can be characterized via Boolean assignments over and extending an ASP solver's decision engine for a atom(Π) body(Π) that do not violate a set of nogoods more high-level proof procedure. A promising approach to imposed by Π. Formally, a Boolean assignment A is a sequence constraint answer set programming (CASP) has been presented (σ