URSA: A System for Uniform Reduction to SAT
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1171/pdf |
| _version_ | 1797268694592651264 |
|---|---|
| author | Predrag Janicic |
| author_facet | Predrag Janicic |
| author_sort | Predrag Janicic |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:33Z |
| format | Article |
| id | doaj.art-5cd769dc64504ae8af4e435509a4546c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:33Z |
| publishDate | 2012-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5cd769dc64504ae8af4e435509a4546c2024-03-08T09:28:00ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-09-01Volume 8, Issue 310.2168/LMCS-8(3:30)20121171URSA: A System for Uniform Reduction to SATPredrag JanicicThere 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.https://lmcs.episciences.org/1171/pdfcomputer science - artificial intelligencef.4.1, d.3.2 |
| spellingShingle | Predrag Janicic URSA: A System for Uniform Reduction to SAT Logical Methods in Computer Science computer science - artificial intelligence f.4.1, d.3.2 |
| title | URSA: A System for Uniform Reduction to SAT |
| title_full | URSA: A System for Uniform Reduction to SAT |
| title_fullStr | URSA: A System for Uniform Reduction to SAT |
| title_full_unstemmed | URSA: A System for Uniform Reduction to SAT |
| title_short | URSA: A System for Uniform Reduction to SAT |
| title_sort | ursa a system for uniform reduction to sat |
| topic | computer science - artificial intelligence f.4.1, d.3.2 |
| url | https://lmcs.episciences.org/1171/pdf |
| work_keys_str_mv | AT predragjanicic ursaasystemforuniformreductiontosat |