significantly different forms [63]. There are a number of both theoretical and practical studies and comparisons between different encoding schemes. Since the log encoding lacks the propagation power of the direct and support encodings, it typically leads to less efficient solutions, compared to these two [72, 28]. The order encoding gives better performance compared with the direct encoding and the support encoding for some csp **problems [66].** Within the ursa **system, numerical variables are represented using binary representation**
that corresponds to the compact encoding, but still, thanks **to the expressiveness of the** specification language, other encoding styles can be simulated and used (as shown by the presented examples).

The ursa **system is related to the special-purpose system for transforming cryptanalysis of hash functions into the** sat **problem [39]. In that approach, implementations of**
hash functions in C++ were used and, by overloading the standard arithmetic and logical operators in C++ and by running the code of the hash functions **within such framework,**
propositional formulae corresponding to cryptanalysis tasks were generated (and then solved by a sat **solver). Similar approach was also used for cryptanalysis of** des **[71].** ursa is a general framework aimed not only to cryptanalysis tasks, but to a much wider range of problems. The framework consists of both a modelling language (instead of C++) and the solving machinery, tightly integrated. The system is stand-alone, does not involve the C++
language in the modelling process, and the language itself defines the modelling power of the approach. The related, C++ based approach, has an advantage that the specification can be used directly as a C++ code, but ursa **specifications can often be used as C code** in verbatim.

There are several general-purpose constraint solving systems based on sat**. Thanks**
to the advances in sat **technology, such systems can be very efficient, despite the main** weakness of this approach: a domain knowledge and a global structure of the problem are lost when it is reduced to the simple propositional logic. sugar21 **is a** sat**-based constraint**
solver that uses the order encoding [66]. It is focused on compiling finite linear csp **into** sat. sugar **uses a syntax of** csp **that is designed to cover the notation of the** xcsp 2.1 format. FznTini22 is a general constraint solver that solves constraint satisfaction and optimization problems (not involving floating point numbers) **given in the general constraint**
language FlatZinc **(typically produced from** MiniZinc **specifications) by translating them**
to sat **and calling a** sat **solver** Tinisat **[35]. The system can be also used for translating to** sat **only (so, it can be used by independent** sat **solvers).** FznTini **uses a fixed**
encoding directly related to binary representation of integers (the two's complement representation) that corresponds to the compact encoding. NPSpec **is a modelling language**
for constraint problems, going with a tool Spec2Sat **that compiles specifications into** sat instances [11]. NPSpec **uses a highly declarative style of programming, similar to Datalog**
(a query language for deductive databases). The semantics of NPSpec **is based on the** model minimality, an extension of the least fixed point semantics of the Horn fragment of first order logic [11]. The system mxg23, focused on np**-hard problems, uses a modelling**
language based on classical first order logic, and for a given **specification produces a propositional formula (and passes it to a** sat **solver) [51, 58]. The system can also translate**
problem specification to sat **extended with cardinality constraints.**
21**http://bach.istc.kobe-u.ac.jp/sugar/**
22**http://users.cecs.anu.edu.au/~jinbo/fzntini/**
23http://www.cs.sfu.ca/research/groups/mxp/