Solving a Constraint Satisfaction Problem (CSP) usually requires a model typically using existing basic constraints. The most flexible form of constraint, ad-hoc (generic) constraints defined with certain constraint representations, such as binary constraint tree (BCT) and decision diagrams, have been proposed where basic constraints in intensional form are insufficient. A modeller may wish to combine basic constraints using logic operators (and, or, negation). However, negation, a key logical operator for expressivity is not tractable in many existing constraint representations. This creates a dilemma, for modelling, we would desire more flexibility, but a model whose operations are intractable may in turn be impractical. In this paper, we give a framework which allows for a tractable negation operator on constraint representations. We apply the framework on the BCT and ordered decision diagram constraints, giving new subforms. These subforms can be strictly more succinct than ordered multi-valued decision diagrams (OMDD), while being as tractable as OMDD for logical combinations. We give applications to show effective propagators from logical combinations and in building large constraint models for configuration problems.

Recently, the Binary Constraint Tree (BCT), a tree structured Binary Constraint Network (BCN), has been shown to be more succinct than various ad-hoc constraints. In this paper, we investigate the modelling power of a well-known tractable hybrid class generalizing BCT, i.e. the class of BCNs satisfying Broken Triangle Property (BTP) called BTP Networks (BTPNs). We show that the consistency checker of BTPN can be computed by polysize monotone circuit, thus, some global constraints cannot be encoded as polysize BTPN, such as the AllDifferent and Linear constraints. Then our study reveals that BTPN is strictly more succinct than the DNNF constraint and all 14 ad-hoc constraints discussed in (Wang and Yap 2023), such as the context-free grammar, BCT and smart table constraints. Furthermore, we also show that BTPN is as powerful as DNNF in terms of computing various operations and queries. In addition, we prove that it is NP-hard to determine the minimum sized BTPN encoding a constraint.

Ad-hoc constraints (also called generic constraints) are important for modelling Constraint Satisfaction Problems (CSPs). Many representations have been proposed to define ad-hoc constraints, such as tables, decision diagrams, binary constraint trees, automata and context-free grammars. However, prior works mainly focus on efficient Generalized Arc Consistency (GAC) propagators of ad-hoc constraints using the representations. In this paper, we ask a more fundamental question which bears on modelling constraints in a CSP as ad-hoc constraints, how the choice of constraints and operations affect tractability. Rather than ad-hoc constraints and their GAC propagators, our focus is on their expressive power in terms of succinctness (polysize) and cost of operations/queries (polytime). We use a large set of constraint families to investigate the expressive power of 14 existing ad-hoc constraints. We show a complete map of the succinctness of the ad-hoc constraints. We also present results on the tractability of applying various operations and queries on the ad-hoc constraints. Finally, we give case studies illustrating how our results can be useful for questions in the modelling of CSPs.

A wide range of verification methods have been proposed to verify the safety properties of deep neural networks ensuring that the networks function correctly in critical applications. However, many well-known verification tools still struggle with complicated network architectures and large network sizes. In this work, we propose a network reduction technique as a pre-processing method prior to verification. The proposed method reduces neural networks via eliminating stable ReLU neurons, and transforming them into a sequential neural network consisting of ReLU and Affine layers which can be handled by most verification tools. We instantiate the reduction technique on the state-of-the-art complete and incomplete verification tools, including$\alpha,\beta$-crown, VeriNet and PRIMA. Our experiments on a large set of benchmarks indicate that the proposed technique can significantly reduce neural networks and speed up existing verification tools. Furthermore, the experiment results also show that network reduction can improve the availability of existing verification tools on many networks by reducing them into sequential neural networks.

