首页/论文/2012.14366

arXiv 2012.143662020-12-28cs.AIcs.SE

计算约束的解的个数

Counting the Number of Solutions to Constraints

Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Johannes Kepler University Linz（林茨约翰内斯·开普勒大学）

Jian Zhang, Cunjing Ge, Feifei Ma

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

与约束满足问题相比，计数问题受到的关注较少。本文综述了约束问题解的个数计算问题的研究工作。约束可以采取各种形式，包括命题逻辑中的公式、实数或整数上的线性不等式、线性约束的布尔组合。我们描述了一些解决计数问题的技术和工具，以及一些应用（例如，自动推理、程序分析、形式化验证和信息安全的应用）。

英文摘要：

Compared with constraint satisfaction problems, counting problems have received less attention. In this paper, we survey research works on the problems of counting the number of solutions to constraints. The constraints may take various forms, including, formulas in the propositional logic, linear inequalities over the reals or integers, Boolean combination of linear constraints. We describe some techniques and tools for solving the counting problems, as well as some applications (e.g., applications to automated reasoning, program analysis, formal verification and information security).

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

基于计数的搜索：约束满足问题的分支启发式算法

Counting-Based Search: Branching Heuristics for Constraint Satisfaction Problems

Dynadec Europe

设计一种跨问题域可靠的约束规划启发式搜索算法是近年来的一个重要研究课题。本文主要研究一类候选算法：基于计数的搜索。这样的算法试图做出分支决策，通过确定每个单独约束的解决方案与该决策一致的比例来保留大多数解决方案。而大多数通用搜索算法在约束编程依赖于本地信息的水平上的个别变量，我们的搜索算法是基于更多的全球信息的约束水平。我们设计了几个算法，用于计算特定家庭的约束的解决方案的数量，并提出了一些搜索算法利用这些信息。本文的实验部分考虑了八个问题域，从完善的基准难题到排班和运动调度。初步的实证分析确定启发式maxSD作为一个强大的候选人，我们的建议。然后，我们评估后者对最先进的，包括最新的通用搜索算法，重新启动，和基于差异的树遍历。实验结果表明，基于计数的搜索一般优于其他通用算法。

2014-01-18cs.AI

带有简化技术的针对整数线性约束模型计数的穷举DPLL方法

An Exhaustive DPLL Approach to Model Counting over Integer Linear Constraints with Simplification Techniques

本文提出一种基于穷举DPLL架构并集成混合整数规划简化技术的整数线性约束模型计数精确方法，实验证明其在随机和应用基准上均显著优于现有最先进方法。

2025-09-17cs.AI

约束可满足性问题解的计数：精确相变与近似算法

Counting Solutions of Constraint Satisfiability Problems:Exact Phase Transitions and Approximate Algorithm

Northeast Normal University（东北师范大学）

NP完全问题相变现象的研究对于理解困难问题的本质具有重要作用。在本文中，我们遵循这条线的研究考虑的问题计数解决方案的约束满足问题（#CSP）。我们考虑随机模型，即RB模型。我们证明了当变量数趋于无穷大时，#CSP的相变确实存在，并且相变发生的临界值是精确的。初步的实验结果也表明，临界点与理论推导相吻合。此外，我们还提出了一个近似算法来估计RB模型的CSP实例的解数的期望值。

2011-02-24cs.AIcs.CC

使用加权一阶模型计数解决组合计数问题

Solving Combinatorial Counting Problems with Weighted First-Order Model Counting

School of Artificial Intelligence, Jilin University, Changchun, China；State Key Laboratory of Complex \& Critical Software Environment, Beihang University, China；National Research Center for Educational Materials, China；Tengen Intelligence Institute, China；Czech Technical University in Prague, Prague, Czech Republic

提出Cofola语言，通过类型化声明式编程和加权一阶模型计数（WFOMC）编译流水线，统一解决集合、多重集、排列、划分等组合计数问题。

2026-05-24cs.AImath.CO

用配分函数近似计算CSP解

Approximate Counting CSP Solutions Using Partition Function

Northeast Normal University（东北师范大学）

提出了一种新的计算约束满足问题（CSP）解个数的近似方法。该方法是在引入自由能的基础上，通过捕捉变量和约束条件的概率关系，推导出配分函数，需要求出边际概率。该算法首先利用置信传播算法求出边缘概率，然后根据配分函数计算解的个数。这允许我们直接将边际概率插入到配分函数中，并有效地计算CSP的解决方案的数量。实验结果表明，该方法可以有效地解决随机问题和结构问题。

