URSA：一个统一归约为SAT的系统
URSA: A System for Uniform Reduction to SAT
摘要：
有大量的问题，从不同的领域，正在解决减少他们的SAT。然而，对于许多应用程序，翻译成SAT是由专门的，特定于问题的工具。在本文中，我们描述了一个新的系统，统一解决了广泛的一类问题，减少他们SAT。该系统使用了一种新的规约语言URSA，结合了命令式和声明式编程范例。对SAT的简化由规约语言的语义精确定义。该方法的域很宽（例如，许多NP完全问题可以简单地指定，然后由该系统解决），并且存在容易由所提出的系统解决的问题，而它们很难通过使用其他程序设计语言或约束程序设计系统来解决。因此，该系统不仅可以被视为通过将问题简化为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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
