Handling Arithmetic Binary and Non-Binary Constraints in Quantified Constraint Satisfaction Problems

Abstract

Researchers have developed many strategies for solving combinatorial problems based on Constraint Satisfaction Problems (CSPs) ([5], [10], [12]). This approach has proved to be very effective in many real-world problems. Recently, the scientific community has started to take on a harder task, the one of solving a generalization of the standard CSP, the quantified Constraint Satisfaction Problem (QCSP) ([18], [19]). One way to solve QCSPs is to use the knowledge acquired by CSP algorithms and methods, and based on them to try and derive QCSP algorithms [17]. Up to now the experimental work in QCSPs has dealt only with binary random problems. Instead, we will concentrate on generating and solving problems with arithmetic binary and non-binary constraints. Our main goal is to study not only the implementation but also the “meaning” of basic algorithms such as Arc Consistency (AC), Backtracking (BT), Forward Checking (FC) and Maintaining Arc Consistency (MAC). In order to reform the aforementioned algorithms so that they can deal with arithmetic constraints, one needs to understand the way they work, the way they search the space of variables and constraints and the nature of this type of search. We will also be dealing with non-binary constraints and presenting an implementation of a prototype library of functions and algorithms for QCSP problems implemented in the Java programming language. Finally, we will give examples of all of the aforementioned so that the reader can comprehend some of the complex definitions and algorithms studied. The examples are taken from various areas of expertise and the main goal of their usage is to help us form a small survey of work closely related to the QCSPs.