DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
针对SMT重要子集SMMT缺乏高效不可满足性证明生成方法的问题，提出基于理论谓词命题定义生成紧致Horn近似以得到DRAT证明的方法，开销低且可处理此前难处理的问题。
2024-04-18 cs.LO
Local Search For Satisfiability Modulo Integer Arithmetic Theories
开发了首个直接操作变量的SMT(IA)局部搜索算法LS-IA，设计针对整数算术的操作符、评分函数和两级选择启发式，实验证明其与Z3组合提升了SMT-LIB可满足基准集上的现有水平。
2023-05-17 cs.LO
Complete Trigger Selection in Satisfiability modulo first-order Theories
本文证明在SMT求解器中，当触发器函数与文字选择函数一致时，量词实例化对饱和子句集是完备的，并给出停机条件及Horn或2SAT情形的多项式时间求解。
2023-06-21 cs.LO
Satisfiability.jl: Satisfiability Modulo Theories in Julia
本文介绍 Julia 开源包 Satisfiability.jl，通过高级接口连接兼容 SMT-LIB 的求解器，以便更便捷地编写复杂 SMT 公式并支持形式化验证。
2023-12-16 cs.LO cs.MS
Separation Logic Modulo Theories
关于程序数据的逻辑推理通常需要处理堆结构以及标量数据类型。可满足性模块化理论（SMT）的最新进展已经提供了处理标量的有效程序，但它们缺乏对处理堆结构的任何支持。在本文中，我们提出了一种方法，集成了分离逻辑-一个突出的逻辑推理表段的堆-和SMT。我们遵循基于模型的方法，在SMT求解器和分离逻辑推理部分之间的堆单元之间传递别名。使用Z3求解器的实验评估表明，我们的方法可以有效地把工作的SMT处理堆结构的进步。这是分离逻辑与SMT理论相结合的第一个决策过程。
2013-03-11 cs.LO
Temporal Stream Logic modulo Theories (Full Version)
时态流逻辑（TSL）在任意函数项上通过更新和谓词扩展LTL。这允许指定LTL表达能力不足的数据密集型系统。在TSL的语义中，函数和谓词是不解释的。在本文中，我们扩展TSL与一阶理论，使我们能够指定系统使用解释功能和谓词，如增量或相等。我们调查的可满足性问题TSL模的标准基础理论的未解释的功能，以及相对于Presburger算法和理论的平等：对于所有这三个理论，TSL可满足性是高度不可判定的。然而，我们确定了三个片段的TSL的可满足性问题是（半）不可判定的理论解释的功能。尽管高的不可判定性，我们提出了一种算法-这是不保证终止-用于检查可满足性的TSL公式在理论的未解释的功能和评估：它的规模以及能够验证假设在现实世界中的系统设计。
2022-01-25 cs.LO
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
Stanford University（斯坦福大学）
本文提出了一种新的决策过程，用于支持常量数组的数组理论，能够处理任意索引域，并不局限于无限情况。
2026-07-22 cs.LO
Computing Tropical Prevarieties with Satisfiability Modulo Theories (SMT) Solvers
一种新的方法，使用SMT（可满足性模理论）求解器来计算热带前变（分别）。平衡）的多项式系统。新的方法是基准对一个天真的方法，使用纯粹的多面体的方法。事实证明，SMT方法比多面体方法更快，否则需要一分钟以上的计算时间，在许多情况下是60倍或更多，在最坏的情况下只是慢了两倍。此外，新的方法是一个随时算法，从而提供了一种方法来计算部分的解决方案时，多面体的方法是不可行的。
2020-06-26 cs.CG cs.LO
Satisfiability Modulo Theories for Verifying MILP Certificates
针对MILP求解器结果正确性问题，提出基于SMT-LIB的VIPR证书验证方法，通过编码推理规则并使用Why3框架形式化验证，实现了求解器无关的证书检查。
2025-10-12 cs.LO
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
我们介绍了一种方法，旨在结合使用的可满足性模理论（SMT）求解器的组合逻辑合成器（CL）的框架。(CL)S是一种用于从用户指定的存储库自动组合软件组件的工具。该框架产生一个树语法，其中包含符合目标类型的所有组合术语。（CL）S的类型规范基于具有交集类型的组合逻辑。我们的方法将树语法转换为SMT功能，这允许考虑额外的特定于域的约束。我们证明了我们的方法在几个实验中的实用性。
2019-08-26 cs.FL cs.LO
Grammatical Inference as a Satisfiability Modulo Theories Problem
Institute for Computing；Information Sciences Radboud University Nijmegen, The Netherlands Email
从可满足性模理论的角度研究了从一组标记符号序列中学习最小一致模型的问题。我们提出了两种编码确定性有限自动机和扩展这些Moore和Mealy机之一。我们的实验结果表明，这些编码提高了国家的最先进的，是有用的，在实践中学习小模型。
2017-05-30 cs.FL cs.LG cs.LO
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
在SAT和SMT中计算Craig插值的问题最近受到了很大的关注，主要是因为它在形式化验证中的应用。插值生成的有效算法已经提出了一些理论的利益-包括平等和未解释的功能，线性算术的有理数，以及它们的组合-他们成功地使用在模型检验工具。然而，对于整数上的线性算术理论（LA（Z）），找到插值的问题更具挑战性，并且为完整理论LA（Z）开发有效的插值生成器的任务仍然是正在进行的研究的目标。在本文中，我们试图缩小这一差距。我们建立在以前的工作，并提出了一种新的插值算法的SMT（LA（Z）），它利用了当前最先进的SMT（LA（Z））求解器的全部功能。我们证明了我们的方法的潜力与我们的实施所提出的算法在MathSAT SMT求解器的广泛的实验评估。
2012-08-09 cs.LO
A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
本研究提出将线性时序逻辑模理论LTL-MT规约为符号数据字自动机SDWAs的新方法，可转化为约束霍恩子句求解，适用于模型检测等场景，实验表现不逊于现有定制方案。
2024-08-16 cs.LO
Satisfiability and Synthesis Modulo Oracles
University of Edinburgh（爱丁堡大学）；UC Berkeley（加州大学伯克利分校）；University of Iowa（爱荷华大学）
在经典的程序合成算法中，例如反例引导归纳合成（CEGIS），算法在合成阶段和预言（验证）阶段之间交替。许多合成算法使用基于可满足性模理论（SMT）求解器的白盒预言机来提供反例。但是，如果白盒Oracle不可用或不容易使用，该怎么办？我们提出了一个框架来解决一般类的预言指导的合成问题，我们长期合成模预言。在这种情况下，预言机可以是黑盒子，具有由合成问题定义的查询-响应接口。作为该框架的一个必要组成部分，我们还形式化了可满足性模理论和预言机问题，并提出了一个算法来解决这个问题。我们实现了一个原型求解器的可满足性和合成模神谕，并证明，通过使用神谕执行功能不容易建模SMT约束，如递归函数或神谕，将编译和执行的代码，SMTO和SyMO能够解决超出标准SMT和合成求解器的能力的问题。
2021-07-28 cs.LG cs.LO cs.PL
From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach
本文提出首个理论反应式合成方法，结合布尔化LTL静态控制器与动态求解器查询，实现理论中的完整控制器合成。
2023-10-11 cs.LO
Modulo quantifiers over functional vocabularies extending addition
本文证明满足位置范式的扩展加法的纯函数词汇表上的FO和FOMOD逻辑具有CBP，并指出证明FOMOD[<,+,2^x]无法定义所有正则语言等价于分离电路复杂性类ACC0和NC1。
2025-02-01 cs.LO
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
我们提出了一个简单的决议证明系统高阶约束霍恩条款（HoCHC）-系统的高阶逻辑模理论-并证明其可靠性和反驳的完整性w.r.t.标准语义。作为推论，我们得到了HoCHC的紧性定理和半可判定性的背景理论，我们证明了HoCHC满足一个典型的模型性质。此外，从高阶到1阶逻辑的著名的翻译的一个变体被证明是健全的和完整的HoCHC在标准语义。我们说明了如何转移的可判定性结果（片段）一阶逻辑模理论，我们的高阶设置，作为例子的Bernays-Schonfinkel-Ramsey片段HoCHC模的限制形式的线性代数算术。
2019-04-19 cs.LO
Satisfiability Modulo ODEs
Carnegie Mellon University（卡内基梅隆大学）
研究包含常微分方程的实数SMT问题，开发了delta完整算法以处理纯存在性量化和受限时间变量全称量化的公式，通过dReal求解器在大规模非线性ODE和变量基准上展示算法可扩展性。
2013-10-30 cs.LO cs.SY eess.SY
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Department of Computer Science, Purdue University, IN, USA（计算机科学系，普渡大学）
本文提出KOCO-SMC，一种集成的精确模计数可满足性求解器，通过跟踪上下界和部分变量赋值实现早期估计，显著提升求解效率。
2025-06-17 cs.AI cs.LO
Neuro-Symbolic Constrained Optimization for Cloud Application Deployment via Graph Neural Networks and Satisfiability Modulo Theory
本文提出基于图神经网络和可满足性模理论的神经符号框架，用于优化云应用部署，通过结合约束推理与机器学习提升求解器的可扩展性和成本最优性。
2025-11-28 cs.LO
Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
针对OMT中完全真值指派枚举易过度限制搜索空间的问题，提出利用部分指派枚举的指派约简技术，在OptiMathSAT中实现并经基准测试验证，可提升最优求解效率与随时求解的解质量。
2025-05-18 cs.LO
Representing Hybrid Automata by Action Language Modulo Theories
Arizona State University（亚利桑那州立大学）；Houzz Inc.（Houzz 公司）
混合自动机和动作语言都是描述动态系统演化的形式化方法。本文建立了它们之间的正式关系。我们展示了如何简洁地表示混合自动机的动作语言，这反过来又被定义为一个高层次的符号的答案集编程模理论（ASPMT）-一个扩展的答案集程序的一阶水平类似的方式可满足性模理论（SMT）扩展命题可满足性（SAT）。首先，我们展示了如何表示线性混合自动机的凸不变量的行为语言模理论。进一步翻译成SMT允许使用支持实数运算的SMT求解器来计算它们。接下来，我们将表示扩展到一般类的非线性混合自动机，甚至允许非凸不变量。我们表示它们的动作语言模ODE（常微分方程），它可以被编译成可满足模ODE。我们开发了一个原型系统cplus 2aspmt的基础上，这些翻译，它允许一个简洁的表示的混合过渡系统，可以有效地计算的最先进的SMT求解器dReal。
2017-07-25 cs.AI cs.FL cs.LO
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）
本文研究有限迹上的线性时态逻辑（LTLf），其中命题字母被替换为任意理论上的一阶公式，其思想是可满足性模理论。由此产生的逻辑，称为LTLf模理论（LTLfMT），是半可判定的。尽管如此，它的高表现力在许多用例中非常有用，例如数据感知流程的模型检查和数据感知规划。尽管这些问题通常是不可判定的，但能够解决可满足的实例是一个值得研究的折衷方案。在激励和描述这样的用例之后，我们提供了一个基于单通道树形tableau系统的SMT编码的LTLfMT的健全和完整的半决策过程。该算法在BLACK可满足性检查工具中实现，并在新的基准测试上进行了实验评估，结果表明了该方法的可行性。
2022-05-24 cs.AI cs.LO
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
针对MCSat求解非线性整数算术SMT问题时赋值选择影响性能的问题，提出融合局部搜索的引导框架，结合加速爬山与可行集跳转实现于Yices2，并在SMT-LIB基准上完成评估。
2025-07-23 cs.LO
Satisfiability of CTL* with constraints
我们证明了在Z上具有等式，顺序和模约束的CTL* 的可满足性是可判定的。以前，仅知道CTL* 的某些片段的可判定性，例如，存在主义和积极的碎片和EF。
2013-06-04 cs.LO
Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
Purdue University（普渡大学）
提出XOR-SMC算法，通过随机化XOR约束将NP^PP-完全的模计数可满足性问题转化为SAT问题，在多项式时间内提供常数近似保证，并在AI向善实验中优于基线。
2023-12-30 cs.AI cs.CC cs.LO
Speculative SAT Modulo SAT
本文提出 SMS 的推广方法 SPEC SMS，通过在模块间推测性地进行决策和双向交换学习子句，克服了原有模块化 SAT 求解的单向性限制，并在 Z3 中实现，在困难基准测试上呈指数级提升性能。
2023-06-30 cs.FL cs.LO
Co-Certificate Learning with SAT Modulo Symmetries
TU Wien（维也纳工业大学）
本文提出共证书学习扩展SMS框架，用于生成满足共NP性质的图，并改进Kochen-Specker向量系统下界，方法更快且扩展性更优。
2023-06-21 cs.AI cs.DM cs.LO
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
University of California, Berkeley（加利福尼亚大学伯克利分校）
针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。
2023-10-18 cs.AI cs.LO cs.PL
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
FBK-IRST（布鲁诺·凯斯勒基金会-材料与微系统研究所）
寻找SAT公式的小不可满足核的问题最近受到了广泛的关注，主要是因为它在形式化验证中的应用。然而，命题逻辑往往是不够的表达，表示许多有趣的验证问题，这可以更自然地解决的框架可满足性模理论，SMT。令人惊讶的是，在SMT中找到不可满足的核心的问题在文献中很少受到关注。在本文中，我们提出了一种新的方法来解决这个问题，称为引理提升方法。其主要思想是将SMT求解器与外部命题核心提取器相结合。SMT求解器产生在搜索期间发现的理论引理，动态地将适量的理论信息提升到布尔级别。核心提取器，然后调用原始SMT问题和理论引理的布尔抽象。这将导致一个不可满足的核心，为原来的SMT问题，一旦剩余的理论引理被删除。这种方法在概念上很有趣，在实践中有几个优点。事实上，它的实现和更新非常简单，并且它可以以即插即用的方式与每个命题核心提取器接口，以便免费受益于已经或将要提供的所有未饱和核心还原技术。我们已经评估了我们的算法与一个非常广泛的实证测试SMT-LIB基准，这证实了这种方法的有效性和潜力。
2014-01-16 cs.AI cs.LO
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
简单线性实算术约束BS（SLR）上的Bernays-Schönfinkel一阶逻辑片段已知是可判定的。我们证明了BS（SLR）子句集的普遍和存在量化的验证条件（条件）可以转换为BS（SLR）子句集的一阶常数的有限集。对于霍恩的情况下，我们提供了一个保留有效性和可满足性的数据锤。从BS（LRA）证明器SPASS-SPL到Datasheet推理器VLog的工具链建立了一种有效的方法来确定Horn片段中的验证条件。这通过验证用于汽车中的车道变换辅助的管理器代码和用于增压燃烧发动机的电子控制单元来举例说明。
2021-07-07 cs.LO
Threat Repair with Optimization Modulo Theories
我们提出了一个基于模型的程序，使用正式的模型自动防止安全威胁。我们将系统模型和潜在威胁编码为可满足性模理论（SMT）公式。该模型允许我们将安全问题作为可满足性查询。我们制定威胁预防作为一个优化问题，在相同的公式。我们的威胁预防过程的结果是一个建议的模型属性修复，消除威胁。每当威胁预防失败时，我们就会自动解释威胁发生的原因。我们使用最先进的Z3 SMT求解器实现我们的方法，并将其与威胁分析工具THREATGET相结合。我们证明了我们的程序的价值，在两个案例研究，从汽车和灵巧家庭领域，包括一个工业强度的例子。
2022-10-06 cs.CR cs.FL cs.LO
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
在过去的十年中，我们已经目睹了一个令人印象深刻的进步，表现力和效率的可满足性模理论（SMT）解决技术。这给最先进的SMT求解器带来了以前难以解决的问题，特别是在软件和硬件验证领域。然而，许多感兴趣的SMT编码问题，也需要找到最佳wrt模型的能力。一些成本函数。在以前的工作中，即“优化模理论与线性有理成本函数- OMT（LAR UT）”，我们利用SMT解决处理成本函数的线性算术的最小化的理由，通过SMT和LP最小化技术的组合。在本文中，我们沿着三个方向推进了OMT方法：首先，我们通过SMT、LP和ILP最小化技术的组合，将其扩展到混合整数/有理数域上的线性运算;其次，我们开发了一个多目标版本的OMT，以便同时处理多个成本函数;第三，我们开发了一个OMT的增量版本，以便利用一些OMT可编码问题的增量性。OMT编码的验证问题上进行的实证评估表明，这些扩展的有用性和效率。
2015-01-16 cs.LO
Generalized Optimization Modulo Theories
本文提出广义优化模理论（OMT），引入基于偏序集目标函数的抽象演算，统一单/多目标优化并支持与理论无关的求解，为OMT方法建立理论基础。
2024-04-29 cs.LO
Decidable Fragments of LTLf Modulo Theories (Extended Version)
University of Udine（乌迪内大学）；Free University of Bozen-Bolzano（博尔扎诺自由大学）
本文研究有限迹上的线性时序逻辑模理论（LTLfMT），提出可靠完备的剪枝规则，证明满足“有限记忆”条件的公式其 tableau 可终止，并由此确立多个 LTLfMT 片段可满足性的新可判定性结果。
2023-07-31 cs.AI cs.LO
How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics
在具有硬实时约束的系统中，有必要计算程序的最坏情况执行时间（WCET）的上界;越接近真实的WCET越好。对于具有固定时钟的同步无功控制回路尤其如此;循环体的WCET不得超过时钟周期。我们计算的WCET（或至少是一个封闭的上限）的解决方案的优化模理论的问题，考虑到语义的程序，在其他方法计算最长的路径是否是可行的，根据这些语义。优化模理论将可满足性模理论（SMT）扩展到最大化问题。将WCET问题立即编码为SMT产量公式对于所有当前的生产级求解器来说都是棘手的;这是在这些求解器中实现的SMT的DPLL（T）方法所固有的。通过结合一些适当的“削减”这些公式，我们大大减少了SMT求解器的计算时间。我们实验了我们的方法对各种控制程序，使用OTAWA分析仪作为基线和底层的微架构分析，我们的分析，并显示出显着的改善WCET绑定在各种基准和控制程序。
2014-05-30 cs.LO cs.PL
ASPMT(QS): Non-Monotonic Spatial Reasoning with Answer Set Programming Modulo Theories
University of Warsaw（华沙大学）；University of Bremen（不来梅大学）
\emph{dynamic spatial systems} [9]的系统建模是广泛应用领域的关键要求，例如常识认知机器人、计算机辅助建筑设计、动态地理信息系统。我们提出了ASPMT（QS），一种新的方法和完全实现的原型非单调空间推理--动态空间系统内的一个关键要求-基于答案集编程模理论（ASPMT）。ASPMT（QS）包括一个（定性）空间表示模块（QS）和一种方法，用于将紧密的ASPMT实例转换为SAT模理论（SMT）实例，以便通过SMT求解器计算稳定的模型。我们正式和实施的默认空间推理和空间框架公理的概念，使用选择公式。空间推理是通过将空间关系编码为多项式约束系统，并利用实非线性算法理论通过SMT求解来实现的。我们经验评估ASPMT（QS）与其他著名的当代空间推理系统相比。我们的研究结果表明，ASPMT（QS）是唯一现有的系统，能够推理的间接空间效应（即解决分歧的问题），并整合几何和定性空间信息的非单调空间推理上下文。
2015-06-16 cs.AI cs.LO
Verification of Provers and Solvers
University of Innsbruck（因斯布鲁克大学）
介绍自动推导工具与证明助手的连接方法，通过认证和验证等方式，回顾比较现有方法并提及成功应用。
2026-07-29 cs.LO cs.SC
Shield Synthesis for LTL Modulo Theories
IMDEA Software Institute（IMDEA软件研究所）；Cornell University（康奈尔大学）；University of California, Irvine（加州大学欧文分校）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）
针对机器学习模型在安全关键系统中存在的不安全行为问题，本研究提出一种基于LTL模理论的屏蔽合成方法，解决现有屏蔽技术仅适用于命题逻辑的局限，实现更丰富逻辑下的安全保障。
2025-02-14 cs.AI cs.LG cs.LO
Interpolation and Model Checking for Nonlinear Arithmetic
提出了一种新的基于模型的可满足性模理论插值方法。该过程使用了一种新的与SMT求解器的交互模式，我们称之为求解模模型。这要么将给定的部分模型扩展为一组断言的完整模型，要么在不存在解决方案时返回解释（模型插值）。这种交互模式非常适合SMT的模型构建可满足性（MCSAT）框架。我们用它来开发任何MCSAT支持的理论的插值程序。特别是，这种方法导致了一个有效的非线性实算术插值程序。我们评估新的程序，将其集成到一个模型检查器，并将其与最先进的非线性算法的模型检查工具进行比较。
2021-06-08 cs.LO cs.PL cs.SC
