An Efficient and Uniform CSP Solution Generator Generator

• $\mathrm{■}$

  A general method to produce fast and self-improving uniform samplers of CSP solutions using a dedicated solving algorithm for random generation.

• $\mathrm{■}$

  A graph based split heuristic and propagation scheme, well fit to partition a problem into independent sub-problems.

• $\mathrm{■}$

  A heuristic Huffman-like representation for the solutions which minimizes the cost of uniform choices.

• $\mathrm{■}$

  A property based testing API, à la quickcheck, allowing for a transparent usage of our hybrid approach between rejection sampling and constraint based solving. The implementation is available at:
  https://osf.io/u4r5q/files/osfstorage?view_only=84af8ee65a6c495d98cb7b7bfad8c54b

This paper is organized as follows: Section 2 defines the concept of generators in general and gives some insight of what is expected from a good generator. Section 3 introduces the main mechanisms needed to build a constraint-based generators. Section 4 is the main contribution of this work: it addresses the problem of building a propagation-exploration scheme well-suited for the design of a constraint based generator. Section 6 presents our implementation and show its performances on some benchmark. Finally, Section 7 presents the related works and Section 8 summarizes our work and discusses its future continuations.

In the most general sense, rejection sampling is the approach that consists in generating samples in a super-set of the set of objects we are interested in, repeatedly until a sample lying in the set of interest is found. For instance, in order to generate a point inside the disk of radius $1$ in ${ℝ}^2$, one could generate points $(X,Y)$ in the square ${[-1,1]}^2$ until $X^2+Y^2\le 1$. In a constraint solving context, this means generating samples within the bounds of the problem until a sample that satisfy the constraints is found. Algorithm 1 illustrates this method.

This algorithm takes as input a set of variables $𝒱$, their associated range of values $𝒟$, and a set of constraints $𝒞$. The spawn function generates a candidate at random (for some probability distribution $\mathbb{P}$) from the given variables and their domains. Then, the sat function evaluates whether the generated candidate satisfies all the constraints in $𝒞$. The procedure is called recursively until a solution is found.

Note that the number of iteration of this algorithm is a random variable. The probability of accepting a sample $X$ at line 3 is the probability $P(X\in A)$ that $X$ lies inside the solution space $A$. Provided that this probability is non-zero, this algorithms terminates, and its number of iterations follows a geometric law of parameter $\mathbb{P}(A)$. It thus makes $\frac{1}{\mathbb{P}(X\in A)}$ iterations in expectation.

Finally, a key observation is that Algorithm 1 implements the probability distribution $\mathbb{P}$ conditioned to only draw elements of the solution space $A$. In particular, if the spawn function draws uniform samples in the domain $𝒟$, then Algorithm 1 is a uniform sampler of solution. The contribution of the present paper is to devise a good spawn function that can guarantee that this algorithm is uniform while providing good performance.

In [29], authors build upon this constraint-solving method an algorithm for uniform sampling under constraints, as shown in Algorithm 3. It repeatedly selects an element $e$ from either the inner or outer sets using a select function. Here, select performs a weighted choice based on the volume of the elements, with the largest elements having the best chance of being chosen. We discuss in the next section the design of a data structure that enables an efficient implementation of this function. The algorithm generates a candidate value $i$ within $e$. If $e$ belongs to the inner set or $i$ satisfies the constraints $𝒞$, the algorithm returns $i$; it repeats these steps otherwise.

This algorithm ensures uniform sampling under three conditions: the elements in $I\cup O$ must not overlap, points within each element $e$ must be sampled uniformly $P(i\mid e)=\frac{1}{v(e)}$, and the probability of selecting an element $e$ must be proportional to its volume ($P(e)=\frac{v(e)}{{\sum }_{e^{\prime }\in I\cup O}v(e^{\prime })}$). These conditions ensure that the sampling process remains uniform across the domain, giving all points in the union of elements an equal likelihood of being chosen.

In order to implement the select function, we need a data structure for storing a collection of abstract elements that supports:

• $\mathrm{■}$

  efficient sampling of an elements with probability proportional to its volume;

• $\mathrm{■}$

  and (we will see later), an efficient way to replace an abstract element with a collection of smaller elements.

