Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/513
Title: URSA: A system for uniform reduction to SAT
Authors: Janičić, Predrag 
Affiliations: Informatics and Computer Science 
Keywords: Constraint solving;SAT problem;Specification languages
Issue Date: 30-Sep-2012
Journal: Logical Methods in Computer Science
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.
URI: https://research.matf.bg.ac.rs/handle/123456789/513
DOI: 10.2168/LMCS-8(3:30)2012
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

14
checked on Dec 20, 2024

Page view(s)

26
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.