Approximate Counting for Complex-Weighted Boolean Constraint Satisfaction Problems
约束满足问题（或CSP）已经在例如人工智能、数据库理论、图论和统计物理学中被广泛研究。从实用的角度来看，近似求解这些CSP是有益的。当一个人试图近似的总数的真值分配，满足所有布尔值的约束（未加权）布尔CSP，有一个已知的分割定理，所有这样的计数问题整齐地分为三个类别下多项式时间（随机）近似保持减少。与此相反，我们得到了一个二分法定理的近似计数复加权布尔CSP，提供了所有复值一元约束可以自由使用。正是自由一元约束的表达能力使我们能够证明这样一个更强、更完备的分类定理。这一发现使所有计数CSP的近似复杂性分类的追求向前迈进了一步。为了处理复杂的权重，我们采用证明技术的因式分解和arity减少沿线解决Holant问题。此外，我们引入了一个新的概念的T-可构造性，自然会导致近似保持约简。我们的结果也给出了一个近似模拟的二分法定理的复杂性的精确计数复加权布尔CSP。
2012-08-23 cs.CC
Counting Solutions of Constraint Satisfiability Problems:Exact Phase Transitions and Approximate Algorithm
Northeast Normal University（东北师范大学）
NP完全问题相变现象的研究对于理解困难问题的本质具有重要作用。在本文中，我们遵循这条线的研究考虑的问题计数解决方案的约束满足问题（#CSP）。我们考虑随机模型，即RB模型。我们证明了当变量数趋于无穷大时，#CSP的相变确实存在，并且相变发生的临界值是精确的。初步的实验结果也表明，临界点与理论推导相吻合。此外，我们还提出了一个近似算法来估计RB模型的CSP实例的解数的期望值。
2011-02-24 cs.AI cs.CC
An Effective Dichotomy for the Counting Constraint Satisfaction Problem
Bulatov（2008）给出了计数约束满足问题#CSP的二分法。#CSP中的一个问题的特征在于约束语言，它是有限域D上的一个固定的有限关系集。这个问题的一个实例使用这些关系来约束更大集合中的变量。Bulatov证明了从#CSP计算任何问题的实例的满意分配的问题要么是在多项式时间（FP）内，要么是#P-完全的。他的证明在很大程度上利用了泛代数的技术，如果没有对该领域的安全掌握，就无法理解。我们给一个基本的证明布拉托夫的二分法，简洁的表示，我们称之为框架，一类高度结构化的关系，我们称之为强矩形的基础上。我们表明，这些正是根据Mal'tsev多态性是不变的关系。在途中，我们给出了一个简化的决策算法的强矩形约束语言，由于Bulatov和Dalmau（2006）。我们建立了一个新的准则#CSP二分法，我们称之为强平衡，我们证明了这个属性是可判定的。事实上，我们在NP中建立了成员资格。因此，我们证明了二分法是有效的，解决了关于#CSP二分法的最重要的公开问题。
2011-08-17 cs.CC
Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers
该研究证明带计数量词的受护两变量片段的有限可满足性问题属于EXPTIME复杂度类，所用方法还为Kazakov近期提出的该片段可满足性问题属EXPTIME的结论给出了简单证明。
2006-01-26 cs.CC cs.LO
Approximate Model Counting: Is SAT Oracle More Powerful than NP Oracle?
本研究探讨近似模型计数中SAT预言机与NP预言机的相对能力，通过新方法证明SAT预言机并不比NP预言机更强大。
2023-06-17 cs.CC cs.DS cs.IT
Complexity of Counting CSP with Complex Weights
本文对具有复权重的计数约束满足问题（简称#CSP）给出了一个复杂性二分法。为此，我们给出了三个条件，其易处理性。设F是复值函数的有限集合，证明了当满足这三个条件时，#CSP（F）是多项式时间可解的，否则是#P-难的.我们的复杂性二分法推广了计数问题的一系列重要结果：（a）图同态的计数问题是F中存在单个对称二元函数的特殊情况，（b）有向图同态的计数问题是F中存在单个不一定对称二元函数的特殊情况;以及（c）#CSP的标准形式是当F中的所有函数都取{0，1}中的值时。
2011-11-10 cs.CC
Constant Unary Constraints and Symmetric Real-Weighted Counting Constraint Satisfaction Problems
一元约束（在布尔域上）是从{0，1}到实数集的函数。除了输入实例之外，辅助一元约束的自由使用已被证明是有用的，在建立一个完整的分类的近似求解加权计数布尔约束满足问题（或#CSP）的计算复杂性。特别是，两个特殊的常数一元约束是任意约束的arity减少的关键，足以满足所需的分类。在精确计数模型中，两个常数一元约束总是被假设为可用的，因为它们可以使用任意的非空约束集有效地消除。相比之下，我们证明了在近似计数模型，其中至少有一个是有效的近似，从而消除了约由一个非空的约束集。这一事实直接导致一个有效的构造多项式时间随机近似保持图灵约简（或AP约简）从指定约束的#CSP到任何给定的#CSP组成的对称实值约束的任意arities，即使在存在任意额外的一元约束。
2013-10-27 cs.CC
Understanding model counting for $β$-acyclic CNF-formulas
ENS Cachan（卡尚高等师范学校）；Inria（法国国家信息与自动化研究所）；Université Paris Diderot（巴黎狄德罗大学）；Ecole Polytechnique（巴黎综合理工学院）
我们扩展了知识，所谓的结构限制的$\mathrm{\#SAT}$给出了一个多项式时间算法的$β$ -无循环$\mathrm{\#SAT}$。与以前的算法在该地区，我们的算法不进行动态规划，但沿消除顺序，解决了加权版本的约束满足。此外，我们给出的证据表明，这种偏离更标准的算法是不是一个巧合，但有可能没有动态规划算法的通常风格的$β$ -非循环$\mathrm{\#SAT}$。
2014-05-23 cs.AI cs.CC
Hypergraph Acyclicity and Propositional Model Counting
Université Paris Diderot（巴黎狄德罗大学）；ENS Cachan（卡尚高等师范学校）；Ecole Polytechnique（巴黎综合理工学院）
我们发现，命题模型计数问题#SAT的CNF-公式与超图，允许一个不相交的分支分解，可以解决在多项式时间。我们发现，这类超图是无法比拟的超图的有界关联度的宽度是最大的一类超图，其中#SAT是已知的多项式时间可解到目前为止。此外，我们提出了一个多项式时间算法，计算一个给定的超图的不相交分支分解，如果它存在，否则拒绝。最后，我们表明，一些轻微的扩张类的超图与不相交的分支分解导致棘手的#SAT，留下开放如何推广本文的计数结果。
2014-01-24 cs.AI cs.CC
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
The Complexity of Planar Counting Problems
我们证明了与各种可满足性，图形和组合问题，当限制到平面的情况下，计数问题的#P-硬度。这些问题包括\begin{romannum} \item[{}] {\sc 3Sat, 1-3Sat, 1-Ex3Sat, Minimum Vertex Cover, Minimum Dominating Set, Minimum Feedback Vertex Set, X3C, Partition Into Triangles, and Clique Cover.} \end{romannum}我们还证明了{\sf NP}-完备性的{ \sc Ambiguity Satisfiability}问题\cite{Sa80}和{ \sf D $^P$ }-完备性（相对于随机多项式约简）的唯一可满足性问题\cite{VV85}与上述几个问题，当限制到平面的情况。以前，很少{ \sf #P}-硬度的结果，没有{ \sf NP}-硬度的结果，没有{ \sf D $^P$ }-完整性的结果是已知的计数问题，模糊的可满足性问题和唯一的可满足性问题，分别限制到平面的实例。假设{ \sf P $\neq $ NP}，上述结果的一个推论是：对于整数上线性不等式约束的平面线性目标函数的最大化或最小化问题，没有$ε$ -近似算法.
1998-09-11 cs.CC cs.DM
Approximation Complexity of Complex-Weighted Degree-Two Counting Constraint Satisfaction Problems
约束满足问题已经在许多领域中被研究，具有实际意义和理论意义。近年来，在计算约束满足问题（或#CSP）的研究中取得了重大突破。特别是，一个计算复杂性分类的有界度#CSP已被发现的所有程度，除了两个，其中的“度”的输入实例是最大的次数，每个输入变量出现在一组给定的约束。尽管最近的研究的努力，但是，度2 #CSP的复杂性分类已经逃避了我们的理解。本文挑战这个开放的问题，并给出其部分解决方案，采用两种新的证明技术- T_{2} -constructibility和参数化对称化-这是专门设计来处理“任意”的约束下随机近似保持减少。我们将整个约束划分为四个集合，并将所有度为2的#CSP的近似复杂性分类为两类：多项式时间可计算的问题或至少像#SAT一样难的问题。我们的证明利用了复加权度2 #CSP和Holant问题之间的密切关系，这是复加权#CSP的自然推广。
2011-09-27 cs.CC
Counting Small Induced Subgraphs Satisfying Monotone Properties
给定一个图的性质$Φ$，问题$\#\mathsf{IndSub}(Φ)$要求，在输入一个图$G$和一个正整数$k$时，计算$G$中满足$Φ$的大小为$k$的导出子图的数目。对$Φ$上确保$\#\mathsf{IndSub}(Φ)$是硬的明确标准的搜索由Jerrum和Meeks发起[J. COMPUT.系统科学15]并且是对图中的小模式进行计数的主要研究路线的一部分。然而，除了由于Curticapean，Dell和Marx [STOC 17]证明完全分类为“容易”和“困难”属性是可能的以及由于Meeks [Discret. 16]和Dörfler等人。[MFCS 19]，知道的不多。在这项工作中，我们完全回答和明确分类的情况下，单调，即子图封闭，属性：我们表明，对于任何非平凡的单调属性$Φ$，问题$\#\mathsf{IndSub}(Φ)$不能解决的时间$f(k)\cdot |V(G)|^{o(k/ {\log^{1/2}(k)})}$的任何功能$f$，除非指数时间假设失败。通过这一点，我们建立了任何显着的改进，蛮力的方法是不可能的，在语言的参数化的复杂性，我们也得到了$\#\mathsf{W}[1]$ -完整性的结果。
2020-04-14 cs.CC
Picturing Counting Reductions with the ZH-Calculus
本文利用ZH-演算这一图形语言，为#SAT到相关计数问题提供了更简单的图形归约，并证明了Clifford+T片段中ZH-图评估问题属于FP^#P，展示了图形演算在计数问题推理中的直观性和实用性。
2023-08-31 cs.CC
Constraint Satisfaction with Counting Quantifiers 2
我们研究约束满足问题（CSP）的计数量词$\exists^{\geq j}$的存在下，断言存在$j$不同的证人的变量的问题。作为我们之前（CSR 2012）论文的延续，我们关注无向图模板的复杂性。作为我们的主要贡献，我们解决了（CSR 2012）中提出的两个主要开放问题。首先，我们通过证明计数量词和团大小的所有可能组合的完全可分性来完成团模板的分类，将每种情况放置在P，NP-完全或Pspace-完全中。这涉及到在团$K_{2j}$上有单个量词$\exists^{\geq j}$的情况的解决。其次，我们证实了（CSR 2012）的一个猜想，该猜想提出了所有有限无向图上的$\exists$和$\exists^{\geq 2}$的完全二分法。这第二个结果的主要推力是解决的复杂性，我们证明是一个多项式时间可解的问题的无限路径。通过将算法应用于无限路径，我们就能够解决有限路径的问题，然后是树木和森林。因此，作为这项工作的推论，结合（CSR 2012）中的其他情况，我们得到了有限图上$\exists$和$\exists^{\geq 2}$量词的完全二分法，每个这样的问题要么是P困难的，要么是NP困难的。最后，我们坚持（CSR 2012）的工作，探索在P和P空间完全之间存在二分法的情况，与可能出现中间NP完全性的情况形成对比。
2013-12-30 cs.CC cs.DM cs.LO
Tensor Network Rewriting Strategies for Satisfiability and Counting
我们平等地提供了SAT和#SAT的图形处理。#SAT的网络可以以标准的方式表示为张量网络。这些张量网络可以用ZH演算的图来解释：这是一个用简单生成器构建的图来推理C上张量的系统，其中计算可以单独通过图的变换来进行。一般来说，ZH图的节点接受C上的参数，这些参数决定了张量系数;对于#SAT实例的标准表示，系数取值为0或1。然后，通过选择一个图的系数在B上的范围，我们表示SAT的相应实例。因此，通过在布尔半环或复数上解释图，我们实例化了问题的决策或计数版本。我们发现，对于类已知是在P，如2SAT和#XORSAT，存在适当的重写规则允许有效的简化图，产生解决方案在多项式时间。相比之下，对于已知为NP完全的类，例如3SAT，或#P完全的类，例如#2SAT，相应的重写规则在图中引入超边，其数量不容易由多项式限制。这种图解方法统一了CSP和#CSP的复杂性诊断，并显示出有助于基于张量网络收缩的算法的希望。
2021-09-06 cs.CC quant-ph
Counting Answer Sets via Dynamic Programming
TU Wien（维也纳工业大学）
虽然近年来命题可满足性（#SAT）的解决方案计数问题重新受到关注，但这一研究趋势并没有影响其他AI解决范式，如答案集编程（ASP）。虽然ASP求解器被设计为枚举所有解决方案，因此计数可以很容易地完成，但所有解决方案的具体化是ASP（#ASP）计数问题的明显瓶颈。在本文中，我们提出了基于动态规划的#ASP算法，利用底层（地面）ASP程序的结构。一个原型实现的实验结果表明，与现有的求解器相比，承诺。
2016-12-22 cs.AI cs.CC cs.LO
The complexity of approximating conservative counting CSPs
研究了近似求解加权计数约束满足问题CSP（F）的复杂性.在保守的情况下，其中F包含所有一元函数，有一个分类已知的情况下，在F中的功能域是布尔的。本文对F中函数具有任意有限区域的更一般问题给出了一个分类。我们定义了弱对数-模和弱对数-超模的概念。证明了若F是弱对数模，则#CSP（F）在FP中.否则，它至少和#BIS一样难以近似，即在二分图中计数独立集的问题。#BIS对于逻辑定义的复杂度类#RHPi1的近似保持约简是完备的，并且被认为是难以处理的。我们进一步细分了#BIS-硬案例。如果F是弱对数超模的，那么我们证明了#CSP（F）和（布尔）对数超模加权#CSP一样简单。否则，我们证明它是NP-难近似。最后，我们给出了arity-2情况下的完全可分性，其中#CSP（F）在FP中，或者是#BIS等价的，或者在难度上等价于#SAT，即近似计数合取范式中布尔公式的满足赋值的问题。我们还讨论了我们的分类算法方面。
2014-05-29 cs.CC
Model Counting for Dependency Quantified Boolean Formulas
National Taiwan University（台湾大学）；University of Liverpool（利物浦大学）
本文研究依赖量化布尔公式（DQBF）的模型计数问题，证明#2-DQBF是#EXP完全的，并开发专用2-DQBF模型计数器，实验显示其在大依赖集场景下扩展性优于基线方法。
2025-11-15 cs.CC cs.LO
Fine-grained reductions from approximate counting to decision
在本文中，我们介绍了一个一般框架细粒度约简近似计数问题的决策版本。(Thus我们使用一个决定是否存在任何见证人的预言机，以最小的开销乘性地近似见证人的数量。这反映了Sipser（STOC 1983）和Stockmeyer（SICOMP 1985）在多项式时间设置下的基本结果，以及Müller（IWPEC 2006）在FPT设置下的类似结果。使用我们的框架，我们获得了一些最重要的细粒度复杂性问题的减少：正交向量问题，3SUM，和负权重三角形问题（这是密切相关的所有对最短路径）。我们还提供了从近似#SAT到SAT的细粒度减少。假设强指数时间假设（SETH）为假，则对于某些$1<c<2$和所有$k$，存在用于k-SAT的$O(c^n)$时间算法。然后证明了对于所有的$k$，存在一个近似于# $k$ -SAT的$O((c+o(1))^n)$ -时间算法.特别是，我们的结果意味着指数时间假设（ETH）等价于一个非常弱的陈述，即没有算法可以在时间上将#3-SAT近似到$1+ε$的因子$2^{o(n)}/ε^2$（将$ε> 0$作为输入的一部分）。
2020-11-23 cs.CC cs.DS
Complexity Classification of Complex-Weighted Counting Acyclic Constraint Satisfaction Problems
本文针对复值无环计数约束满足问题，依据是否允许自由使用XOR约束，分别给出二分与三分复杂度分类，并引入AT-可构造性工具分析复杂度上界。
2024-03-14 cs.CC cs.FL cs.SC
