# Ursa: A System For Uniform Reduction To Sat Predrag Janici ˇ C´

Faculty of Mathematics, Studentski trg 16, 11000 Belgrade, **Serbia**
e-mail address**: janicic@matf.bg.ac.rs**
Abstract. **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.

## 1. Introduction

Following spectacular advances made over the last years, the sat **solving technology has** many successful applications nowadays - there is a wide range of problems being solved by reducing them to sat**. Very often solving based on reduction to** sat **is more efficient**
than using a problem-specific solution. Therefore, sat **solvers are already considered to**
be a Swiss army knife **for solving many hard** csp and np**-complete problems and in many** areas including software and hardware verification, model checking, termination analysis, planning, scheduling, cryptanalysis, electronic design automation, etc. [6, 3, 12, 25, 74, 48, 50]. Typically, translations into sat **are performed by specialized, problem-specific tools.** However, using a general-purpose system capable of reducing a wide range of problems to sat **can simplify this task, make it less error prone, and make this approach more easily** accessible and more widely accepted.

There are already a number of approaches for solving combinatorial and related problems by general-purpose systems that reduce problems to underlying theories and domains
(instead of developing special purpose algorithms and implementations). A common motivation is that it is much easier to develop a problem specification for a general system than a 1998 ACM Subject Classification: **F.4.1, D.3.2.**
Key words and phrases: sat **problem, constraint solving, specification languages.**