new, special-purpose solver. The general problem solving systems include libraries for general purpose programming languages, but also modelling and **programming languages built**
on top of specific solvers [36, 33, 42, 14]. Most modelling languages are highly descriptive and have specific language constructs for certain sorts of constraints. Specific constraints are translated to underlying theories by specific reduction **techniques. Some modelling systems use** sat as the target problem [31, 35] and some of them focus on solving np**-complete**
problems by reduction to sat **[10].**
In this paper we present a novel approach for solving problems by reducing them to sat**. The approach can be seen also as a general-purpose constraint programming system** (for finite domains). The approach consists of a new specification/modelling language ursa
(from Uniform Reduction to SAt) and an associated interpreter. In contrast to other modelling languages, the proposed language combines features **of declarative and imperative**
programming paradigms. What makes the language declarative is not how the constraints are expressed, but only the fact that a procedure for finding solutions does not need to be explicitly given. On the other hand, the system has features **of imperative languages and**
may be seen as an extension of the imperative programming paradigm,1**similarly as some**
constraint programming systems are extensions of logic programming paradigm. In contrast to other modelling languages, in the proposed specification **language loops are represented**
in the imperative way (not by, generally more powerful, recursion), destructive updates are allowed, there is support for constraints involving bitwise operators and operators for arithmetic modulo 2n. There are problems for which, thanks to these features, the **modelling**
process is simpler and specifications are more readable and easier to maintain than for other languages and constraint systems. However, of course, the presented system does not aim to replace other constraint systems and languages, but rather to provide a new alternative with some distinctive features.

The used uniform approach enables a simple syntax and semantics of the ursa **language,**
a simple, uniform reduction to sat **and, consequently, a simple architecture of the whole** system. This enables a straightforward implementation of the proposed system and a rather straightforward verification of its correctness. This is very important because, although it is often easier for a declarative program than for a corresponding imperative program to verify that it meets a given specification, this still does not lead to a high confidence if the constraint solving system itself cannot be trusted.

The presented approach is accompanied with an open-source implementation, publicly available on the Internet. A limited experimental comparison suggest that the system (combined with state-of-the-art sat **solvers) yields good performance, competitive to other**
modern approaches.

Overview of the paper. In Section 2 we give relevant definitions; in Section 3 we provide motivation and basic ideas of the proposed approach. In Section 4 we describe the specification language ursa**, in Section 5 its semantics, in Section 6 the corresponding interpreter,**
and in Section 7 pragmatics of the language. In Section 8 we discuss related techniques, languages and tools. In Section 9 we discuss directions for future work and in Section 10 we draw final conclusions.