A framework for representing and solving NP search problems

TLDR

NP search and decision problems are ubiquitous in AI, and general‑purpose methods such as SAT, CSP, and ASP have been developed to address them. The authors propose a declarative constraint programming framework that combines the strengths of SAT, CSP, and ASP while mitigating their weaknesses. They formalize the framework as a model extension problem that extends a structure by new relations, and present a parameterized version that captures NP. They discuss properties of the framework that support effective modelling and outline prospects for effective solver design.

Abstract

NP search and decision problems occur widely in AI, and a number of general-purpose methods for solving them have been developed. The dominant approaches include propositional satisfiability (SAT), constraint satisfaction problems (CSP), and answer set programming (ASP). Here, we propose a declarative constraint programming framework which we believe combines many strengths of these approaches, while addressing weaknesses in each of them. We formalize our approach as a model extension problem, which is based on the classical notion of extension of a structure by new relations. A parameterized version of this problem captures NP. We discuss properties of the formal framework intended to support effective modelling, and prospects for effective solver design.