Janicic, Predrag - URSA: A System for Uniform Reduction to SAT

lmcs:1171 - Logical Methods in Computer Science, September 30, 2012, Volume 8, Issue 3
URSA: A System for Uniform Reduction to SAT

Authors: Janicic, Predrag

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.

DOI : 10.2168/LMCS-8(3:30)2012
Volume: Volume 8, Issue 3
Published on: September 30, 2012
Submitted on: March 8, 2011
Keywords: Computer Science - Artificial Intelligence,F.4.1, D.3.2


Consultation statistics

This page has been seen 170 times.
This article's PDF has been downloaded 300 times.