GOS A new declarative tool for modelling and solving CSPs to SAT

Abstract

When somebody wants to solve a problem, surely, the most common approach in the programming world is to use an imperative programming language and define an algorithm with the steps to solve it. But there are many alternatives to that. Constraint Satisfaction Problems (CSP)s are a type of problems in which variables are defined and, by applying constraints, you try to limit the domain of this variables until you reach a solution, but without proposing any specific algorithm to solve it. This kind of problems are easily modelled with declarative programming languages. Declarative programming languages attempt to describe what the program must accomplish in terms of the problem domain, rather than describe how to accomplish it as a sequence of the programming language primitives. This is in contrast with imperative programming, which implements algorithms in explicit steps. A subset of declarative languages are modelling languages. This project will be focused on this subset and the main purpose will be create a new declarative programming language for modelling any CSP to Boolean Satisfiability (SAT). One of the most successful methodologies for solving CSP relies on the conversion into SAT problems. The advantage is the wide availability of free and efficient SAT-solvers. A SAT problem contains a formula built on a set of boolean variables, which can take only value true (or 1) and false (or 0). A solution to SAT problem is an assignment of values true/false to the logical variables, such that all clauses are satisfied