In [29], sorted list in decreasing order of volume are used for element selection, so that the elements with highest probability are met faster during sampling. However, if elements are of the same size, this approach offers no advantage, as all selections become equally likely. Also, they do not require to update their structure in their work. We can do better by arranging these elements in a binary tree. The idea is to store the abstract elements at the leaves of the tree and to maintain, in every node, the sum of the volumes of all the leaves below that node. Using such a data structure, drawing a abstract element proportional to its volume corresponds to drawing a uniform real variable between $0$ and the total volume of the tree, and to recursively descend in the tree, choosing between the left and right child based on their weights. This is illustrated in Algorithm 4.

Here, the cost of selecting an element is proportional to the length of the path from the root to the selected leaf. Given the volume of every abstract element (and thus their probability of being drawn), there is an optimal way to arrange these elements in the tree in order to minimise the expected cost of the generation. Information theoretic results tell us that the expected path length between the root and the sample is lower bounded by the entropy of the probability distribution, that is

where the sum ranges over the abstract elements stored in the tree, and $p_x$ is the sampling probability of element $x$. The optimal way to organise the tree in order to remain close to this lower bound is to use a Huffman tree [16]:

• $\mathrm{■}$

  start from a collection of leaves,

• $\mathrm{■}$

  iteratively pair the two smallest elements of the collection as a binary node,

• $\mathrm{■}$

  this process terminates when every leaves belong to the same tree.

A tree built this way has the property that its expected path length to a leaf is at most $\mathscr{H}+1$.

Unfortunately, the good properties of Huffman trees are hard to maintain efficiently when we update the collection of abstract elements, which we need for in the adaptive algorithm presented in Section 3.3. To circumvent this issue, we use the following heuristic:

1. 1.

   before doing any sampling, we do a first solving pass until a certain depth;

2. 2.

   after this pre-processing, we construct a Huffman tree $T$ based on the volumes of the resulting elements;

3. 3.

   then, during the iterative sampling process, every time we need to split an abstract element $e$ into a collection of smaller elements $(e_1,e_2,\mathrm{\dots },e_p)$, we construct a Huffman tree $T^{\prime }$ for $(e_1,e_2,\mathrm{\dots },e_p)$ and we replace the leaf $e$ in $T$ with $T^{\prime }$.

It is worth noting that the replacement of the last sampled leaf can be optimised by keeping a pointer to this last leaf, rather than traversing the tree a second time to find it.

The initial Huffman tree $T$ constructed at step 2 thus potentially evolves away from its optimal shape as we update leaves. However, since the elements that have the highest probability to be selected (and thus split) are the bigger ones, we expected our heuristic to maintain some balance in the tree. Our benchmarks, presented in Section 6, seem to show that this data structure performs well in practice. An interesting algorithmic problem would be to investigate the real performance of this idea, and potentially find a better data structure, which is a work in progress.

From a practical point of view, we cannot really replace an inefficient sampler with a generator based on an extremely expensive constraint solving mechanism. This would simply replace a slow generation speed, by a faster one preceded by a huge overhead due to solving time. This is especially prejudicial when the generator is only used a handful of time.

Iterative solvers are commonly used when dealing with complex constraint satisfaction problems where finding an exact solution is computationally infeasible or impractical. Instead of attempting to solve the entire problem in one step, iterative solvers work incrementally, refining the solution repeatedly until a certain termination criterion is met.

We therefore propose to use constraint resolution mechanisms parsimoniously: first, we will target in priority on certain parts of the problem, identified on the fly, whose filtering can greatly improve the performance of random generation. Second, we try to amortize the cost of the resolution steps (filtering and exploration) during the generation. For example, every $n$ time a generator is called, we can perform a resolution step. Thus, the more a generator is used, the more it improves. To achieve this, the generator embeds an internal solving state that evolves with each step. This state retains information from previous resolution steps, allowing the generator to improve progressively rather than starting from scratch each time.

Algorithm 2 revolves around two primary decisions: selecting which element to refine and determining how to refine it. On the one hand, intuitively, the focus should be on larger elements with higher rejection rates, as they are more critical to the rejection rate and, thus, the efficiency of the whole process. On the other hand, sampling also requires choosing an element, with larger elements being more likely to be selected. This leads to the question of whether sampling’s focus on larger elements can be used to help guide the solving process.

