直接处理离散变量的原生SAT求解器，比传统方法更快更准确。
Dsat: A Native SAT Solver for Discrete Logic
- 设计原生离散逻辑的SAT求解器，支持任意取值变量
- 在离散逻辑上实现单元归结与子句学习，性能优于二值化方案
- 适合需要高效推理的可解释AI、规划等场景
离散变量广泛存在于概率推理、规划和可解释AI等领域。传统方法常将离散变量二值化为布尔变量，以使用布尔计算工具如SAT求解器。但该方法面临计算效率与语义失真的挑战。本文提出一种原生离散逻辑的SAT求解器，是布尔逻辑的自然扩展，变量可取任意值。其设计与布尔SAT求解器相似，包含单元归结、子句学习等机制，但直接作用于离散变量。通过与约束满足问题（CSP）求解器、二值化后的布尔SAT求解器及混合求解器的对比实验，验证了所提方法在离散合取范式（CNF）上的有效性与优势。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。