Cardinality networks: a theoretical and empirical study

DOI10.1007/s10601-010-9105-0zbMath1217.68200OpenAlexW2012413542MaRDI QIDQ538318

Enric Rodríguez-Carbonell, Roberto Asín, Albert Oliveras, Robert Nieuwenhuis

Publication date: 25 May 2011

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-010-9105-0

zbMATH Keywords

cardinality constraintsSATSAT encodings

Mathematics Subject Classification ID

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

Related Items

Propositional SAT Solving ⋮ \textsc{Conjure}: automatic generation of constraint models from problem specifications ⋮ Improving the Normalization of Weight Rules in Answer Set Programs ⋮ WPM3: an (in)complete algorithm for weighted partial MaxSAT ⋮ Encoding cardinality constraints using standard encoding of generalized selection networks preserves arc-consistency ⋮ Sorting networks: to the end and back again ⋮ Exact and approximate determination of the Pareto front using minimal correction subsets ⋮ Rewriting optimization statements in answer-set programs ⋮ Resizing cardinality constraints for MaxSAT ⋮ Mining top-\(k\) motifs with a SAT-based framework ⋮ Compiling finite domain constraints to SAT withBEE ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ Encoding cardinality constraints using multiway merge selection networks ⋮ On propositional coding techniques for the distinguishability of objects in finite sets ⋮ A lower bound on CNF encodings of the at-most-one constraint ⋮ Delegatable Functional Signatures ⋮ SAT encodings for pseudo-Boolean constraints together with at-most-one constraints ⋮ Writing Declarative Specifications for Clauses ⋮ On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving ⋮ Iterative and core-guided maxsat solving: a survey and assessment

Uses Software

• MiniSat
• Plingeling
• PrecoSAT
• Lingeling

Cites Work

• Unnamed Item
• Unnamed Item
• A linear-time transformation of linear inequalities into conjunctive normal form
• Solving SAT and SAT Modulo Theories
• Towards Robust CNF Encodings of Cardinality Constraints
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• New Encodings of Pseudo-Boolean Constraints into CNF
• Diagnosis of Discrete Event Systems Using Satisfiability Algorithms: A Theoretical and Empirical Study
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2003