On the Decidability of Connectedness Constraints in 2D and 3D Euclidean Spaces

AAAI Conferences

We investigate (quantifier-free) spatial constraint languages with equality, contact and connectedness predicates as well as Boolean operations on regions, interpreted over low-dimensional Euclidean spaces. We show that the complexity of reasoning varies dramatically depending on the dimension of the space and on the type of regions considered. For example, the logic with the interior-connectedness predicate (and without contact) is undecidable over polygons or regular closed sets in the Euclidean plane, NP-complete over regular closed sets in three-dimensional Euclidean space, and ExpTime-complete over polyhedra in three-dimensional Euclidean space.

Redundancy in Random SAT Formulas

AAAI Conferences

The random k-SAT model is extensively used to compare satisfiability algorithms or to find the best settings for the parameters of some algorithm. Conclusions are derived from the performances measured on a large number of random instances. The size of these instances is, in general, small to get these experiments done in reasonable time. This assumes that the small size formulas have the same properties as the larger ones. We show that small size formulas have at least a characteristic that makes them relatively easier than the larger ones (beyond the increase in the size of the formulas).

Constraint Satisfaction Techniques for Combinatorial Problems

AAAI Conferences

The last two decades have seen extraordinary advances in industrial applications of constraint satisfaction techniques, while combinatorial problems have been pushed to the sidelines. We propose a comprehensive analysis of the state of the art in constraint satisfaction problems when applied to combinatorial problems in areas such as graph theory, set theory, algebra, among others. We believe such a study will provide us with a deeper understanding about the limitations we still face in constraint satisfaction problems.

On the CNF encoding of cardinality constraints and beyond

arXiv.org Artificial Intelligence

In this report, we propose a quick survey of the currently known techniques for encoding a Boolean cardinality constraint into a CNF formula, and we discuss about the relevance of these encodings. We also propose models to facilitate analysis and design of CNF encodings for Boolean constraints.

Tractable Set Constraints

Journal of Artificial Intelligence Research

Many fundamental problems in artificial intelligence, knowledge representation, and verification involve reasoning about sets and relations between sets and can be modeled as set constraint satisfaction problems (set CSPs). Such problems are frequently intractable, but there are several important set CSPs that are known to be polynomial-time tractable. We introduce a large class of set CSPs that can be solved in quadratic time. Our class, which we call EI, contains all previously known tractable set CSPs, but also some new ones that are of crucial importance for example in description logics. The class of EI set constraints has an elegant universal-algebraic characterization, which we use to show that every set constraint language that properly contains all EI set constraints already has a finite sublanguage with an NP-hard constraint satisfaction problem.