2013-09-11cs.AI

使用统计估计的位向量模型计数

Bit-Vector Model Counting using Statistical Estimation

University of Minnesota（明尼苏达大学）

位向量SMT公式的近似模型计数（推广SAT）在概率推理和定量信息流安全等方面有着广泛的应用，但计算困难。添加随机奇偶约束（XOR精简），然后检查可满足性是一种有效的近似技术，但它需要一个关于模型计数的先验假设才能产生有用的结果。我们提出了一种方法的灵感来自统计估计不断完善的概率估计的模型计数的公式，使每个XOR精简查询产生尽可能多的信息。我们实现这种方法，近似的概率模型，作为一个包装周围的现成的SMT求解器或SAT求解器。实验结果表明，该方法的实现速度比以前使用简单的细化策略的最相似的方法。该技术还可以让我们的模型计数公式在浮点数的限制，我们证明了一个应用程序中的漏洞差分隐私机制。

2017-12-21cs.AIcs.CR

更多相关论文收起更多论文

Range and Roots：两种常见的计数和发生约束的验证和验证模式

Range and Roots: Two Common Patterns for Specifying and Propagating Counting and Occurrence Constraints

LIRMM；CNRS（法国国家科学研究中心）；U. Montpellier（蒙彼利埃大学）；UCC（科克大学）；Izmir University of Economics（伊兹密尔经济大学）；Univ. di Bologna（博洛尼亚大学）；NICTA（国家信息与通信技术研究院）；UNSW（新南威尔士大学）

我们提出了范围和根，这是两个常见的模式，用于指定一个广泛的计数和发生的约束。我们为这两种模式设计了专门的传播算法。因此，使用这些模式指定的计数和出现约束直接继承传播算法。为了说明范围和根约束的能力，我们指定了一些从文献中获得的全局约束。初步的实验表明，传播计数和发生的约束，使用这两种模式导致一个小的性能损失相比，专门的全球性的约束，是有竞争力的替代分解使用基本的约束。

2009-03-02cs.AI

验证常规计数约束

Propagating Regular Counting Constraints

Mines de Nantes（南特矿业学院）；Uppsala University（乌普萨拉大学）；NICTA（澳大利亚国家信息与通信技术研究院）；The University of Melbourne（墨尔本大学）

有限变量序列上的约束在排序和排序中是普遍存在的。此外，在实际应用中的各种各样的这种约束导致了一般的建模技术和通用的传播算法，通常基于确定性有限自动机（DFA）及其扩展。我们考虑反DFA（cDFA），它提供了简洁的模型，定期计数的约束，这是约束的次数，定期语言模式出现在一个序列。我们展示了如何在多项式时间内执行域一致性，最多和至少定期计数约束的基础上，频繁的情况下，只接受状态和一个单一的计数器，可以通过转换递增的cDFA。我们还证明了精确正则计数约束的满足是NP难的，并指出精确正则计数约束的不完全算法比[3]中现有的传播算子更快，并提供更多的修剪。常规计数约束与CostRegular约束密切相关，但有助于自然抽象和一些计算优势。

2013-09-27cs.AIcs.FL

一类计数约束的广义弧一致性算法：一种修正的修正版

A Generalized Arc-Consistency Algorithm for a Class of Counting Constraints: Revised Edition that Incorporates One Correction

Mines-Nantes（南特矿业学院）；LINA UMR CNRS 6241（法国国家科学研究中心LINA联合研究单元（UMR 6241））

本文引入了SEQ BIN元约束，并根据其性质，提出了一种实现广义弧一致性的多时间算法。SEQ BIN可用于编码计数约束，如CHANGE、SMOOTH或INCREAS- ING NVALUE。对于其中的一些约束和它们的一些变体，GAC可以在域大小的总和中以线性的时间和空间复杂度来执行，这改进或等于文献中最好的已知结果。

2011-10-21cs.AI

FO2中带基数约束和计数量词的加权模型计数：一个封闭形式公式

Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula

Fondazione Bruno Kessler（布鲁诺·凯斯勒基金会）；University of Trento（特伦托大学）

