Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
From MaRDI portal
Publication:3524229
DOI10.1007/11564751_73zbMath1153.68488OpenAlexW2100609826MaRDI QIDQ3524229
Publication date: 9 September 2008
Published in: Principles and Practice of Constraint Programming - CP 2005 (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.87.6156
Related Items (71)
On an MCS-based inconsistency measure ⋮ PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF ⋮ Propositional SAT Solving ⋮ A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis ⋮ maxSAT-based large neighborhood search for high school timetabling ⋮ Parameterized complexity classes beyond para-NP ⋮ A greater \texttt{GIFT}: strengthening \texttt{GIFT} against statistical cryptanalysis ⋮ Coupling different integer encodings for SAT ⋮ Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem ⋮ Some computational aspects of DISTANCE SAT ⋮ WPM3: an (in)complete algorithm for weighted partial MaxSAT ⋮ A SAT Approach to Clique-Width ⋮ SAT-based optimal classification trees for non-binary data ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ New method for combining Matsui's bounding conditions with sequential encoding method ⋮ Computing optimal hypertree decompositions with SAT ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Boosting branch-and-bound MaxSAT solvers with clause learning ⋮ State identification and verification with satisfaction ⋮ Interactive portfolio selection involving multicriteria sorting models ⋮ Differential cryptanalysis of round-reduced \texttt{SPEEDY} family ⋮ Exploring SAT for cryptanalysis: (quantum) collision attacks against 6-round SHA-3 ⋮ Convexity of division property transitions: theory, algorithms and compact models ⋮ A comparison of ASP-based and SAT-based algorithms for the contension inconsistency measure ⋮ Exact and approximate determination of the Pareto front using minimal correction subsets ⋮ Drawing Order Diagrams Through Two-Dimension Extension ⋮ Balanced covering arrays: A classification of covering arrays and packing arrays via exact methods ⋮ GAC Via Unit Propagation ⋮ Towards Robust CNF Encodings of Cardinality Constraints ⋮ \textit{teaspoon}: solving the curriculum-based course timetabling problems with answer set programming ⋮ Modeling and solving staff scheduling with partial weighted maxSAT ⋮ Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions ⋮ Propositional proof systems based on maximum satisfiability ⋮ Finding the Hardest Formulas for Resolution ⋮ Mining top-\(k\) motifs with a SAT-based framework ⋮ Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability ⋮ Algorithms for computing minimal unsatisfiable subsets of constraints ⋮ Intra- and interdiagram consistency checking of behavioral multiview models ⋮ Learning discrete decomposable graphical models via constraint optimization ⋮ Cardinality networks: a theoretical and empirical study ⋮ Three-dimensional stable matching with cyclic preferences ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ Encoding cardinality constraints using multiway merge selection networks ⋮ Optimal symmetry breaking for graph problems ⋮ A lower bound on CNF encodings of the at-most-one constraint ⋮ Delegatable Functional Signatures ⋮ Real-time solving of computationally hard problems using optimal algorithm portfolios ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Encoding Treewidth into SAT ⋮ Sequential Encodings from Max-CSP into Partial Max-SAT ⋮ Cardinality Networks and Their Applications ⋮ New Encodings of Pseudo-Boolean Constraints into CNF ⋮ Solving (Weighted) Partial MaxSAT through Satisfiability Testing ⋮ Automatic Search of Linear Trails in ARX with Applications to SPECK and Chaskey ⋮ Computing properties of stable configurations of thermodynamic binding networks ⋮ Formal Analysis of the Entropy / Security Trade-off in First-Order Masking Countermeasures against Side-Channel Attacks ⋮ Boolean satisfiability in quantum compilation ⋮ Propagation complete encodings of smooth DNNF theories ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords ⋮ Multi-agent path finding with mutex propagation ⋮ Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models ⋮ Backdoors to tractable answer set programming ⋮ meSAT: multiple encodings of CSP to SAT ⋮ On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving ⋮ MiFuMax—a Literate MaxSAT Solver ⋮ Hard satisfiable 3-SAT instances via autocorrelation ⋮ Iterative and core-guided maxsat solving: a survey and assessment ⋮ Implementing Efficient All Solutions SAT Solvers ⋮ Learning Optimal Decision Sets and Lists with SAT ⋮ On the query complexity of selecting minimal sets for monotone predicates
This page was built for publication: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
