Modal Logic S5 Satisfiability in Answer Set Programming
University of Calabria（卡拉布里亚大学）；Technical University of Crete（克里特理工大学）；University of Huddersfield（哈德斯菲尔德大学）
本文提出使用回答集编程实现模态逻辑S5可满足性判定，通过可达性关系识别相关命题原子，实验表明该方法性能与基于SAT的先进求解器相当，而蕴含关系推理开销较大。
2021-08-09 cs.AI
Logic Programming with Satisfiability
本文提出了一个Prolog接口的MiniSat可满足性求解器。具有可满足性的逻辑程序- ming结合了两种范式的优势：一方面将搜索问题编码为可满足性的逻辑编程，另一方面有效地求解SAT。这两者之间的协同作用暴露了一个编程范式，我们在这里提出的逻辑编程珍珠。为了说明逻辑编程与SAT解决我们给出了一个例子Prolog程序解决部分MAXSAT的实例。
2007-02-13 cs.AI cs.PL
A Complete Calculus for Possibilistic Logic Programming with Fuzzy Propositional Variables
Universitat de Lleida (UdL)（莱里达大学）；CSIC（西班牙国家研究委员会）
本文提出了一种用于可能性不确定性推理和表示模糊知识的命题逻辑程序设计语言。公式由对（A，c）表示，其中A是多值命题，c是单位区间[0，1]中的值，它表示关于A的信念在必要性测度方面的下界。信念状态的所有多值解释的集合上的可能性分布建模。在这个框架中，（i）定义了一般不确定性逻辑的语法和语义，（ii）给出了Horn-规则子语言的一个前件式演算，并证明了它对于确定模糊命题变量从公式集合中导出的最大可能性信念度是完备的;最后，（iii）我们展示了如何计算模糊命题变量之间的部分匹配，在必要性措施的模糊集，可以包括在我们的逻辑编程系统。
2013-01-16 cs.AI
A Probabilistic Approach to Satisfiability of Propositional Logic Formulae
University of New Hampshire（新罕布什尔大学）
我们提出了一个版本的WalkSAT算法，命名为BetaWalkSAT。该方法使用概率推理来偏置局部搜索算法的起始状态。Beta分布用于对文字的布尔值的置信度建模。我们的研究结果表明，提出的BetaWalkSAT算法可以优于其他的不知情的局部搜索方法复杂的布尔可满足性问题。
2019-12-04 cs.AI cs.LO
Sequential decomposition of propositional logic programs
Vienna University of Technology（维也纳工业大学）
本文通过研究程序间在半群理论中著名的Green关系$\mathcal{L,R,J}$，探讨了命题逻辑程序的顺序分解问题，为迈向逻辑程序设计的代数理论迈出了进一步的一步。
2023-09-14 cs.AI cs.LO
diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
National University of Ireland, Galway（爱尔兰国立高威大学）
本文介绍了diff-SAT，一个答案集和SAT求解器，它结合了经常使用概率条款，事实和规则的能力，解决和采样的最佳世界观（满足布尔变量分配或答案集的多集）受用户提供的概率约束。采样过程使用称为可微可满足性求解（$\partial\mathrm{SAT}$）或可微答案集编程（$\partial\mathrm{ASP}$）的基于梯度下降的优化方法来最小化用户定义的可微目标函数。用例是i.a.概率逻辑编程（以概率答案集编程的形式），概率布尔可满足性求解（PSAT）和模型多集（答案集或布尔解释）的分布感知采样。
2021-01-03 cs.AI cs.LO
Exact ASP Counting with Compact Encodings
National University of Singapore（新加坡国立大学）；Indian Institute of Technology Bombay（印度理工学院孟买分校）；University of Toronto（多伦多大学）
针对现有精确ASP计数器难以处理大规模输入、可扩展性差的问题，本文提出sharpASP框架，通过替代答案集定义迁移命题模型计数关键技术，在1470个基准上实现了显著性能提升。
2023-12-19 cs.AI cs.LO
Logic programs with propositional connectives and aggregates
Google Inc（谷歌公司）
答案集编程（ASP）是一种逻辑编程范式，可用于解决复杂的组合搜索问题。聚合是一种ASP构造，在许多应用程序中起着重要作用。定义一个令人满意的语义聚合原来是一个困难的问题，在本文中，我们提出了一个新的方法，基于聚合和命题连接词之间的类比。首先，我们扩展了答案集/稳定模型的定义，以涵盖任意命题理论;然后，我们将聚合定义为原始构造和公式的缩写。我们的集合的定义结合了表达性和简单性，它继承了许多关于嵌套表达式程序的定理，如强等价和分裂定理。
2008-12-08 cs.AI
Differentiable Satisfiability and Differentiable Answer Set Programming for Sampling-Based Multi-Model Optimization
National University of Ireland, Galway（爱尔兰国立高威大学）
本文提出了一种求解多模型优化问题的可微可满足性和可微答案集编程算法（Differentiable Satisfiability and Differentiable Answer Set Programming，简称SAT/ASP）。模型（答案集或满足真值分配）使用一种新的SAT/ASP求解方法，该方法使用基于梯度下降的分支机制进行采样。采样继续进行，直到用户定义的多模型成本函数的值达到给定阈值。作为我们的方法的主要用例，我们提出了分布感知模型采样和表达但可扩展的概率逻辑编程。作为我们的主要算法方法，微分SAT/ASP，我们介绍了一个增强的国家的最先进的CDNL/CDCL算法SAT/ASP解决。此外，我们提出了替代算法，使用未经修改的ASP求解器（Clingo/扣）和映射的优化任务，以传统的答案集优化或使用所谓的传播。我们还报告了开源软件DelSAT，我们的主要算法的最近原型实现，以及初步实验结果，这些结果表明，DelSAT的性能，当应用于概率逻辑推理的用例时，与马尔可夫逻辑网络（MLN）推理性能相当，尽管与MLN相比具有有利的特性，例如表达归纳定义的能力，以及在所有情况下直接将概率作为权重的能力。我们的实验还表明，我们的主要算法是非常优越的性能相比，所提出的替代方法，减少了一个共同的情况下，一般的问题，定期SAT/ASP。
2018-12-31 cs.AI cs.LG cs.LO
Explainability via Short Formulas: the Case of Propositional Logic with Implementation
Tampere University（坦佩雷大学）
我们概念化的逻辑和公式大小的可解释性，给出了一些相关的定义，在一个非常一般的设置的可解释性。我们的主要兴趣是所谓的特殊解释问题，其目的是解释输入模型中输入公式的真值。解释是最小尺寸的公式，其（1）与输入模型上的输入公式一致，并且（2）将所涉及的真值全局地传输到输入公式，即，在每一个模型。作为一个重要的例子，我们研究命题逻辑在这种情况下，并表明，特殊的可解释性问题是完整的第二层次的多项式。我们还提供了一个实现这个问题的答案集编程和调查的能力，解释答案的n-皇后和支配集问题。
2022-10-25 cs.AI cs.LO
Reasoning about Actions with Temporal Answer Sets
Università del Piemonte Orientale（皮埃蒙特东方大学）；Università di Torino（都灵大学）
本文结合回答集编程（ASP）和动态线性时间时态逻辑（DLTL）定义了一种时态逻辑程序设计语言，用于推理复杂动作和无限计算。DLTL扩展了线性时间的命题时态逻辑，使用命题动态逻辑的正则程序来索引时态模态。动作语言允许在域描述中包含一般DLTL公式，以约束可能扩展的空间。我们引入了一个概念的时间回答集域描述，通常的概念的基础上的回答集。此外，我们提供了一个标准的ASP域描述的翻译，我们使用有限的模型检验技术的DLTL约束的验证。
2011-10-17 cs.AI cs.LO
Backdoors to Abduction
Vienna University of Technology（维也纳技术大学）
溯因推理（或简称溯因）是最基本的人工智能推理方法之一，具有广泛的应用，包括故障诊断，信念修正和自动规划。不幸的是，溯因具有很高的计算复杂性，即使是命题溯因也是N_2^P-完全的，因此比NP和coNP更难。这个复杂性障碍排除了命题可满足性（SAT）的多项式变换的存在。在这项工作中，我们使用的溯因实例的结构属性来打破这一复杂性障碍。我们利用小后门集的问题结构。我们提出了固定参数的易于处理的转换，从绑架到SAT，这使得今天的SAT求解器的电源可用于绑架。
2013-04-22 cs.AI cs.CC cs.LO
SMT-based Constraint Answer Set Solver EZSMT+
University of Maryland, College Park（马里兰大学帕克分校）；University of Nebraska at Omaha（内布拉斯加大学奥马哈分校）
约束回答集编程将回答集编程与约束处理相结合。系统EZSMT+是一个约束答案集编程工具，利用可满足性模理论求解器进行搜索。它的理论基础是对Niemela关于逻辑程序的回答集的水平排序的刻画的推广。
2019-06-03 cs.AI cs.LO
Stable Model Counting and Its Application in Probabilistic Logic Programming
National ICT Australia（澳大利亚国家信息与通信技术研究院）；The University of Melbourne（墨尔本大学）
模型计数是计算满足给定命题理论的模型的数量的问题。它最近被应用于解决概率逻辑编程中的推理任务，其目标是计算给定查询为真的概率，提供一组相互独立的随机变量，一个模型（逻辑程序）和一些证据。解决这一推理任务的核心是将逻辑程序转换为命题理论并使用模型计数器。在本文中，我们表明，对于一些问题，涉及归纳的定义，如在图中的可达性，翻译的逻辑程序SAT可以是昂贵的目的，解决推理任务。对于这样的问题，直接实现稳定的模型语义允许更有效的解决。我们提出了两种实现技术，基于无根据集检测，扩展一个命题模型计数器的稳定模型计数器。我们的实验表明，对于特定的问题，我们的方法可以优于一个国家的最先进的概率逻辑编程求解器的几个数量级的运行时间和空间的要求，并可以解决显着更大的规模上，目前的求解器运行的时间或内存的实例。
2014-11-20 cs.AI
DATALOG with constraints - an answer-set programming system
最近出现了一种可行的编程范例，它很好地适应了人工智能、约束满足和组合学中的搜索问题。可以说，命题逻辑是最简单的ASP系统，具有直观的语义，支持问题约束的直接建模。然而，对于某些应用程序，特别是那些需要计算传递闭包的应用程序，它需要额外的变量和大型理论的结果。因此，它可能不是一个实用的计算工具，这样的问题。另一方面，ASP系统基于非单调逻辑，如稳定的逻辑编程，可以有效地处理传递闭包计算，并在一般情况下，产生非常简洁的理论作为问题表示。然而，它们的语义更加复杂。寻找中间地带，本文介绍了一种新的非单调逻辑，DATALOG约束或DC。非正式地，DC理论包括命题子句（约束）和霍恩规则。语义是命题逻辑语义的简单而自然的扩展。然而，由于系统中存在Horn规则，传递闭包的建模变得简单。我们描述了DC的语法和语义，并研究了它的性质。我们讨论了DC的实施和目前的DC的有效性的实验研究结果，比较它与CSAT，可满足性检查和SMODELS实现稳定的逻辑编程。我们的研究结果表明，DC是有竞争力的其他两种方法，在许多搜索问题的情况下，往往会产生更有效的解决方案。
2000-03-24 cs.AI
An Abstract View on Optimizations in Propositional Frameworks
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）
搜索优化问题在科学和工程领域中大量存在。长期以来，人工智能对搜索算法和声明性程序设计语言的发展做出了贡献，这些语言旨在解决和建模搜索优化问题。自动推理和知识表示是人工智能的子领域，特别是在这些发展中。许多流行的自动推理范例为用户提供了支持优化语句的语言：答案集编程或Minone上的MaxSAT，仅举几例。这些范例在它们的语言和它们在计算解决方案上表达质量条件的方式上有很大的不同。在这里，我们提出了一个统一的框架，所谓的重量系统，消除了语法之间的区别范例，并允许我们看到本质的相似性和差异提供的优化语句的范例。这种统一的观点在自动推理和知识表示中的优化和模块化研究中具有显著的简化和解释潜力。它还为研究人员提供了一个方便的工具，用于证明不同框架的形式属性;桥接这些框架;并促进翻译求解器的开发。
2023-03-20 cs.AI
Programming with Personalized PageRank: A Locally Groundable First-Order Probabilistic Logic
Carnegie Mellon University（卡内基梅隆大学）
在许多概率一阶表示系统中，推理是通过“接地”来执行的，即，将其映射到命题表示，然后执行命题推理。有了一个庞大的事实数据库，基础可以非常大，使推理和学习计算昂贵。在这里，我们提出了一个一阶概率语言，这是非常适合近似“本地”接地：每个查询$Q$可以近似接地与一个小图。该语言是随机逻辑程序的扩展，其中推理由个性化PageRank的变体执行。实验表明，该方法在实体解析任务中没有权重学习的情况下表现良好;监督权重学习提高了准确性;接地时间与DB大小无关。我们还表明，数量级的加速是可能的并行学习。
2013-05-10 cs.AI
Decidability and Undecidability Results for Propositional Schemata
CNRS（法国国家科学研究中心）
我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。
2014-01-16 cs.AI cs.LO
Makespan Optimal Solving of Cooperative Path-Finding via Reductions to Propositional Satisfiability
National Institute of Advanced Industrial Science and Technology (AIST)（产业技术综合研究所）；Charles University（查理大学）
研究了协同寻路的最大完工时间最优解问题。CPF中的任务是以非冲突的方式重新定位一组代理，以便每个代理最终从给定的初始位置到达其目标位置。在这项工作中采用的抽象假设，代理人是离散的项目在一个无向图中遍历边缘移动。CPF的Makespan最优解是指生成的解在执行解所需的总时间步数方面尽可能短。我们发现，减少CPF命题可满足性（SAT）是一个可行的选择，获得最大完工时间的最优解。CPF到命题公式的几种编码的建议和实验评估。评估表明，SAT基于CPF求解优于其他最大完工时间优化方法显着在高度约束的情况下（密集占用代理的环境）。
2016-10-18 cs.AI
dcs: An Implementation of DATALOG with Constraints
最近出现了一种可行的编程范例-我们在这里描述了一个ASP系统，DATALOG与约束或DC，基于非单调逻辑。非正式地，DC理论包括命题子句（约束）和霍恩规则。语义是命题逻辑语义的简单而自然的扩展。然而，由于系统中存在Horn规则，传递闭包的建模变得简单。我们描述了DC的语法，使用和实现，并提供实验结果。
2000-03-14 cs.AI
An Application of Proof-Theory in Answer Set Programming
University of Kentucky（肯塔基大学）；University of California（加利福尼亚大学）
我们将证明理论技术应用于答案集编程。主要结果包括：1.逻辑程序中Gelfond-Lifschitz算子连续性的一个刻画2.逻辑程序的稳定模型的一种命题表征（不涉及循环公式）。
2010-01-11 cs.AI
Reasoning about Minimal Belief and Negation as Failure
我们研究MBNF的命题片段中的推理问题，Lifschitz引入的最小信念和否定的逻辑，它可以被认为是几个非单调形式主义的统一框架，包括默认逻辑，自认知逻辑，限定，认知查询和逻辑编程。我们描述的复杂性，并提供算法的命题MBNF推理。特别是，我们表明，蕴涵命题MBNF位于第三级的多项式层次，因此，它比推理在所有上述命题形式主义的非单调推理。我们还证明了MBNF中的否定失败和摩尔的自认知逻辑中的否定内省之间的确切对应关系。
2011-06-01 cs.AI
Logical Boltzmann Machines
University of Tasmania（塔斯马尼亚大学）；City, University of London（伦敦大学城市学院）
在连接主义系统中表示符号知识的想法是一个长期的努力，最近引起了很多关注，其目标是将机器学习和可扩展的声音推理相结合。早期的研究表明，命题逻辑和对称神经网络之间存在对应关系，但对称神经网络不能很好地随变量的数量而扩展，而且其训练机制效率低下。在本文中，我们介绍了逻辑玻尔兹曼机（LBM），神经符号系统，可以表示任何命题逻辑公式的严格析取范式。我们证明了LBM的能量最小化和逻辑可满足性之间的等价性，从而表明LBM是能够合理推理的。我们评估推理经验表明，LBM是能够找到所有令人满意的分配一类逻辑公式的搜索不到0.75%的可能（约10亿）的分配。我们将LBM中的学习与符号归纳逻辑程序设计系统、最先进的神经符号系统和纯粹基于神经网络的系统进行比较，在七个数据集中的五个数据集中实现了更好的学习性能。
2021-12-10 cs.AI cs.LG cs.LO
A Logic for Reasoning about Upper Probabilities
Cornell University（康奈尔大学）
我们提出了一个命题逻辑推理的不确定性事件，其中的不确定性是由一组概率的措施分配一个概率的间隔，每个事件建模。我们给出了该逻辑的一个完备公理化，并证明了可满足性问题是NP-完全的，并不比命题逻辑的可满足性问题难。
2014-08-07 cs.AI cs.LO
Fages' Theorem and Answer Set Programming
我们推广了Francois Fages的一个定理，该定理描述了以否定为失败的逻辑程序的完成语义和答案集语义之间的关系。对这种关系的研究对于答案集编程的出现非常重要。只要这两种语义等价，答案集就可以通过可满足性求解器来计算，而不需要使用诸如models和dlv之类的答案集求解器。作为一个例子，讨论了由于Ilkka Niemperor块世界的逻辑编程表示。
2000-03-09 cs.AI
Reasoning With Qualitative Probabilities Can Be Tractable
University of California, Los Angeles（加利福尼亚大学洛杉矶分校）
我们最近描述了一种形式主义，用于使用“若-则”规则进行推理，这些规则以不同的坚定性水平重新表达[18]。形式主义将这些规则解释为极端条件概率陈述，指定了不可信的数量级，这对世界的可能排名施加了约束。结果表明，一旦我们计算的优先级函数Z+的规则，一个给定的查询被确认或拒绝的程度可以计算在O（log n`）命题可满足性测试，其中n是在知识库中的规则的数量。在本文中，我们证明了计算Z+需要O（n2 X log n）的可满足性测试，而不是在[18]中列出的指数数，这在Horn表达式的情况下降低到多项式复杂度。我们还展示了如何推理与不精确的意见，可以纳入我们的形式主义，以及如何流行的信念修正和认知的战壕概念体现自然和听话。
2013-03-13 cs.AI
A logic for reasoning about upper probabilities
我们提出了一个命题逻辑%，它可以用来推理的不确定性事件，其中的不确定性是由一组概率的措施分配一个区间的概率为每个事件建模。我们给出了该逻辑的一个完备公理化，并证明了可满足性问题是NP-完全的，并不比命题逻辑的可满足性问题难。
2003-07-30 cs.AI cs.LO
Local-search techniques for propositional logic extended with cardinality constraints
我们研究了局部搜索可满足性求解器扩展的基数原子命题逻辑，也就是说，表达式，提供明确的方式来模型的基数集的约束。将基数原子添加到命题逻辑的语言中有助于对搜索问题进行建模，并且通常会导致简洁的编码。我们提出了两个“本地”本地搜索求解器的理论在扩展语言。我们还描述了技术，以减少问题的标准命题可满足性，并允许我们使用现成的SAT求解器。我们对这些方法进行了实验研究。我们的总体发现是，专门为扩展语言设计的本地求解器比依赖于SAT求解器的间接方法执行得更好。
2003-10-31 cs.AI
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
Characterizing and Reasoning about Probabilistic and Non-Probabilistic Expectation
期望是概率论的核心概念。期望的概念也适用于其他不确定性的概念。我们引入了一个命题逻辑推理的期望，语义取决于潜在的表示的不确定性。在基本表示是（a）概率，（b）概率测度集，（c）置信函数和（d）可能性测度的情况下，我们给出了该逻辑的合理而完整的公理化.我们表明，这种逻辑是更有表现力的比相应的逻辑推理的可能性的情况下的概率措施集，但同等表现力的情况下，概率，信念，和可能性。最后，我们证明了这些逻辑的可满足性是NP-完全的，并不比命题逻辑的可满足性难。
2007-04-20 cs.AI cs.LO
On Forgetting in Tractable Propositional Fragments
Guizhou University（贵州大学）
从知识库中提取与字母表子集相关的部分，这被认为是遗忘，已经引起了人工智能社区的广泛兴趣。在标准命题逻辑中，对于可满足性易处理的各种片段，仍然缺乏一种通用的遗忘算法及其面向计算的研究。本文旨在填补这一空白。在讨论了命题逻辑中遗忘的一些基本性质后，给出了CNF片段的基于分解的遗忘算法，并给出了Horn、可重命名Horn、q-Horn、Krom、DNF和CNF片段的遗忘复杂度结果.
2015-02-10 cs.AI
On the use of associative memory in Hopfield networks designed to solve propositional satisfiability problems
Okinawa Institute of Science and Technology Graduate University（冲绳科学技术大学院大学）
该研究探索用于求解命题可满足性问题的Hopfield网络中联想记忆的应用，验证了自优化（SO）模型可求解SAT类组合问题，同时发现其存在关键信息丢失生成伪最优解的副作用，可为难解问题求解研究提供启发。
2024-03-05 cs.AI nlin.AO q-bio.NC
Reasoning about Expectation
Cornell University（康奈尔大学）
期望是概率论的核心概念。期望的概念也适用于其他不确定性的概念。我们引入了一个命题逻辑推理的期望，语义取决于潜在的表示的不确定性。在基本表示是（a）概率，（b）概率测度集，（c）置信函数和（d）可能性测度的情况下，我们给出了该逻辑的合理而完整的公理化.我们表明，这种逻辑是更有表现力的比相应的逻辑推理的可能性的情况下的概率措施集，但同等表现力的情况下，概率，信念，和可能性。最后，我们证明了这些逻辑的可满足性是NP-完全的，并不比命题逻辑的可满足性难。
2014-07-27 cs.AI
On the Tour Towards DPLL(MAPF) and Beyond
Czech Technical University in Prague（布拉格捷克理工大学）
我们讨论了里程碑之旅对DPLL（MAPF），多智能体路径寻找（MAPF）求解器完全集成的戴维斯-普特南-洛格曼-洛夫兰（DPLL）命题可满足性测试算法通过可满足性模理论（SMT）。MAPF的任务是在无向图中以无冲突的方式导航代理，以便每个代理最终到达其唯一的目标顶点。一次最多只能有一个代理驻留在一个顶点中。代理可以通过遍历边来瞬间移动，只要移动不会导致碰撞。最近试图解决MAPF最佳w.r.t.基于MAPF到命题可满足性（SAT）约简的费用和或完工时间已经出现。最成功的方法依赖于通过SMT范例中启发的过程为给定的MAPF实例惰性地构建命题编码。然而，在现有的方法中，SAT求解器和编码的高级构造的可满足性测试的集成相对松散。因此，该方向研究的最终目标是构建DPLL（MAPF）算法，这是一种MAPF求解器，其中编码的构建与底层SAT求解器完全集成。我们讨论了当前最先进的MAPF解决方案和需要做什么步骤，以获得DPLL（MAPF）。DPLL（MAPF）的优点，在其潜在的交替参数化与MAPF $^R$，一个理论的连续MAPF的几何代理，也进行了讨论。
2019-07-11 cs.AI cs.MA
Quantitative Logic Reasoning
University of São Paulo（圣保罗大学）
在本文中，我们展示了同时处理演绎和定量推理的逻辑系统之间的几个相似之处。我们认为把这些系统执行的任务称为定量逻辑推理是合适的。类似的性质保持整个类，其成员存在一套线性代数技术适用于研究可满足性决策问题。在这个演示中，我们认为定量逻辑推理的任务所执行的命题概率逻辑;一阶逻辑计数量词的一个片段包含一元和有限的二元谓词;和命题Lukasiewicz无限值概率逻辑
2019-05-14 cs.AI cs.LO
SAT vs CSP: a commentary
TU Berlin（柏林工业大学）；UNSW Sydney（新南威尔士大学悉尼分校）；Germany and Australia（德国和澳大利亚（注：此处根据上下文理解为作者所属机构所在国家/地区，非独立机构名称，严格按要求仅提取明确机构名，故原文本中该部分不单独作为机构提取））
在2000年，我发表了一个相对全面的研究命题可满足性（SAT）和约束满足问题（CSP）之间的映射[Wal 00]。我分析了四个不同的映射到CSP的SAT问题，和两个CSP到SAT问题。对于每个映射，我比较了在CSP上实现弧一致性与在相应SAT问题上的单元传播的影响，并将这些结果提升到在搜索期间保持（某种程度的）弧一致性的CSP算法，如FC和MAC，以及Davis- Putnam过程（在每个搜索节点执行单元传播）。这些结果有助于深入了解命题可满足性和约束满足之间的关系，为随后的一系列重要而有价值的工作奠定了基础。我在这里讨论是什么促使了这篇论文，以及接下来发生了什么。
2019-09-27 cs.AI
Integer Linear Programming Preprocessing for Maximum Satisfiability
Laboratoire MIS UR 4290 Université de Picardie Jules Verne（MIS实验室 帕莱尔大学）
本文提出将整数线性规划预处理技术整合到MaxSAT求解流程中，从而提升多个顶级MaxSAT求解器的性能，尤其在未加权赛道中表现突出。
2026-01-26 cs.AI
Towards Non-Monotonic Entailment in Propositional Defeasible Standpoint Logic
University of Cape Town and CAIR, South Africa（开普敦大学和CAIR，南非）；Université Sorbonne Paris Nord, Inserm, Sorbonne Université, Limics, 93017 Bobigny, France（巴黎-索邦大学，Inserm，索邦大学，Limics，法国93017博比尼）；ISTI-CNR, Pisa, Italy（意大利比萨ISTI-CNR）
本文通过引入情境立场条件句，将KLM风格的非单调理性蕴涵关系提升到命题可废止立场逻辑（PDSL）的一个片段中，并证明了该片段可表达为一组情境条件句，进而将基于排序的蕴涵关系（如理性和词典序闭包）从命题情况忠实翻译到PDSL，同时保持复杂度界限。
2026-06-02 cs.AI cs.LO
A novel framework for systematic propositional formula simplification based on existential graphs
School of Computer Science, University of St Andrews, Scotland, UK（斯旺西大学计算机科学学院）；Software Competence Centre Hagenberg (SCCH), Austria（海因堡软件能力中心）
本研究基于皮尔士存在图与蕴涵图提出等价保持的命题逻辑化简规则及流程，可推广现有SAT预处理方法，并分析了算法复杂度，还通过n元蕴涵图实现规则扩展。
2024-05-27 cs.AI cs.LO math.LO
SAT as a game
Université de Bourgogne Franche-Comté（勃艮第-弗朗什孔泰大学）
我们提出了一个有趣的SAT表示。虽然主要的兴趣是为了教学目的以一种有趣的方式呈现命题的可满足性，但它也可以激发新的搜索算法。
2015-11-03 cs.AI cs.CC
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
Computing Laboratory（计算实验室）；Oxford University（牛津大学）；School of Computer Science（计算机科学学院）；University of Manchester（曼彻斯特大学）
本文研究了分级模态逻辑在自反性、序列性、对称性、传递性和欧几里得性等不同组合框架类上的可满足性问题，并为其获得了紧致的复杂性界限。
2009-05-19 cs.AI cs.CC cs.LO
A First Polynomial Non-Clausal Class in Many-Valued Logic
Artificial Intelligence Research Institute (IIIA) - CSIC（人工智能研究所 (IIIA) - CSIC）
多项式公式类与演绎效率的相关性激发了他们的搜索，目前，已知有大量这样的类。尽管如此，它们一直专门在小句形式和命题逻辑的设置中寻找，这当然对实际应用有明显的限制。因此，最近提出了第一个非子句（NC）形式的多项式命题类。沿着这些路线，并朝着NC易处理性适用于超越命题逻辑，首先，我们定义了正规多值霍恩非子句类，或RH，通过适当合并两个正规类：霍恩和NC。其次，我们证明了（1）RH与正则Horn类之间的关系是：在句法上RH包含Horn类，但两者在语义上是等价的;（2）RH与正则非小句类之间的关系是：RH包含所有小句形式为Horn的NC公式。第三，我们定义了正则非子句单位归结，或RUR-NC，并证明了它是RH的完全的，并在多项式时间内检查其可满足性。后一个事实表明，由于RH是多值的，非子句的和易处理的，我们的预期目标已经达到。由于RH和RUR-NC都是DPLL方案的基础，在命题逻辑中是最有效的，并且可以扩展到其他一些非经典逻辑，我们认为它们为基于DPLL的高效非子句近似推理铺平了道路。
2021-10-21 cs.AI cs.LO
Satisfiability Modulo Theory Meets Inductive Logic Programming
The University of Edinburgh（爱丁堡大学）
本文提出一种模块化的SMT-ILP架构，结合PyGol与Z3，通过整合可满足性模理论增强归纳逻辑编程在数值约束推理中的能力。
2025-12-15 cs.AI
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
Propositional and Relational Bayesian Networks Associated with Imprecise and Qualitative Probabilistic Assesments
Universidade Estadual de Ponta Grossa（蓬塔格罗萨州立大学）
本文研究了一种表示语言的灵活性启发的概率逻辑和紧凑性启发的关系贝叶斯网络。我们的目标是处理命题和一阶结构与精确，不精确，不确定和定性概率评估。本文展示了如何通过信用网络理论来实现这一点。新的精确和近似推理算法的基础上多线性规划和迭代/循环传播的区间概率，其优越的性能，相比现有的，经验表明。
2012-07-11 cs.AI
Fuzzy Answer Set Computation via Satisfiability Modulo Theories
University of Calabria（卡拉布里亚大学）；Free University of Bozen-Bolzano（博岑-博尔扎诺自由大学）
模糊答案集编程（FASP）结合了两个声明性框架，答案集编程和模糊逻辑，以模型推理默认不精确的信息。几个连接词可用于组合不同的表达式;特别是\Godel和\Luka模糊连接词，由于它们的属性，通常被考虑。虽然\Godel连接可以很容易地从规则头中删除，我们通过复杂性参数表明，这样的简化是不可行的，一般所有其他连接词。%，即使主体仅限于\Luka或\Godel连词。本文分析了一种将FASP程序转换为可满足性模理论（SMT）的方法，SMT由于语义的最小性，一般产生量化的公式。许多FASP程序的结构特性允许消除量化，或合理地减少量化变量的数量。事实上，完整性约束可以取代递归规则通常用来强制布尔解释，和完成子公式可以保证最小的非循环程序与原子头。此外，头循环自由的规则可以取代移位的子程序，其结构取决于消除头连接，使有序完成可以取代最小检查，如果也\Luka析取规则机构是非循环的。本文还介绍了一个原型系统实现这些翻译和评估。出现在逻辑编程理论与实践（TPLP），ICLP 2015会议记录。
2015-07-14 cs.AI
A Scalable Two Stage Approach to Computing Optimal Decision Sets
Monash University（莫纳什大学）；CSIRO Data61（澳大利亚联邦科学与工业研究组织Data61）；ANITI；IRIT（图卢兹计算机科学研究所）；CNRS（法国国家科学研究中心）
机器学习（ML）在现代生活中无处不在。由于它被部署在影响我们隐私和安全的技术中，因此了解其决策背后的推理通常至关重要，从而避免了对可解释的人工智能的需求。基于规则的模型，例如决策树、决策列表和决策集，通常被认为是最可解释的。最近的工作使用命题可满足性（SAT）求解（及其优化变体）来生成最小大小的决策集。由于这些早期方法的实际可扩展性有限，本文提出了一种新的方法来学习最小大小的决策集，通过枚举目标决策集的各个规则彼此独立，然后解决集合覆盖问题来选择规则的子集。该方法利用现代最大可满足性和整数线性规划技术。在广泛的公开数据集上的实验证明了新方法在基于SAT的决策集学习中的优势。
2021-02-03 cs.AI cs.LG cs.LO
Phase Transitions of the Typical Algorithmic Complexity of the Random Satisfiability Problem Studied with Linear Programming
Universität Oldenburg（奥尔登堡大学）
本文研究NP完全$K$ -SAT问题。虽然NP完全问题的最坏情况的复杂性被证明是指数的，但存在参数化的随机问题集合，其中对于适当的参数范围，通常可以在多项式时间内找到解决方案。事实上，对于足够小的$α$值，可以快速求解以$α=M/N $作为控制参数的随机$K$-SAT.它显示了一个相变之间的可满足阶段和不可满足阶段。对于分支定界算法，它在可行的布尔配置的空间中操作，经验上最困难的问题仅位于接近这个相变。在这里，我们研究$K$（$K=3,4$）和相关的优化问题MAX-SAT的线性规划方法，这是广泛用于实际问题，并允许多项式运行时间。与分枝定界法不同，它在可行构形空间之外运行。另一方面，不能保证在多项式时间内找到解决方案。我们研究了几种变体，如包括人工目标函数，所谓的切割平面方法，以及映射到NP完全顶点覆盖问题。我们观察到几个容易的困难的过渡，从那里的问题通常是可解决的（在多项式时间内）使用给定的算法，分别在多项式时间内，他们是不可解决的。对于随机图上的相关顶点覆盖问题，这些易-难转换可以用图的结构性质来识别，如渗透转换。对于目前的随机$K$ -SAT问题，我们已经研究了许多结构特性，也表现出明确的过渡，但他们似乎不相关，在这里观察到的易-难过渡。这使得随机$K$ -SAT的行为比例如顶点覆盖问题
2018-09-18 cond-mat.dis-nn cond-mat.stat-mech cs.AI