For each element in our cover, we track the number of times it was selected and record the number of times it successfully produced a sample. We also track the total number of successes and failures for the whole cover. When our algorithm fails to produce a valid solution within a selected element, we must then decide whether it is necessary to split it or not. To do this, we base our choice on its acceptance rate. If it falls below the global acceptance rate, we proceed to refine that element, meaning we split it and replace it within the cover with the resulting sub-elements. Otherwise, it is left unchanged. This dynamic adjusting of the refinement process can lead to a faster convergence and avoids over-splitting, which can deteriorate the element selection procedure. This is illustrated by Algorithm 5.

The iterative process of splitting and filtering gradually ensures that certain constraints are locally satisfied, allowing them to be removed from the graph. Whenever a constraint is removed, the solver checks whether its removal disconnects the graph. When this is the case, the graph is split into connected components, enabling their independent handling.

Constraints become redundant when their validity is guaranteed by current domain assignments. Our implementation recomputes connected components whenever a constraint is removed by the solver so as to be able to exploit the independence of the components.

To achieve this, we develop a propagation scheme and an exploration heuristic that help reduce the connectivity of the constraint graph. For each edge, we maintain information on whether it is a bridge or not. A bridge is an edge whose removal increases the number of connected components in the graph. We identify bridges using Tarjan’s algorithm [25]. Tracking which edges are bridges is useful for guiding exploration, since variables that are part of a bridge are particularly interesting for splitting. When a constraint is removed, if it was a bridge, the connected components (CCs) are recomputed. Otherwise, the removal is checked to determine whether it introduced new bridges, without recalculating the connected components. If a bridge is detected, we attempt to eliminate it, as its removal would disconnect the graph and thus improve the sampler’s performance. This is done by prioritizing the variables in the bridge’s support during splitting steps.

GeGen’s generators differ fundamentally from traditional QuickCheck-style generators as they produce symbolic variables rather than concrete values. Traditional property-based testing frameworks generate fixed values like random integers or floats. In contrast, GeGen’s generators operate at a symbolic level which makes possible constraint composition and solving. For instance, instead of directly generating a number, GeGen creates a symbolic variable that represents the number and associates it with a range of possible values. This symbolic variable acts as a declaration on the solver’s side. Additionally, instead of applying a predicate to verify wether a value satisfies or not the property being tested, GeGen’s predicates impose constraints on this variable such as “the number must be even” or “the number must be less than another variable” that are collected to construct a CSP. Finally, we apply the previously discussed solving and sampling techniques to the constructed CSP. For example, to generate circles within a given square in QCheck, we can use the following code:

The find_example function generates random integer values for $x$, $y$, and $r$, then applies the given predicate to check whether the generated circle satisfies the constraints. This process repeats until a valid example is found or the search limit is exhausted. Note that here, int is an atomic generator that produces random integers and pair is a combinator that constructs a generator of pairs from two base generators.

The interest of our approach is that the same code, when linked against our library, will yield identical results but in a significantly more efficient manner, and using a fundamentally different mechanism. Instead of directly sampling random values for $x$, $y$, and $r$, we constructs a symbolic representation of the problem. From the solver’s perspective, a constraint satisfaction problem (CSP) with three floating-point variables $v_1,v_2$ and $v_3$ is formulated. However, this approach abstracts certain details about the algebraic structure of the type. Therefore, a reconstruction function is designed alongside the CSP, so that once a sample $s$ is drawn, it can be re-assembled to a value of the correct type. In this particular case, the function is $f(s)=((s(v_1),s(v_2)),s(v_3))$. It ensures that once the solver produces a valid assignment for the symbolic variables, the corresponding concrete values are reconstructed in a way that respects the intended algebraic structure. Finally the predicate, instead of returning a truth value will actually build the equivalent constraint system. In essence, this allows us to decouple the problem-solving phase from the data generation phase (at the API level) while ensuring that the generated values maintain the correct type.