加权一阶模型计数（WFOMC）计算给定有限域上一阶逻辑理论模型的加权和。一阶逻辑理论，承认多项式时间WFOMC w.r.t域基数被称为域提升。我们引入了解除解释的概念，作为制定封闭形式的WFOMC的工具。使用解除解释，我们重建多项式时间FOMC的封闭形式的公式，在FO2的普遍量化的片段，早期提出的Beame等人。然后，我们扩展这个封闭形式，将基数约束，存在量词，计数量词（又名C2），而不失去域提升。最后，我们表明，所获得的封闭形式激发了一个自然的定义，一个家庭的权重函数严格大于对称的权重函数。

2022-04-12cs.AIcs.LOmath.CO

超越CNF的编译与快速模型计数

Compilation and Fast Model Counting beyond CNF

TU Wien（维也纳技术大学）

本文研究了布尔函数向d-DNNF的编译理论，提出了以关联树宽为参数的固定参数可解（FPT）编译方法，涵盖超越CNF的多种约束，并给出了一种无需编译的更高效FPT模型计数算法。

2025-02-01cs.AIcs.CCcs.LO

带基数约束的二元片段加权模型计数：一个封闭形式公式

Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula

University of Trento（特伦托大学）；Fondazione Bruno Kessler（布鲁诺·凯塞勒基金会）

加权一阶模型计数（WFOMC）计算给定有限域上一阶理论模型的加权和。WFOMC已经成为概率推理的基本工具。WFOMC算法在多项式时间内运行。域大小被称为提升推理算法。这样的算法已经开发了多个扩展的FO2（片段的一阶逻辑与两个变量）的特殊情况下的对称权函数。我们引入的概念，解除解释作为制定多项式WFOMC的工具。使用解除的解释，我们重建多项式时间FOMC在FO2的通用片段，早期提出的Beame等人的封闭形式的公式。然后，我们扩展这个封闭形式，将存在量词和基数约束，而不失去域的可提升性。最后，我们表明，所获得的封闭形式激发了一个自然的定义，一个家庭的权重函数严格大于对称的权重函数。

2021-05-28cs.AIcs.LO

基于散列的近似DNF计数方法研究

On Hashing-Based Approaches to Approximate DNF-Counting

National University of Singapore（新加坡国立大学）；Rice University（莱斯大学）

命题模型计数是人工智能中的一个基本问题，有着广泛的应用，如概率推理、不确定性决策和概率数据库。因此，这个问题既有理论意义，也有实际意义。当约束表示为DNF公式时，基于蒙特卡罗的技术已被证明可以提供完全多项式随机近似方案（FPRAS）。对于CNF约束，基于散列的近似技术已被证明是非常成功的。此外，它表明，基于散列的技术也产生一个FPRAS的DNF计数，而不使用蒙特卡洛采样。然而，我们的分析表明，提出的基于散列的方法来DNF计数提供穷人的时间复杂度相比，基于蒙特卡洛的DNF计数技术。鉴于基于散列的技术在CNF约束中的成功，很自然地会问：基于散列的技术能否为DNF计数提供有效的FPRAS？在本文中，我们提供了一个肯定的答案，这个问题。为此，我们介绍了两种新的算法技术：\emph{Symbolic Hashing}和\emph{Stochastic Cell Counting}，以及一个新的哈希家族\emph{Row-Echelon hash functions}。这些创新使我们能够设计一个基于散列的FPRAS DNF计数类似的复杂性（多对数因子），作为以前的作品。此外，我们希望这些技术有潜在的应用超越DNF计数。

2017-10-14cs.AIcs.LO

CombEval：评估大语言模型中组合计数的框架

CombEval: A Framework for Evaluating Combinatorial Counting in Large Language Models

School of Artificial Intelligence, Jilin University（吉林大学人工智能学院）；Czech Technical University in Prague（捷克布拉格理工大学）；CRRC Zhuzhou Institute（中车株洲研究所）；Tengen Intelligence Institute（天元智能研究院）；International Center of Future Science, Jilin University（吉林大学未来科学国际合作中心）；Engineering Research Center of Knowledge-Driven Human-Machine Intelligence, MOE（教育部知识驱动人机智能工程研究中心）

提出CombEval动态基准，通过类型化Cofola规范生成组合计数问题，评估11个大语言模型在直接和代码增强设置下的表现，发现模型在有序对象、不可区分元素、相对位置约束和嵌套对象依赖上存在脆弱性。

2026-10-01cs.AIcs.CL

超越加权模型计数的高效知识编译

Efficient Knowledge Compilation Beyond Weighted Model Counting

TU Vienna（维也纳工业大学）；KU Leuven（鲁汶大学）

