| Summary: | There are a huge number of problems, from various areas, being solved by
reducing them to SAT. However, for many applications, translation into SAT is
performed by specialized, problem-specific tools. In this paper we describe a
new system for uniform solving of a wide class of problems by reducing them to
SAT. The system uses a new specification language URSA that combines imperative
and declarative programming paradigms. The reduction to SAT is defined
precisely by the semantics of the specification language. The domain of the
approach is wide (e.g., many NP-complete problems can be simply specified and
then solved by the system) and there are problems easily solvable by the
proposed system, while they can be hardly solved by using other programming
languages or constraint programming systems. So, the system can be seen not
only as a tool for solving problems by reducing them to SAT, but also as a
general-purpose constraint solving system (for finite domains). In this paper,
we also describe an open-source implementation of the described approach. The
performed experiments suggest that the system is competitive to
state-of-the-art related modelling systems.
|
|---|