variable - from the minimal (maximal) element in the range onwards, seeking for a minimal (maximal) value that meets the constraint.

6.4. **Turning** sat Models into Values of the Independent Variables. **If the** sat solver finds a satisfying valuation for the input formula, that valuation is used for computing values of independent ursa **variables. For this, only the basic variables are relevant**
(and not the definitional variables introduced during transformation to cnf**). Each satisfying valuation determines a vector of fixed Boolean values that correspond to an independent**
variable. The numerical (and Boolean) values are trivially **computed from such representations and returned by the** ursa **system.**
7. Pragmatics of ursa Language Representation of symbolic values natively used in ursa corresponds to binary representation of unsigned integers, but the specification language **is expressive enough and leaves**
enough freedom for modelling problems in substantially different ways and in different encoding styles, leading to simpler or more efficient solutions. For illustrating this, a prototypical csp example - the queens problem is considered. The problem is to **place** N
chess queens on an N × N **chessboard such that none of them is able to capture any other** (following the standard chess queen's moves). For modelling this problem, in the following text we do not use symmetry breaking or other similar additional constraints, but only the basic formulations of the problem.

Since each row (denoted by numbers 0 to N − **1) of the board can have exactly one**
queen on it, the problem is, simply reformulated, to determine, for each row, a column for one queen to be placed. Hence, a solution to the problem is a sequence r0, r1, **. . .**, rN−1 that meet the given constraints. If such sequence is given in **advance, it can be simply**
checked whether it is indeed a solution of the problem. The next ursa **program, followed** by a fragment of the output, specifies the problem (for the problem size 8; in this and other ursa specifications that follow, the dimension of an instance can **be trivially changed in** one line).

/* ***** queens-1 ***** */
nDim=8; bDomain = true; bNoCapture = true; for(ni=0; ni<nDim; ni++) {
bDomain &&= (n[ni]<nDim);
for(nj=ni+1; nj<nDim; nj++)
bNoCapture &&= n[ni]!=n[nj] && ni+n[nj]!=nj+n[ni] && ni+n[ni]!=nj+n[nj];
}
assert_all(bDomain && bNoCapture);
*************************************
********* URSA Interpreter ********* *************************************
--> Solution 1 n[0]=0 n[1]=6