Binary Encodings for Solving Ad-hoc Constraints

Abstract:

Historically, work on Constraint Satisfaction Problems (CSPs) began with binary CSPs and algorithms proposed to enforce Arc Consistency (AC) on binary constraints. In addition, 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) algorithms. Existing results and “folklore” suggest that AC algorithms with binary encodings do not compete with GAC algorithms on the original non-binary constraints. In this thesis, we propose new binary encodings to solve non-binary ad-hoc constraints, such as the table and Ordered Multi-valued Decision Diagram (MDD) constraints.

We give a specialized algorithm called HTAC to enforce AC on constraints encoded by Hidden Variable Encoding (HVE). Preliminary experiments show that our AC algorithm on HVE encoded constraints is competitive to state-of-the-art GAC algorithms on the original non-binary constraints and faster in some instances. This result is surprising and is contrary to the "folklore" on AC versus GAC algorithms.

We use a new binary encoding called Bipartite Encoding (BE) to transform table constraints into binary constraints. AC on the BE encoded constraints can achieve a higher level of consistency than GAC on the original constraints. In addition, we give a specialized algorithm to enforce AC on the BE encoded constraints. Experiments show that BE with our AC algorithm can outperform the state-of-the-art table GAC algorithms.

We propose a binary encoding called Direct Tree Binary Encoding (DTBE) to transform decision diagram and automata constraints into Binary Constraint Trees (BCTs), where a BCT is a set of binary constraints with a tree structure. We show that BCTs can be super-polynomially smaller than the MDD, regular and non-deterministic finite state automaton constraints. Furthermore, we introduce reduction rules to simplify BCT constraints, and give a specialized algorithm to enforce AC on the BCT constraints. Our experiments show that simplified BCT constraints can be up to 2166 times smaller than the DTBE encoding, and the BCT AC algorithm can be significantly faster than MDD GAC algorithms.

In addition to AC algorithms, we also tailor the CNF encodings of binary constraints to transform BCT constraints into CNF forms, making them suitable for SAT solvers. We compare the propagation strength of the BCT CNF encodings and experimentally evaluate the encodings on a range of benchmarks. Experimental results show that the CNF encodings of BCT constraints can outperform those of MDD constraints on various benchmarks.