Weaker consistency notions for all the CSPs of bounded width
Feder和Vardi [SICOMP'98]提出的所有有界宽度的约束满足问题的特征在[Bulatov'09]中得到了确认，并在[FOCS'09，JACM'14]中独立得到了确认。这两个证明都是基于（2，3）-一致性（在[FOCS'09]中使用布拉格一致性，直接在[Bulatov'09]中），这是昂贵的验证。我们引入了一个新的一致性概念，单点线性弧一致性（SLAC），并表明，它解决了相同的家庭的问题。SLAC弱于Singleton弧一致性（SAC），因此结果回答了[JLC'13]中的问题，表明SAC解决了所有有界宽度的问题。与此同时，验证弱一致性（甚至SAC）的问题比验证（2，3）-一致性的问题具有显著的计算优势，从而改进了求解有界宽度CSP的算法。
2016-07-13 cs.CC cs.LO
No-Rainbow Problem and the Surjective Constraint Satisfaction Problem
满射约束满足问题（Surjective Constraint Satisfaction Problem，SCSP）是判定一组变量在给定的约束条件下是否存在满射赋值的问题，其中满射赋值是包含定义域中所有元素的赋值。在本文中，我们证明了最著名的SCSP，称为无彩虹问题，是NP-难的。此外，我们反驳的猜想说，SCSP约束语言$Γ$和CSP相同的语言常数具有相同的计算复杂性多时间减少。我们的反例还表明，SCSP的复杂性不能描述的约束语言的多态性。
2021-04-29 cs.CC cs.LO math.RA
Arc Consistency and Friends
限制约束满足问题的一种自然且既定的方法是修复可用于构成约束的关系;这样的关系族称为约束语言。在这篇文章中，我们研究了弧一致性，一个大量研究的推理方法，并从约束语言的角度对其进行了三个扩展。我们进行了比较的基础上，他们解决的约束语言的研究方法，我们提出了新的多项式时间的易处理性结果单弧一致性，最强大的方法研究。
2011-04-26 cs.AI cs.CC cs.LO
Local Consistency and SAT-Solvers
University of Oxford（牛津大学）
局部一致性技术，如k-一致性是约束满足问题的专用求解器的关键组成部分。在本文中，我们表明，使用k-一致性技术的权力，约束满足问题，正是通过使用一个特定的推理规则，我们称之为负超分辨率，标准的直接编码的问题，布尔子句。我们还表明，目前的子句学习SAT求解器将发现在预期的多项式时间的任何不一致，可以推断出从一组给定的子句使用负超解式的固定大小。我们结合这两个结果表明，没有明确设计这样做，目前的子句学习SAT求解器有效地模拟k-一致性技术，为所有固定值的k。然后，我们给出了一些实验结果表明，这个功能允许子句学习SAT求解器有效地解决某些家庭的约束问题，这是传统的约束编程求解器的挑战。
2014-01-18 cs.AI cs.LO
Symmetric Linear Arc Monadic Datalog and Gadget Reductions
Institut für Algebra（代数研究所）；TU Dresden（德累斯顿工业大学）
本文研究了对称线性弧单子Datalog，通过小工具缩减和同态对偶性，确定了有限域约束满足问题的可解性条件。
2025-01-08 cs.CC cs.LO math.RA
A finer reduction of constraint problems to digraphs
一般的关系结构A上的约束满足问题等价于某个关联有向图上的约束满足问题是多项式时间的。我们提出了一个变体的这种结构，并表明相应的约束满足问题是对数空间等价于在A。此外，我们发现，几乎所有的常见的多态性的性质都等价地举行的A和构造的有向图。因此，代数CSP二分法猜想以及刻画CSP在对数空间和非确定性对数空间中可解的定理等价于它们对有向图的限制。
2015-12-28 cs.CC cs.LO math.CO
Quantum Polymorphisms and the Complexity of Quantum Constraint Satisfaction
TU Graz（格拉茨工业大学）；Hamburg University of Technology（汉堡工业大学）
本文引入量子多形性概念，构建量子CSP间的代数框架，并建立量子多形性minion与量子关系构造之间的Galois联系。通过利用量子多形性的上下文性，完全刻画了关系结构中交换器的存在性，证明了奇环参数化的量子CSP和Siggers子句的量子可满足性问题为不可判定。
2026-04-01 cs.CC cs.LO math.CO
Constraint Satisfaction Problems over Finitely Bounded Homogeneous Structures: a Dichotomy between FO and L-hard
Faculty of Mathematics and Computer Science, Jagiellonian University（雅盖隆大学数学与计算机科学学院）
本文证明了有限有界同构模型完全核心的第一阶扩展的CSP要么可由一阶定义（非均匀AC$^0$），要么在第一阶约简下为L难。该结果是Bodirsky-Pinsker猜想范围内最一般的复杂性二元性。
2026-07-16 cs.CC cs.LO
An Algebraic Hardness Criterion for Surjective Constraint Satisfaction
Universidad del País Vasco（巴斯克大学）；IKERBASQUE, Basque Foundation for Science（伊克尔巴斯克，巴斯克科学基金会）
关系结构B上的约束满足问题（constraint satisfaction problem，CSP）是在给定关系B的变量上的一组约束条件的情况下，判定是否存在满足所有约束条件的变量的赋值;满射CSP是判定是否存在满足对B的论域的满射赋值的变体。我们提出了一个代数条件B的多态克隆，并证明了它是足够的有限结构B上的满射CSP的硬度，在这个意义上说，这个问题承认从一定的固定结构CSP减少。据我们所知，这是第一个结果，允许使用代数信息从一个关系结构B推断信息的复杂性硬度满射约束满足的B。我们的结果的一个推论是，在任何有限的非平凡结构，只有本质上一元多态性，满射约束满足是NP-完全的。
2014-06-02 cs.AI cs.CC cs.LO
Topology is irrelevant (in a dichotomy conjecture for infinite domain constraint satisfaction problems)
有限域约束满足问题（CSP）的易处理性猜想指出，只要在某种精确的技术意义上，3-SAT问题没有自然约简，这样的CSP在多项式时间内是可解的;否则，它们是NP完全的。它最近的决议借鉴了代数特征的限制边界：CSP的有限结构不允许自然减少从3-SAT当且仅当稳定剂的多态克隆的核心结构满足一些非平凡系统的身份，这种满足总是见证了几个特定的非平凡系统的身份不依赖于结构。上述公式中的易处理性猜想被推广到一类无限域CSP，即有界齐次结构约简的CSP。后来证明，硬度和易加工性之间的界限，即，一个自然减少从3-SAT，可以为这一类的特点是结合了代数和拓扑性质。然而，它是不知道的拓扑组件是否是必不可少的，在这个特性。我们提供了一个否定的答案，这个问题的证明，边界线的特点是由一个特定的代数身份，即伪Siggers身份$αs(x,y,x,z,y,z) \approx βs(y,x,z,x,z,y)$。这就完成了将无限域CSP二分法猜想降为有限情形的策略的一个步骤。我们的主要定理也是独立的数学兴趣，表征拓扑性质的任何$ω$ -范畴的核心结构（存在一个连续的同态的稳定剂的多态克隆的预测）在纯代数方面（失败的身份如上所述）。
2021-01-11 cs.LO
Finite Domain Bounds Consistency Revisited
一种广泛采用的解决约束满足问题的方法将系统树搜索与约束传播相结合，以修剪搜索空间。约束传播由实现某种一致性概念的传播器执行。边界一致性是为算术约束和有限整数域中的几个全局约束构建传播子的首选方法。然而，在边界一致性的定义上存在一些混乱。在本文中，我们澄清了三个常用的界限一致性概念之间的差异和相似之处。
2004-12-06 cs.AI cs.LO
Eidoku: A Neuro-Symbolic Verification Gate for LLM Reasoning via Structural Constraint Satisfaction
Independent Researcher（独立研究者）
Eidoku通过结构约束满足方法有效检测LLM推理中的结构不一致幻觉，提供神经符号验证机制。
2025-12-19 cs.AI cs.LO
Sensitive instances of the Constraint Satisfaction Problem
我们调查的影响修改的约束关系的约束满足问题（CSP）的实例，与一个固定的模板，对一组解决方案的实例。更确切地说，我们调查敏感的实例：CSP的实例被称为敏感的，如果从任何约束关系中删除任何元组使实例的某些解决方案无效。等价地，可以要求来自其任何一个约束的每个元组扩展到实例的解。显然，任何非平凡模板都有不敏感的实例。因此，我们遵循Feder和Vardi（SICOMP 1999）提出的方向（在严格宽度的上下文中），并要求只有本地一致性检查算法产生的实例是敏感的。在语言的代数方法的CSP，我们表明，一个有限的幂等代数$\mathbf{A}$有一个$k+2$变量附近的一致性项操作，当且仅当任何实例，从运行的$(k, k+1)$一致性算法的实例上$\mathbf{A}^2$是敏感的。我们的结果的一个版本，没有幂等性，但在各种代数的敏感性条件成立，解决了G。伯格曼关于代数的投影系统，这些投影系统产生于代数的有限积的某个子代数。我们的结果适用于无限（虽然在$\mathbf{A}$幂等的情况下）代数，以及表现出惊人的相似性，严格的宽度$k$条件提出的Feder和Vardi。这两种条件的特征都可以是存在近乎一致的操作，但操作的特性相差1。
2020-05-01 cs.LO math.LO
Strong subalgebras and the Constraint Satisfaction Problem
在2007年，它被证明，约束满足问题（CSP）的约束语言$Γ$是易处理的，当且仅当$Γ$是由一个弱近似（WNU）操作保持。经过多次努力和部分结果，该猜想于2017年由Andrei Bulatov和作者独立证明。在本文中，我们认为我的证明，即强子代数，使我们能够减少域的变量迭代的两个主要成分之一。为了解释这个想法是如何工作的，我们展示了强子代数的代数性质，并提供了关于CSP复杂性的两个重要事实的自包含证明。首先，我们证明，如果一个约束语言不被保存的WNU操作，那么相应的CSP是NP-难的。其次，我们描述了所有的约束语言，可以解决局部一致性检查。此外，我们刻画了所有幂等代数没有一个WNU项的具体arity $n$，没有一个WNU项，有WNU项的所有arity大于2。本文中提出的大多数结果都不是新的，但我相信本文可以帮助理解我对CSP的方法，并且对已知事实的新的自包含证明也将是有用的。
2020-05-01 cs.CC cs.LO math.LO
k-Hyperarc Consistency for Soft Constraints over Divisible Residuated Lattices
我们研究了可分剩余格（DRL）作为软约束满足问题（软CSP）的一般评价框架的适用性。DRL实际上是这个角色的自然候选者，因为它们形成了一个大家族的子结构和模糊逻辑的代数语义。我们提出以下结果。(i)我们表明，DRL subterranial重要的软约束，如交换幂等半环和公平的估值结构的估值结构，在这个意义上说，最后两个是成员的某些子品种的DRL（即，Heyting代数和BL-代数分别）。(ii)在J. Larrosa和T. Schiex [2004]和S. Bistarelli和F. Gadducci [2006]描述了一种多项式时间算法，该算法在DRL上评估的软CSP上强制执行k-超弧一致性。观察到，在一般情况下，DRL既不是幂等的，也不是完全有序的，该算法的可用算法，强制执行k-超弧一致性的推广。
2008-05-22 cs.LO
Combinatorial Gap Theorem and Reductions between Promise CSPs
CSP实例的值通常被定义为可以同时满足的约束的一部分。我们提出了另一种定义的一个实例的值，并表明，纯粹的组合的原因，一个不可解的实例的值是有界远离一个，我们称之为这一事实的间隙定理。我们发现，间隙定理意味着NP-硬度的间隙版本的分层标签覆盖问题。从PCP定理可以得到同样的结果，但是我们的简化的完整的、自包含的证明是相当短的，并且结果仍然可以为许多问题提供无PCP的NP-困难证明。我们的推理的简单性也表明，较弱版本的独特游戏类型的结构，例如，d到1猜想，可能是可访问的，并作为一个中间步骤，证明这些猜想在他们的全部力量。作为第二个主要应用，我们给出了一个充分条件，在此条件下，一个固定模板的承诺约束满足问题（PCSP）减少到另一个PCSP。归约的正确性取决于间隙定理，但归约本身非常简单。因此，我们得到每个CSP可以规范地减少到大多数已知的NP-困难的PCSP，如近似超图着色问题。
2021-07-20 cs.CC cs.LO
A categorical perspective on constraint satisfaction: The wonderland of adjunctions
Charles University, Prague, Czech Republic（布拉格查理大学）；Czech Technical University, Prague, Czech Republic（捷克理工大学）；University of Birmingham, Birmingham, UK（伯明翰大学）
本文从范畴论角度探讨约束满足问题及Promise约束满足问题的复杂性，通过范畴论方法重新证明核心结果，展现更简洁且广泛适用的证明方式，为研究提供新视角。
2026-05-14 cs.LO math.CT
Notes on CSPs and Polymorphisms
本文是多年学习研讨会的笔记，系统总结了CSP代数方法中的少子幂理论、吸收子代数及其在局部一致性求解中的应用，并介绍了保守CSP模板的二分类定理。
2025-05-26 cs.CC cs.DM cs.LO
Super-linear Lower Bounds for CSP Non-Redundancy via Shrinking Instances
University of California, Berkeley（加州大学伯克利分校）；Eindhoven University of Technology（埃因霍温理工大学）；Linköping University（林雪平大学）；Royal Holloway, University of London（伦敦大学皇家霍洛威学院）
本文通过超图投影框架重新审视CSP非冗余性相关的gadget减少方法，从而更精确地预测哪些gadget减少可以产生超线性非冗余性下界，并展示了如何利用SAT求解器自动推导gadget减少，为发现更多CSP非冗余性关系开辟了新的计算途径。
2026-09-22 cs.DM cs.LO math.CO
A CHR-based Implementation of Known Arc-Consistency
在经典的CLP（FD）系统中，变量的域在约束传播过程的开始是完全已知的。然而，在与外部环境交互的系统中，在约束传播开始之前获取变量的整个域可能导致计算时间的浪费，或者甚至导致所获取的数据在使用时过时。对于这样的情况，交互式约束满足问题（ICSP）模型已经被提出作为CSP模型的扩展，以使得即使在域不完全已知时也可以开始约束传播，仅在必要时执行域元素的获取，并且不需要在每次获取之后重新开始传播。在本文中，我们将展示如何求解器的两个排序CLP语言，在以前的工作中定义，表达ICSP，已实施的约束处理规则（约束处理规则）语言，声明性语言特别适合于高层次的约束求解器的实现。
2004-08-24 cs.AI cs.LO
Toward a Uniform Algorithm and Uniform Reduction for Constraint Problems
本文提出统一框架，通过多valued minion描述约束问题的求解能力，引入新的SDP-like向量放松方法，证明其等价于AIP-Z_p放松的第k级，并解决二面体群D4的CSP问题。
2026-04-07 cs.CC cs.DS cs.LO
SDPs and Robust Satisfiability of Promise CSP
本研究首次探索Promise CSP的鲁棒满足算法，提出基于多数/交替阈值多态性的鲁棒SDP舍入算法，证明缺少该多态性的对称布尔谓词对PCSP困难，并给出相关PCSP的代数刻画猜想。
2025-09-08 cs.DM cs.DS cs.LO
Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard
University of Potsdam（波茨坦大学）；TU Wien（维也纳工业大学）
标准答案集程序（ASP）的一致性判定是NP-完全的，与经典命题逻辑（SAT）的满意度问题一样困难。解决这些问题的最佳算法在最坏的情况下需要指数时间。指数时间假设（ETH）意味着这个结果对于SAT是紧的，也就是说，SAT不能在亚指数时间内求解。这立即确定了结果对于ASP的一致性问题也是紧的。然而，考虑到问题的树宽，ASP的一致性问题比SAT稍微困难一些：虽然SAT可以通过在树宽k中以指数时间运行的算法来解决，但最近表明ASP需要在k \cdot log（k）中以指数时间运行。这个额外的成本是由于检查程序中的正循环导致没有自支持的真实原子。本文改进了上述结果，并证明了ASP的一致性问题可以在k \cdot log（λ）中指数时间内得到解决，其中λ是程序正依赖图中树宽与最大强连通分量的最小值.我们提供了一个动态规划算法，解决了这个问题，并坚持上述限制的树宽意识减少从ASP到SAT。
2020-07-09 cs.AI cs.CC cs.LO
The complexity of general-valued CSPs seen from the other side
约束满足问题（CSP）是关于两个结构之间的同态。对于具有限制性左手边结构的CSP，Dalmau，Kolaitis和Vardi [CP'02]，Grohe [FOCS'03/JACM'07]，Atserias，Bulatov和Dalmau [ICALP'07]的结果建立了多项式时间可解性（受复杂性理论假设）和有界一致性算法可解性（无条件）的精确边界作为有界树宽模同态等价。一般值约束满足问题（VCSP）是两个值结构之间同态的CSP的推广。对于VCSPs与限制的左手边值结构，我们建立了精确的边界多项式时间的可解性（受复杂性理论的假设）和可解性的$k$ -级的Sherali-Adams LP层次（无条件）。我们还获得了结果，有关问题的解决方案和认识到听话的情况下，后者在数据库理论中的应用。
2021-10-03 cs.CC cs.DM cs.DS
A Machine-checked Proof of Consistency for Impredicative Pure Type Systems
Universidad ORT Uruguay（乌拉圭ORT大学）
研究非直谓纯类型系统的一致性，通过使用经典语法和多重替换，给出β归约合流性、主体归约及一致性证明，发展α交换关系理论，用Agda机器检查，取得类型理论机械化方法的进展。
2026-07-23 cs.LO
Bounded Synthesis of Reactive Programs
大多数反应系统的综合算法都集中在有限状态机的构造上，而不是实际的程序。这通常会导致结构不良、不可读的代码。在本文中，我们提出了一个有界的合成方法，自动构造，从一个给定的规范在线性时间时序逻辑（LTL），一个程序在Madhusudan的简单的命令式语言的反应程序。我们开发和比较两个主要的方法减少的综合问题的布尔约束满足问题。第一个约简是基于有界合成到双向交替自动机的推广，第二个约简是基于约束系统中程序语法的直接编码。我们报告的初步经验与原型实现，这表明直接编码优于自动机的方法。
2018-07-24 cs.FL cs.LO
Generalizing Consistency and other Constraint Properties to Quantified Constraints
Microsoft Research Ltd（微软研究院）；Università di Roma La Sapienza（罗马第一大学）
量化约束和量化布尔公式通常比经典约束更难推理，因为量词交替使得通常的解概念不合适。因此，约束满足问题（CSP）的基本属性，如一致性或可替代性，在量化的情况下，不完全理解。这些属性很重要，因为它们是大多数用于解决经典（存在量化）约束的推理方法的基础，并且人们希望在量化约束的解决中受益于类似的推理方法。在本文中，我们表明，大多数的CSP求解器使用的属性可以推广到量化CSP。这需要重新思考一些基本概念，特别是，我们提出了一个概念的结果，概括了经典的解决方案的概念，所有的定义都是基于。我们提出了一个系统的研究这些属性之间的关系，以及复杂性的结果，这些属性的决定。最后，由于这些问题通常是棘手的，我们推广了CSP中使用的方法，并提出了较弱的，更容易检查的概念的基础上的局部性，允许检测这些属性不完全，但在多项式时间。
2007-05-24 cs.AI cs.LO
On the speed of constraint propagation and the time complexity of arc consistency testing
RWTH Aachen University（亚琛工业大学）；Humboldt-Universität zu Berlin（柏林洪堡大学）；Institute for Applied Problems of Mechanics and Mathematics（力学与数学应用问题研究所）
在两个关系结构上建立弧一致性是求解约束满足问题最常用的算法之一。我们的目标是确定弧一致性测试的时间复杂度。输入结构$G$和$H$可以被假设为连通着色图，因为一般问题简化为这种特定情况。我们首先观察上界$O(e(G)v(H)+v(G)e(H))$，这意味着边界$O(e(G)e(H))$的边数和边界$O((v(G)+v(H))^3)$的顶点数。然后，我们表明，这两个界限是紧到一个常数因子，只要弧的一致性算法是基于约束传播（像任何算法目前已知的）。我们对下界的论证是基于慢约束传播的例子。我们测量的速度约束传播上观察到的一对$G,H$的大小证明，在一个自然的组合证明系统，剧透赢得存在的2卵石游戏$G,H$。证明的大小由游戏长度$D(G,H)$从下而上限定，我们分析的一个关键要素是$G,H$与$D(G,H)=Ω(v(G)v(H))$的存在性。我们发现一个这样的例子在旧的基准实例的弧一致性问题，也提出了一个新的，不同的建设。
2013-03-28 cs.AI cs.LO
Constraint Reductions
CNRS-Université Paris Diderot（法国国家科学研究中心-巴黎第七大学）
这是对CP 2003论文“布尔基数约束的高效cnf编码”的评论。在回顾其背景下，我们概述了一个分类的约束就其演绎能力一般弧一致性（GAC）。
2020-06-03 cs.AI cs.LO
Checking Robustness Between Weak Transactional Consistency Models
对数据库的并发访问通常封装在事务中，以便能够与其他并发计算隔离并对故障具有弹性。现代数据库为事务提供了各种语义，对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供更好的性能，因此一个重要的问题是调查给定程序所需的最弱一致性级别（以满足其规范）。作为处理这个问题的一种方式，我们调查的问题，检查是否一个给定的程序具有相同的一组行为时，更换一个较弱的一致性模型。这种被称为鲁棒性的特性通常意味着在削弱一致性时保留程序的任何规范。我们专注于一致性模型的鲁棒性问题，这是弱于标准的串行化，即因果一致性，前缀一致性，快照隔离。我们发现，检查这些模型之间的鲁棒性是多项式时间减少到一个状态可达性问题下的串行化。我们使用这种减少也得到一个务实的证明技术的基础上，利普顿的减少理论，允许证明程序的鲁棒性。我们已经将我们的技术应用于几个具有挑战性的应用程序，从分布式系统和数据库的文献。
2021-01-22 cs.LO cs.PL
Three Fundamental Questions in Modern Infinite-Domain Constraint Satisfaction
TU Wien（维也纳工业大学）；Institut für Diskrete Mathematik und Geometrie, FB Algebra, TU Wien（维也纳工业大学离散数学与几何研究所代数系）；TU Dresden（德累斯顿工业大学）；Institut für Algebra, TU Dresden（德累斯顿工业大学代数研究所）
本文围绕无限域CSP的Bodirsky-Pinsker猜想提出三个基本问题并给出肯定答案，从结构与代数角度简化猜想适用范围，建立其与有限域PCSP的强关联，并通过系统发育CSP案例验证相关结论。
2026-05-06 cs.LO math.LO
Positivity-hardness results on Markov decision processes
本文通过从线性递推序列 Positivity 问题的多项式时间归约，证明单计数器 MDPs 和整数权重 MDPs 上的一系列优化问题在数学上本质困难，其算法求解需解析数论的重大突破。
2024-04-05 cs.LO
Subsumption Algorithms for Three-Valued Geometric Resolution
本文针对三值几何归结中的子sumption测试难题，将其转化为广义约束满足问题，提出直接算法和两种SAT转化，并利用局部一致性过滤及最小子集求解，提升效率且可独立应用于约束求解。
2018-12-10 cs.LO