Many practical applications require synthesizing directed graphs that satisfy the acyclic constraint along with some side constraints. Several methods have been devised for encoding acyclicity of directed graphs into SAT, each of which is based on a cycle-detecting algorithm. The leaf-elimination encoding (LEE) repeatedly eliminates leaves from the graph, and judges the graph to be acyclic if the graph becomes empty at a certain time. The vertex-elimination encoding (VEE) exploits the property that the cyclicity of the resulting graph produced by the vertex-elimination operation entails the cyclicity of the original graph. While VEE is significantly smaller than the transitive-closure encoding for sparse graphs, it generates prohibitively large encodings for large dense graphs. This paper reports on a comparison study of four SAT encodings for acyclicity of directed graphs, namely, LEE using unary encoding for time variables (LEE-u), LEE using binary encoding for time variables (LEE-b), VEE, and a hybrid encoding which combines LEE-b and VEE. The results show that the hybrid encoding significantly outperforms the others.

Ordered Multi-valued Decision Diagram (MDD) is a compact representation used to model various constraints, such as regular constraints and table constraints. It can be particularly useful for representing ad-hoc problem specific constraints. Many algorithms have been proposed to enforce Generalized Arc Consistency (GAC) on MDD constraints. In this paper, we introduce a new compact representation called Binary Constraint Tree (BCT). We propose tree binary encodings to transform any MDD constraint into a BCT constraint. We also present a specialized algorithm enforcing GAC on the BCT constraint resulting from a MDD constraint. Experimental results on a large set of benchmarks show that the BCT GAC algorithm can significantly outperform state-of-the-art MDD as well as table GAC algorithms.

Ordered Multi-valued Decision Diagrams (MDDs) have been shown to be useful to represent finite domain functions/relations. For example, various constraints can be modelled with MDD constraints. Recently, a new representation called Binary Constraint Tree (BCT), which is a (special) tree structure binary Constraint Satisfaction Problem, has been proposed to encode MDDs and shown to outperform existing MDD constraint propagators in Constraint Programming solvers. BCT is a compact representation, and it can be exponentially smaller than MDD for representing some constraints. Here, we also show that BCT is compact for representing non-deterministic finite state automaton (NFA) constraints. In this paper, we investigate how to encode BCT into CNF form, making it suitable for SAT solvers. We present and investigate five BCT CNF encodings. We compare the propagation strength of the BCT CNF encodings and experimentally evaluate the encodings on a range of existing benchmarks. We also compare with seven existing CNF encodings of MDD constraints. Experimental results show that the CNF encodings of BCT constraints can outperform those of MDD constraints on various benchmarks.

Constraint Programming is a powerful paradigm to model and solve combinatorial problems. While there are many kinds of constraints, the table constraint (also called a CSP) is perhaps the most significant—being the most well-studied and has the ability to encode any other constraints defined on finite variables. Thus, designing efficient filtering algorithms on table constraints has attracted significant research efforts. In turn, there have been great improvements in efficiency over time with the evolution and development of AC and GAC algorithms. In this paper, we survey the existing filtering algorithms for table constraint focusing on historically important ideas and recent successful techniques shown to be effective.

Constraint Satisfaction Problems (CSPs) are typically solved with Generalized Arc Consistency (GAC). A general CSP can also be encoded into a binary CSP and solved with Arc Consistency (AC). The well-known Hidden Variable Encoding (HVE) is still a state-of-the-art binary encoding for solving CSPs. We propose a new binary encoding, called Bipartite Encoding (BE) which uses the idea of partitioning constraints. A BE encoded CSP can achieve a higher level of consistency than GAC on the original CSP. We give an algorithm for creating compact bipartite encoding for non-binary CSPs. We present a AC propagator on the binary constraints from BE exploiting their special structure. Experiments on a large set of non-binary CSP benchmarks with table constraints using the Wdeg, Activity and Impact heuristics show that BE with our AC propagator can outperform existing state-of-the-art GAC algorithms (CT, STRbit) and binary encodings (HVE with HTAC).

Effective general-purpose search strategies are an important component in Constraint Programming. We introduce a new idea, namely, using correlations between variables to guide search. Variable correlations are measured and maintained by using domain changes during constraint propagation. We propose two variable heuristics based on the correlation matrix, crbs-sum and crbs-max. We evaluate our correlation heuristics with well known heuristics, namely, dom/wdeg, impact-based search and activity-based search. Experiments on a large set of benchmarks show that our correlation heuristics are competitive with the other heuristics, and can be the fastest on many series.