URSA: A System for Uniform Reduction to SAT

TL;DR

URSA introduces a unified system that simplifies solving a wide range of problems by translating them into SAT using a novel specification language, combining imperative and declarative paradigms, and demonstrating competitive performance.

Contribution

The paper presents URSA, a new specification language and system for uniform problem reduction to SAT, enabling broad applicability and competitive performance.

Findings

System is effective for many NP-complete problems.

URSA's approach is competitive with state-of-the-art systems.

Open-source implementation is available for practical use.

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.