逻辑编程的定量扩展通常需要解决所谓的第二级推理任务，即，在加法和乘法之上涉及第三操作（诸如最大化或归一化）的问题，并且因此超出了分布语义下的概率逻辑编程的公知的加权或代数模型计数设置。我们引入二级代数模型计数（2AMC）作为这些问题的通用框架。由于2AMC是（代数）模型计数的forall-exists-SAT是命题可满足性，这是出了名的难以解决。基于知识编译（KC）的第一级技术已被改编为特定的2AMC实例施加可变的顺序约束所产生的电路。然而，这些约束会严重增加电路尺寸，从而降低这种方法的效率。我们表明，我们可以利用2AMC问题的逻辑结构，省略这些约束的一部分，从而限制了负面影响。此外，我们引入并实现了一个策略，以产生一个足够的约束静态，与先验保证KC的性能。我们对几个基准和任务的实证评估证实了我们的理论结果可以转化为更有效的解决在实践中。正在考虑接受TPLP。

2022-05-16cs.AIcs.LO

约束计数和抽样：弥合理论与实践之间的差距

Constrained Counting and Sampling: Bridging the Gap between Theory and Practice

约束计数和抽样是计算机科学中的两个基本问题，具有许多应用，包括网络可靠性、隐私、概率推理和约束随机验证。在约束计数中，任务是根据给定的加权函数计算给定约束的解集的总权重。在约束抽样中，任务是随机抽样，服从给定的加权函数，从一组给定约束的解决方案中。因此，约束计数和抽样多年来一直受到密集的理论和实证研究。然而，以前的工作，提供了启发式技术的准确性保证较差或方法与证明的保证，但在实践中表现不佳。在这篇论文中，我们介绍了一种新的基于哈希的算法框架约束采样和计数，结合了经典的算法技术的通用哈希组合推理工具，特别是，SAT和SMT，在过去的二十年中取得的巨大进展。由此产生的计数框架（ApproxMC 2）和采样框架（UniGen）可以处理具有多达百万个变量的公式，这比现有技术工具处理数百个变量的能力有了显着提高。如果初始约束集表示为析取范式（DNF），则ApproxMC是唯一已知的不涉及Monte Carlo步骤的完全多项式随机逼近方案（FPRAS）。通过利用公式的可定义性和由3-通用散列函数定义的单元格中的解的分布的方差之间的联系，我们引入了一种算法技术MIS，该算法技术将底层通用散列函数中采用的XOR约束的大小减少了多达两个数量级。

2018-06-06cs.AIcs.LO

困难模型计数器的生成与预测

Generation and Prediction of Difficult Model Counting Instances

Insight Centre for Data Analytics（洞察数据分析中心）；University College Cork（科克大学学院）

我们提出了一种方法来创建小而困难的模型计数实例。我们的生成器是高度可参数化的：它生成的实例的变量数量，以及它们的子句数量和每个子句中的文字数量，都可以设置为任何值。我们的实例已经在最先进的模型计数器上进行了测试，与其他困难的模型计数实例相比，在模型计数比赛中。在变量数量和子句数量方面，竞赛中最小的未解决实例都是我们的。在随机实例和生成器构建的实例中，我们还观察到固定变量数量和改变子句数量时的难度峰值。使用这些结果，我们预测的参数值，最难计数的实例将发生。

2022-12-06cs.AI

一种基于攻击者和防御者计数的抽象论证方法

Attacker and Defender Counting Approach for Abstract Argumentation

Tsinghua University（清华大学）

在Dung的抽象论证中，给定一个选择的可接受性概念，论证要么是可接受的，要么是不可接受的。这给出了一种粗略的比较参数的方法。在本文中，我们提出了一个计数的方法，更好地获得评估的论点，通过统计各自的攻击者和防御者的数量的论点图和论点游戏的基础上。一个论点是更容易接受的，如果支持者提出了更多的捍卫者，反对者提出了更少的攻击者对它。我们表明，我们的计数模型有两个良好的行为性质：规范化和收敛。然后，我们定义了一个基于该模型的计数语义，并研究了语义的一些一般性质。

2015-06-13cs.AI

求解带有可证明保证的面向符号与统计AI集成的模计数可满足性问题

Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees

Purdue University（普渡大学）

提出XOR-SMC算法，通过随机化XOR约束将NP^PP-完全的模计数可满足性问题转化为SAT问题，在多项式时间内提供常数近似保证，并在AI向善实验中优于基线。

2023-12-30cs.AIcs.CCcs.LO