We define a new formalism, called$\beth$CHR, which generalises the CHR formalism by introducing some meta-constraints, called behaviors, allowing us to easily specify problems modelling an adversary. We define a new language with a syntax and a proof-theoretical semantics as an extension of the syntax and semantics of the CHR language.

In this article, the QCSP (Quantified Constraint Satisfaction Problems) framework is shifted to the QCHR (Quantified Constraint Handling Rules) framework by enabling dynamic generation of quantifiers and access to user-defined constraints. QCSP offers a natural framework to express PSPACE problems as finite two-players games. But to define a QCSP model, the alternation of quantifiers must be formerly known and cannot be built dynamically even if the worst case will not occur. To overcome this issue, the new QCHR formalism, that allows to generate quantifiers dynamically during the solving, is defined. QCHR models exhibit state-of-the-art performances on a priori fixed alternation of quantifiers and outperforms previous QCSP approaches when the generation of quantifiers is dynamic.

Encoding an instance of a Constraint Satisfaction Problem (CSP) into a Propositional Satisfiability Problem (SAT) instance is usually a good way to benefit from the highly efficient SAT solvers. However, an encoding may not be suitable for all the constraints in the model because it produces a large instance, the modeling of a constraint is complicated or, it does not propagate adequately. In general, a good encoding should aim to improve resolution effectiveness (independently of the solver chosen) and produce an instance of reasonable size. Standard CSP-to-SAT encodings usually focus on some aspects like straightforwardness, compactness, or good performance for specific constraints. Hybrid encodings combine encodings to obtain the best from each one of them. This article presents the Abacus Encoding, a new hybrid encoding that combines Log and Order encodings and provides a good trade-off between the instance size and the resolution effectiveness. Like the Chinese abacus, this encoding represents integer values as the addition of units and tens. Units are set with Log encoding and tens with Order encoding. This approach allows a compact representation of values, and it is easily adaptable to improve solving efficiency. This article presents the Abacus Encoding, a new hybrid encoding that combines Log and Order encodings and provides a good trade-off between the instance size and the resolution effectiveness. Like the Chinese abacus, this encoding represents integer values as the addition of units and tens. Units are set with Log encoding and tens with Order encoding. This approach allows a compact representation of values, and it is easily adaptable to improve solving efficiency.

Quantified Constraint Satisfaction Problems (QCSP) are a generalization of Constraint Satisfaction Problems (CSP) in which variables may be quantified existentially and universally. QCSP offers a natural framework to express PSPACE problems as finite two-player games or planning under uncertainty. State-of-the-art QCSP solvers have an important drawback: they explore much larger combinatorial spaces than the natural search space of the original problem since they are unable to recognize that some sub-problems are necessarily true. We introduce a new tool, inspired by the cut rule of Prolog as a tool under responsibility of the designer of the QCSP, to prune those parts of the search space which are by construction known to be useless. We use this new tool to restore on one hand the annihilator property of true for disjunction in QCSP solver and, on the other hand, to prune the search space in two-player games. It is a simple solution to use efficiently QCSP to design finite two-player games without restricting the QCSP language. This tool does not need to modify the QCSP solver but has only one requirement: be able to tell the QCSP solver that the current QCSP is solved. Our QCSP solver built over Ge Code, a CSP library, obtained very good results compared to state-of-the-art QCSP solvers.

We propose to use constraint programming (CP) to assist the user in 3D layout of restricted virtual environments (VEs). With this aim in mind, we integrated a constraint solver, into a professional authoring tool allowing the development of 3D real-time applications. The solver is used to formalize and develop different types of layout constraints and to find a solution to a user-specified layout problem. A communication module was developed to transmit the solution to the VE which automatically re-arranges itself. Modeling the problem and finding solutions are completely transparent for the user since he/she interacts with the VE regardless of the resolution mechanisms. In addition to the automatic objects placement, the proposed system can be used to assist the user during a manual layout by providing visual informations about the areas in which a given object cannot be placed. An experimental study has been carried out to investigate the effect of the provided look ahead-based assistance on user performance in 3D layout tasks.