Constraint Answer Set Programming

Constraint answer set programming (CASP) is a novel, promising direction of research whose roots go back to propositional satisfiability (SAT). SAT solvers are efficient tools for solving boolean constraint satisfaction problems that arise in different areas of computer science, including software and hardware verification. Some constraints are more naturally expressed by non-boolean constructs. Satisfiability modulo theories (SMT) extends boolean satisfiability by the integration of non-boolean symbols defined by a background theory in another formalism, such as a constraint processing language. Answer set programming (ASP) extends computational methods of SAT in yet another way, inspired by ideas from knowledge representation, logic programming, and nonmonotonic reasoning. As a declarative programming paradigm, it provides a rich, simple modeling language that, among other features, incorporates recursive definitions. Answer set programming languages also use variables; software tools called grounders are used as front ends of answer set solvers to eliminate variables, whereas SAT-like procedures form their back-ends