- **the user has a fuller control of internal representation of the problem, so can influence**
the efficiency of the solving phase.

- **a specification can be taken, almost as-is, from and to languages such as C (within C,**
such code would check if some given concrete values are indeed a solution of the problem).

- **the system can smoothly extend imperative languages like C/C++ or Java, (as constraint**
programming extends logic programming).

- **the system can be verified to be correct in a straightforward manner.**
In addition, the system ursa**, in contrast to most of (or all) other modelling systems,**
supports bit-wise logical operators and constraints involving modular arithmetic (for the base of the form 2n**), which is essential for many applications, and can also enable efficient**
problem representation and problem solving.

The proposed approach can be used for solving all problems with Boolean and numerical unknowns, over Boolean parameters and numerical parameters with finite domains that can be stated in the specification language (e.g., the domain of the system is precisely determined by expressiveness of its specification language).

The search for required solutions of the given problem is performed by modern sat solvers that implement very efficient techniques not directly applicable to other domains.

While sat is already used for solving a wide range of various problems, **the proposed system** makes these reductions much easier and can replace a range of **problem-specific tools for** translating problems to sat**. The tool** ursa **can be used not only as a powerful general**
problem solver (for finite domains), but also as a tool for generating sat **benchmarks (both**
satisfiable and unsatisfiable).38 Concerning weaknesses, ursa is not suitable for problems where knowledge of the domain and problem structure are critical and can be efficiently **tackled only by specialized**
solvers, and this holds for reduction to sat **generally. Due to its nature, by interfacing** ursa with standard specification languages like xcsp or MiniZinc**, most of the** ursa **modelling** features and power would be lost (e.g., bit-wise logical operators and destructive updates), while global constraints supported by these languages would be translated in an inefficient way. Therefore, it makes no much sense to enable conversion from these standard languages to ursa **and this makes** ursa **a bit isolated system in the world of constraint solvers or** related systems.

In this paper we do not propose:
- **a new** sat**-encoding technique - rather, the** ursa **specification language can be used for**
different encoding styles;
- **a technique for transforming a** sat **formula to conjunctive normal form - this step is**
not a part of the core of the ursa **language and is not covered by its semantics, so any** approach (meeting the simple specification) can be used; the **current technique seem to** work well in practice, while it can still be a subject of improvements.

- a sat **solver - rather,** ursa **can use any** sat **solver (that can generate all models for**
satisfiable input formulae); moreover, having several sat **solver would be beneficial, since** some solvers are better suited to some sorts of problems.

In this paper we also described the system ursa **that implements the proposed approach and provided some experimental results and comparison with related systems. They**
38**A large number of** sat **instances obtained from cryptanalysis of** des [71] (by using simpler version of the system proposed in this paper), were part **of the** sat **Competition corpus**
(http://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf).