{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:31:41Z","timestamp":1770834701289,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,9,30]],"date-time":"2012-09-30T00:00:00Z","timestamp":1348963200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"Ministry of Education, Science and Technological Development of Republic of Serbia","award":["174021"],"award-info":[{"award-number":["174021"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>There are a huge number of problems, from various areas, being solved by\nreducing them to SAT. However, for many applications, translation into SAT is\nperformed by specialized, problem-specific tools. In this paper we describe a\nnew system for uniform solving of a wide class of problems by reducing them to\nSAT. The system uses a new specification language URSA that combines imperative\nand declarative programming paradigms. The reduction to SAT is defined\nprecisely by the semantics of the specification language. The domain of the\napproach is wide (e.g., many NP-complete problems can be simply specified and\nthen solved by the system) and there are problems easily solvable by the\nproposed system, while they can be hardly solved by using other programming\nlanguages or constraint programming systems. So, the system can be seen not\nonly as a tool for solving problems by reducing them to SAT, but also as a\ngeneral-purpose constraint solving system (for finite domains). In this paper,\nwe also describe an open-source implementation of the described approach. The\nperformed experiments suggest that the system is competitive to\nstate-of-the-art related modelling systems.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:30)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":9,"title":["URSA: A System for Uniform Reduction to SAT"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Predrag","family":"Janicic","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,9,30]]},"reference":[{"key":"587:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1171\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1171\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:05:28Z","timestamp":1681243528000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,30]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:30)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1012.1255","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1012.1255","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1080\/10556788.2019.1685993","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9,30]]},"article-number":"1171"}}