BINARY ENCODINGS FOR SOLVING AD-HOC CONSTRAINTS

Abstract

Historically, work on Constraint Satisfaction Problems (CSPs) began with binary CSPs and propagators proposed to enforce Arc Consistency (AC) on binary constraints. Additionally, several well-known binary encoding methods can be used to transform non-binary constraints into binary constraints. However, in more recent times (from the 1990s), research has focused on non-binary constraints and Generalized Arc Consistency (GAC) propagators. In this thesis, we propose new binary encodings with specialized AC propagators to efficiently solve non-binary ad-hoc constraints, such as the table, Ordered Multi-valued Decision Diagram and regular constraints. In addition, we also tailor the CNF encodings of binary constraints to transform binary encodings into Conjunctive Normal Form (CNF), making them suitable for SAT solvers. Our experiments show that binary encodings can significantly improve the GAC propagators and CNF encodings of the original non-binary ad-hoc constraints.