The constraint language used in GeGen supports arithmetic and boolean expressions. It includes: arithmetic operation (addition, multiplication, etc.), Boolean logic (comparisons, conjunctions, disjunctions, negations), and variables. We build upon those generators for more complex types such as tuples and lists by composing the different elements of a generator.

GeGen extends standard arithmetic and Boolean operators by overriding them to facilitate the construction of constraints, making it possible to define a CSP in a manner that closely resembles programming its logical predicate counterpart. This intuitive approach aligns the construction of constraints with familiar programming paradigms, simplifying the transition from predicates to constraints.

For instance, consider a predicate that verifies whether a list is sorted. This predicate can naturally be expressed in a functional style as follows:

This predicate can be applied to concrete lists of integers to determine whether they are sorted. This is what is done when doing rejection sampling. Using GeGen, the predicate takes another meaning as it operates on lists of variables to dynamically construct a CSP. The overloaded operators automatically translate the predicate logic into corresponding constraints. For example:

Here, the open GeGen directive brings in scope the operators <= and && (among others), so that instead of computing a boolean value, the is_sorted function now builds a constraint. Beside that the only difference is the use of the symbolic constraint true_ instead of the builtin OCaml boolean true, which can’t be avoided as OCaml does not permit the overriding of litterals. This approach preserves the logical structure and readability of the predicate while generating a constraint representation that can be used to solve CSPs.

We have written generators using our framework for several realistic examples: the convex problem defines the predicate for star-convex polygons, i.e. the vectors corresponding to two consecutive edges of the polygons have a negative cross-product. The diagdom, idempotent, symmetric and orthogonal problems, define the predicates for some well known classes of matrices. The distrib, itvcover and sorted represent respectively the predicate for valid distribution of probability i.e., list of positive values that sum to one, interval-covering list that is a list that contains a set of intervals that cover a specific range without gaps and finally the set of sorted lists in increasing order. We compare our approach against QCheck’s standard rejection sampler, as it serves as a baseline for property-based testing. This comparison is relevant since we have designed an API that allows users to write the same specifications while seamlessly generating samples using our method instead.

Table 1 presents the number of samples generated by GeGen and QCheck for various problem instances. Each row corresponds to a specific problem. The first column lists the problem names. The second column indicates the problem size parameters, denoted as $|𝒱|,|𝒞|$. The remaining columns report the number of generated samples for different time constraints (0.1, 1, and 2 seconds of generation time), with results shown separately for GeGen and QCheck. Best result for each are shown in bold font. The problem sizes were selected to ensure that trends in sample generation could be clearly observed while maintaining a fair evaluation of both methods. The measurements were conducted on a machine with a 12th Gen Intel(R) Core(TM) i5-1235U processor and 15 GiB of RAM.

The results indicate that GeGen consistently outperforms QCheck, generating significantly more samples across nearly all problem types and sizes. While QCheck performs adequately for smaller problem instances, its performance drops as problem complexity increases, often failing to generate any samples for larger cases. In contrast, GeGen scales effectively, maintaining high sample generation rates even for more complex problems. Also, the performance of the rejection sampler remains stable over time while the ones of the generator built using GeGen improves as the process progresses. This trend is illustrated in Figure 3, which depicts the time in seconds (y-axis) required to generate the $i$-th sample (x-axis), for 10000 samples. GeGen’s times (solid line), and QCheck’s (dashed line) are shown on a single problem, sorted lists of size $n$, to highlight this feature of our generators, although the same behaviour can be noticed on problems of table 1. Notable spikes in the curves correspond to garbage collection cycles, which are particularly apparent for small values of $n$.

Figure 3(a) demonstrates that for small list sizes, QCheck and GeGen exhibit similar performance. In fact, QCheck marginally outperforms GeGen, as the rate of sorted lists among lists of size 3 is relatively high. However, as $n$ increases, the rejection rate also rises, causing GeGen to surpass QCheck. By the time n=9n=9, GeGen is already outperforming QCheck by three orders of magnitude, as shown in Figure 3(c). Note that, due to the scale, the GeGen line appears very close to the x-axis. For larger values of $n$, rejection sampling via QCheck becomes impractical, and thus only the results for GeGen are presented. This figure shows that the incremental nature of our generators allows them to scale effectively, handling larger $n$ more efficiently.