Example 8.1 illustrates one family of problems that can be simply solved by the ursa system. Specifications of functions in C (analyzed if they are equivalent) can be almost in verbatim used within ursa**, while it would be extremely difficult to represent this kind of**
problems in existing declarative programming languages - consider, for instance, complex functions (say, like cryptographic functions) that involve a large number of destructive assignments in their specifications. Additional problem is **that the bitwise operators are**
not supported in other modelling systems.

Example 8.1. **One of the common problems in software verification is ensuring that two**
implementations are equivalent. The ursa **system can be suitable for such tasks. Consider,** for example, two implementations (both based on C-style bitwise operators) of the check that the input number n **has in its representation exactly one bit set: the first (encoded by**
b1) is rather compact, while the second (encoded by b2**) is more elaborated but simpler.** ursa **(for the vector length for representation of numbers equal** nLen**), verifies that the**
condition b1^^b2 **is unsatisfiable, hence the two implementations give the same result for**
any input number.

b1 = (nv!=0) && ((nv & (nv-1))==0);
nLen=8; bOne = false; bMoreThanOne = false; for(ni=0; ni<nLen; ni++) {
bMoreThanOne ||= bOne && ((nv & 1)!=0);
bOne ||= ((nv & 1)!=0);
nv >>= 1;
} b2 = bOne && !bMoreThanOne; assert(b1^^b2);
8.3. **Reduction to** sat and sat-Based Constraint Solvers. **There are a huge number**
of problems solved by reduction to sat**, in a range of domains (e.g., in scheduling [74],** termination analysis [25], cryptanalysis [48, 50], model checking [12], to name just a few).

One of the reasons for such a wide application range are tremendous advances in sat technology over the last years and a number of efficient solvers. The ursa **system does not**
introduce or promote one sat **solver. Rather,** ursa **can use any** sat **solver in the solving** phase. Moreover, it is fruitful to have, within ursa**, a number of different** sat **solvers,** appropriate for different sorts of input problems, following **ideas of** sat **portfolio solvers** [55].

There are several approaches for encoding csp **problems into** sat **[60]. Probably the**
most popular basic types of encodings into sat are: the sparse encoding, the compact encoding, and the order encoding **[34, 66]. In the sparse encoding, a propositional variable**
xv,i is defined as true iff the integer variable v has a value i **assigned to it. Examples of**
the sparse encoding are the direct encoding and the support encoding **[60]. In the compact**
encoding (or log encoding**), a propositional variable is assigned to each bit of each integer**
variable (within a finite domain) [60]. In the order encoding (also known as regular encoding**), related to many-valued logics and often used for the finite-domain linear problems, an**
inequality v ≤ i **is encoded by a different propositional variable for each integer variable** v and integer value i [66, 1]. Even within one encoding style, modelling of a problem can take