Olivier Bailleux
In this report, we propose a quick survey of the currently known techniques for encoding a Boolean cardinality constraint into a CNF formula, and we discuss about the relevance of these encodings. We also propose models to facilitate analysis and design of CNF encodings for Boolean constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied for their uses in the design of algorithms for various computational problems on CNF-formulas. Here we consider the expressivity of these formulas in the model of clausal encodings with auxiliary variables. We first show that bounding the width for many of the measures from the literature leads to a dramatic loss of expressivity, restricting the formulas to …
The runtime performance of modern SAT solvers is deeply connected to the phase transition behavior of CNF formulas. While CNF solving has witnessed significant runtime improvement over the past two decades, the same does not hold for several other classes such as the conjunction of cardinality and XOR constraints, denoted as CARD-XOR formulas. The problem of determining the satisfiability of CARD-XOR formulas is a fundamental problem with a wide variety of applications ranging from discrete integration in the field of artificial intelligence to maximum likelihood decoding in coding theory. The…
This is a commentary on the CP 2003 paper "Efficient cnf encoding of boolean cardinality constraints". After recalling its context, we outline a classification of Constraints with respect to their deductive power regarding General Arc Consistency (GAC).
BoolVar/PB is an open source java library dedicated to the translation of pseudo-Boolean constraints into CNF formulae. Input constraints can be categorized with tags. Several encoding schemes are implemented in a way that each input constraint can be translated using one or several encoders, according to the related tags. The library can be easily extended by adding new encoders and / or new output formats.
Compilation and Fast Model Counting beyond CNF
本文研究了布尔函数向d-DNNF的编译理论，提出了以关联树宽为参数的固定参数可解（FPT）编译方法，涵盖超越CNF的多种约束，并给出了一种无需编译的更高效FPT模型计数算法。
PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas
针对CNF表示不自然的问题，提出在表达能力更强的伪布尔公式上执行加权模型计数，基于ADDMC框架实现工具PBCounter，实验表明其优于现有CNF计数器。
In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formulation. To avoid combinatorial explosion, Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, …
We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings and leads to speed-ups in solving times.
We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate f…
Efficient Representations for High-Cardinality Categorical Variables in Machine Learning
针对高基数分类变量导致的稀疏高维与可扩展性问题，提出均值、低秩和多项逻辑回归编码，并用理论与实验验证其性能及效率提升。
Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with propagation strength guarantees rely upon prior compilation of the constraints into DNNF (decomposable negation normal form), BDD (binary decision diagram), or some other sub-variants. However it has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size. Since DNNFs a…
Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs
针对特征模型中基数约束等表达性构造难以高效转换为 CNF 的问题，提出伪布尔编码与编译为 d-DNNF 的新方法，显著加速表达性特征模型的自动推理，并在基本构造上保持竞争力。
Power Term Polynomial Algebra for Boolean Logic
提出幂项多项式代数，一种介于CNF和ANF之间的布尔公式表示语言，通过幂项和多项式直接编码CNF子句与单项式族，避免辅助变量和约束，支持代数运算与重写规则。
In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literal-weighted CNF formula $φ$, we study Boolean MPE, a more general problem that requests a model $τ$ of $φ$ with the highest weight, where the weight of $τ$ is the product of weights of literals satisfied by $τ$. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. Recent work proposed DPMC, a dynamic-programming model counter that leverages graph-decomposition te…
Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
本文针对混合SAT求解问题，提出基于惩罚项的无约束连续优化公式，并通过理论与实验证明Adam等无约束优化器能有效提升混合基准上的SAT求解性能。
We study local-search satisfiability solvers for propositional logic extended with cardinality atoms, that is, expressions that provide explicit ways to model constraints on cardinalities of sets. Adding cardinality atoms to the language of propositional logic facilitates modeling search problems and often results in concise encodings. We propose two ``native'' local-search solvers for theories in the extended language. We also describe techniques to reduce the problem to standard propositional satisfiability and allow us to use off-the-shelf SAT solvers. We study these methods experimentally.…
The At-Most-One (AMO) constraint is a special case of cardinality constraint that requires at most one variable from a set of Boolean variables to be set to TRUE. AMO is important for modeling problems as Boolean satisfiability (SAT) from domains where decision variables represent spatial or temporal placements of some objects that cannot share the same spatial or temporal slot. The AMO constraint can be used for more efficient representation and problem solving in mutex networks consisting of pair-wise mutual exclusions forbidding pairs of Boolean variable to be simultaneously TRUE. An on-lin…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。