of the sat **problem and passed to a** sat **solver. If the formula is satisfiable, its model is** transformed back to variables describing the problem, giving a solution to the problem.

3.1. Problem Specification. Let us consider problems of the following general form: **find**
(if it exists) a set of values S such that given constraints are met **(variations of this form** include: only checking if such values exists, and finding all **values that meet the given** conditions). A problem of this form can be specified by a test that checks if a given set S meets the given constraints (with one assertion that combines all the constraints). The test can be formulated in a language designed in the style of imperative programming languages and such a test is often easy to formulate.

Example 3.1. Let us consider a trivial problem: if v equals u + 1, find a value for u **such**
that v equals 2. A simple check in an imperative form can be specified **for this problem** - if a value of u **is given in advance, one could easily check whether it is a solution of the**
problem. Indeed, one would assign u+1 to v and finally check whether v **equals 2. Such test** can be written in the form of an imperative C-like code (where assert(b) **checks whether**
b **is true) as follows:**
v = u+1; assert(v==2);
The example above is trivial, but specifications may involve **more variables and more**
complex operations, including conditional operations and **loops, as illustrated by the following example.**
Example 3.2. **The most popular way of generating pseudorandom numbers is based on**
linear congruential generators. A generator is defined by a recurrence relation of the form:
xn+1 ≡ (axn + c) (mod m**) (for** n ≥ 0)
and x0 is the seed value (0 ≤ x0 < m**). One example of such relation is:**
xn+1 ≡ (1664525xn + 1013904223) (mod 232**) (for** n ≥ 0)
It is trivial to compute elements of this sequence. The check **that** x100 **is indeed equal to the**
given value if the seed is equal to nseed **can be simply written in the form of an imperative**
C-like code as follows (assuming that numbers are represented by 32 bits):
nx=nseed; for(ni=1;ni<=100;ni++)
nx=nx*1664525+1013904223; assert(nx==3998113695);
However, the following problem, realistic in simulation and testing tasks, is a non-trivial programming problem (unless problem-specific, algebraic knowledge is used): given, for example, the value x100 compute x0**. Still, the very same test shown above can serve** as a specification of this problem. This example illustrates **one large family of problems**
that can be simply specified using the proposed approach - problems that are naturally expressed in terms of imperative computations and that involve destructive assignments.

Such problems are often difficult to express using other languages and systems. For the above specification, since in constraint programming systems the destructive assignment is not allowed, in most specification languages one would have to introduce variables for all elements of the sequence from x0 to x100 **and the constraints between any succeeding two.** Also, other systems typically do not support modular arithmetic constraints and integers of arbitrary length.