A lower bound on CNF encodings of the at-most-one constraint

DOI10.1007/978-3-319-66263-3_26zbMath1417.68198arXiv1704.08934OpenAlexW2963190649WikidataQ62044316 ScholiaQ62044316MaRDI QIDQ5915765

Vojtěch Vorel, Petr Savický, Petr Kučera

Publication date: 15 November 2017

Published in: Theoretical Computer Science, Theory and Applications of Satisfiability Testing – SAT 2017 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1704.08934

zbMATH Keywords

knowledge compilationcardinality constraintat most one constraintpropagation-complete encodingpropagation complete encoding

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (2)

A lower bound on CNF encodings of the at-most-one constraint ⋮ On the complexity of monotone circuits for threshold symmetric Boolean functions

Uses Software

• JBool

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cardinality networks: a theoretical and empirical study
• Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Complexity issues related to propagation completeness
• Automatic Generation of Propagation Complete SAT Encodings
• Perfect Hashing and CNF Encodings of Cardinality Constraints
• Knowledge Compilation with Empowerment
• GAC Via Unit Propagation
• Towards Robust CNF Encodings of Cardinality Constraints
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• A Computing Procedure for Quantification Theory
• Principles and Practice of Constraint Programming – CP 2003
• A lower bound on CNF encodings of the at-most-one constraint

This page was built for publication: A lower bound on CNF encodings of the at-most-one constraint