Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.

翻译：离散变量在许多应用中普遍存在，例如概率推理、规划与可解释人工智能。当符号推理技术被应用于这些场景时，处理离散变量的标准方法是将二值化处理为布尔变量，以便利用布尔计算工具（如SAT求解器）。然而，这种方法可能面临计算效率与语义表达两方面的挑战。本研究开发了一种面向离散逻辑的原生SAT求解器，该逻辑是布尔逻辑的直接扩展，其中变量可取值任意值。所提出的求解器采用与布尔SAT求解器类似的设计，包含单元归约与子句学习等机制，但这些机制原生地作用于离散变量。通过将本求解器与应用于离散合取范式的约束满足求解器、用于二值化合取范式的布尔SAT求解器以及若干混合求解器进行实验对比，我们展示了该SAT求解器的优势。