ASPEN - Answer Set Programming with BoolEaN Satisfiability

One of the challenges of Artificial Intelligence is to find a general-purpose approach for modelling and solving practical combinatorial problems. This approach must take into account issues such as diverse domains, spatial and temporal reasoning, constraints, incomplete information and preferences.

In this context, several formal languages have been proposed, including Answer Set Programming (ASP). ASP is a form of
declarative programming particularly suited for knowledge representation, which is similar in syntax to traditional logic programming and close in semantics to non-monotonic logic. Some of the most important characteristics of ASP include: the use of default negation to allow for reasoning about incomplete knowledge; a very intuitive semantics based on multiple answer-sets for reasoning about several possible worlds; possibility to compactly represent all NP and coNP problems; fully declarative character in the sense that the program specification resembles the problem specification; and the existence of a number of well studied extensions such as preferences, revision, abduction, etc. Enormous progress concerning the theoretical foundations of ASP have been made in recent years, and the existence of reasonably efficient ASP solvers (e.g. DLV, SMODELS and CLASP) has made it possible to use it in real applications such as Decision Support for the Space Shuttle, Automated Product Configuration, Heterogeneous Data Integration; Phylogenetic Trees Inference, Resource Allocation, as well as Reasoning about actions, Legal Reasoning, Games, Planning, Scheduling, Diagnosis, etc.

Answer set solvers - solvers for generating stable models - normally start with grounding the program by instantiating its variables by ground literals, thus obtaining a propositional formula. At this stage, the use of Boolean satisfiability (SAT) solvers plays a key role. SAT solvers are well known for its efficiency, even though SAT is a NP-complete problem. Formulas with millions of variables and thousands of millions of clauses are amongst the formulas that state of the art SAT solvers can deal with. SAT solvers are still based on the old DPLL algorithm, although being further enhanced with sophisticated techniques. These techniques are deemed essential to the efficiency of SAT solvers and range from learning clauses to prevent future similar conflicts to dedicated data structures and dynamic heuristics.

For most of the contexts, SAT solvers are simply expected to either provide a solution, i.e. an assignment to the variables in the formula, or to prove that no such assignment exists. However, more sophisticated applications may require more than this, such as more than one solution or an explanation for having no solutions. Indeed, such extensions can be naturally incorporated into SAT solvers.

The ASPEN project is expected to be a breakthrough in Answer Set Programming by providing a flexible albeit competitive ASP solver, which will be able to take into account the user needs and preferences. These goals will be achieved extending the SAT solver which is the core of the ASP solver. Flexibility will be achieved through providing the user with detailed reasons for supporting either the solutions found or the nonexistence of solutions. The user will also be given the possibility to interact with the solver requiring other more suitable solutions.

This work will be supported by the knowledge and experience of the research team in the fields of ASP and SAT. In the ASP field, the research team from FCT has worked in the development of extensions of ASP to deal with knowledge revision and updates, in the area of declarative debugging, and applications of ASP in general. In the SAT field, the research team from INESC-ID has developed in the past the expertise in encoding problems into SAT and developing competitive SAT solvers providing failure explanations when no solution is found.

The ability to make ASP solvers more flexible will certainly be a burst for the use of ASP solvers in a larger number of domains. ASP users will be able to further understand the output provided by the solver, as well as to interact with the solver in order to get the most suitable explanations. This is expected to have a strong impact in effectively solving combinatorial problems coming from practical applications.

Funding entity: Fundação Ciência e Tecnologia (MCTES).

Reference: PTDC/EIA-CCO/110921/2009

Funding: 91567.