used as an underlying theory (instead of propositional logic) and any solver for bit-vectors arithmetic can be used as a solving engine. Generally, the reduction could be adaptable to smt **solvers available - if some solver is available, then its power can be used, otherwise all**
generated constraints are exported to propositional logic. This would make the approach more powerful and such development is the subject of our current work - the system ursa major **will be able to reduce constraints not only to** sat **but to different** smt **theories. That**
system will be a general constraint solver and also a high-level front-end to the low level smt-lib **interchange format, and, further, to all** smt **solvers that supports it. Reduction to** the theory of bit-vector arithmetic is firstly explored in this context [46] and it shows that reducing to bit-vector arithmetic does not necessarily lead to more efficient solving process than reducing to sat **(and the same holds for other** smt **theories).**
With the increased power of the presented system (by using both sat and smt **solvers),**
we are planning to further consider a wide range of combinatorial, np**-complete problems,**
and potential one-way functions and also to apply the ursa **system to real-world problems** (e.g., the ones that are already being solved by translating **them to** sat**). Some applications** in synthesis of programs are already the subject of our current work.

For the sake of easier practical usability of the ursa **system, we are planning to develop**
a support for integration of ursa **with popular imperative languages (C, C++, Java).**

## 10. Conclusions

In this paper we described a novel approach for uniform representation and solving of a wide class of problems by reducing them to sat**. The approach relies on:**
- **a novel specification language that combines features of imperative and declarative languages - a problem is specified by a test, expressed in an imperative form, that some**
values indeed make a solution to the problem;
- **symbolic computations over unknowns represented by (finite) vectors of propositional**
formulae.

The approach is general and elegant, with precisely defined syntax and induced (by the concept of symbolic execution) semantics of the specification language. This enables straightforward implementation of the system and it works as a "clear box". The proposed language is a novel mixture of imperative and declarative paradigms, leading to a new programming paradigm. Thanks to the language's declarative aspects - the problem is described by what makes a solution and not by describing how to find it - using the system does not require human expertise on the specific problem being solved. On the other hand, specifications are written in imperative form and this **gives the following advantages** compared to other modelling languages (all of them are declarative):
- **problem specifications can involve destructive assignments, which is not possible in declarative languages and this can be essential for many sorts of problems (e.g., from software**
verification);
- **modelling problems that naturally involve loops (and nested loops) is simple and the**
translation is straightforward;
- **for users familiar with imperative programming paradigm, it should be trivial to acquire**
the specification language ursa **(since there are no specific commands or flow-controls** aimed at constraint solving);