Efficient SAT-based encodings of conditional cardinality constraints

DOI10.29007/KFJBzbMATH Open1415.68185arXiv1804.00211OpenAlexW2908513458MaRDI QIDQ5222954FDOQ5222954

Authors: Abdelhamid Boudane, Said Jabbour, Badran Baddaoui, Lakhdar Sais 

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Abstract: 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, the polarity of the sub-formula $Phi$ is taken into account leading to conditional constraints of the form $yightarrowPhi$, or $Phiightarrowy$, where $y$ is a fresh propositional variable. In the case where $Phi$ represents a cardinality constraint, such translation leads to conditional cardinality constraints subject of the present paper. We first show that when all the clauses encoding the cardinality constraint are augmented with an additional new variable, most of the well-known encodings cease to maintain the generalized arc consistency property. Then, we consider some of these encodings and show how they can be extended to recover such important property. An experimental validation is conducted on a SAT-based pattern mining application, where such conditional cardinality constraints is a cornerstone, showing the relevance of our proposed approach.

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

Recommendations

• A parametric approach for smaller and better encodings of cardinality constraints
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Efficient CNF encoding of Boolean cardinality constraints
• Cardinality networks: a theoretical and empirical study
• Cardinality Networks and Their Applications

zbMATH Keywords

modellingcardinality constraintspropositional satisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited In (5)

• Incremental Encoding and Solving of Cardinality Constraints
• A parametric approach for smaller and better encodings of cardinality constraints
• Encoding cardinality constraints using standard encoding of generalized selection networks preserves arc-consistency
• Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models
• More Efficient Match-Making and Satisfiability The Five Card Trick

This page was built for publication: Efficient SAT-based encodings of conditional cardinality constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5222954)