Apart from systems that can translate problem specifications to sat**, there are also**
systems that translate such specifications to smt**. For instance,** fzn2smt **[5] translates from** the FlatZinc **language and the system** simply **[4] translates from a declarative modelling**
language similar to, but simpler than MiniZinc**. Both systems translate to the standard**
smt-lib format24 **and can use various underlying** smt **theories and available** smt **solvers.**
The system ursa **and the above systems share the underlying solving technology, but**
their specification languages are very different. In contrast to ursa**, all of the above tools use** declarative languages, and they don't have features of imperative languages (e.g., destructive assignments), as discussed in Section 8.2. Also, the languages used by the above tools provide support for various operators and global constraints, but typically do not support bit-wise operators and constraints involving modular arithmetic, which can be essential in many cases. This way, the input languages restrict the tools **from having the full power** of modelling in propositional logic. Concerning expressiveness, sugar and FznTini use rather simple, low-level specification language without flow control structures and other features of programming languages that ursa **has. Using representation based on binary** representation of integers is very similar in FznTini and ursa **(with a minor difference that** FznTini **uses the two's complement representation).**
8.4. Experimental Comparison. **It is very difficult to make a fair and thorough comparison of the modelling systems: they were not built with the same motivation and purposes;**
it is not only performance that is important but also expressiveness and ease of acquiring a modelling language; some systems perform better on some sorts of problems (and worse on the other); a single problem can be often specified in different **ways; most systems do not**
share the same input language (even if they do, some types of specifications may be better suited to some systems); the leading systems are under ongoing developments, and there are new features being added constantly; there are new emerging systems, etc. Still, with all of the above cautious, several (a very few, likely due to the above difficulties) existing reports give some general picture of efficiency of systems for **constraint solving over finite**
domains [24, 43, 21] while new insights are provided by a number of system competitions recently initiated.

For experimental comparison with the ursa **system, we used the following state-ofthe-art systems (and versions), including several industrial ones: constraint logic programming systems** B-Prolog 7.425 and SICStus 4.1.126 **(with the** clpdf **module), a deductive**
database system (using Disjunctive Datalog language that combines databases and logic programming) dlv27 **[42],** asp **solvers (used with** Smodels **specifications and a grounder**
Lparse **1.1.2)** clasp 1.3.228 **[27],** Cmodels 3.7929 **[31] and** Smodels 2.3430 **[65], hybrid optimization system (using a custom object-oriented programming language)** comet **2.1.1**31
[49], a hybrid optimization system (using a custom declarative modelling language) ibm 24**http://www.smtlib.org/** 25**http://www.probp.com/** 26**http://www.sics.se/isl/sicstuswww/site/** 27**http://www.dbai.tuwien.ac.at/proj/dlv** 28**http://www.cs.uni-potsdam.de/clasp/**
29**http://www.cs.utexas.edu/~tag/cmodels/**
30**http://www.tcs.hut.fi/Software/smodels/** 31http://dynadec.com