Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Cited In (81)

Boolean satisfiability in quantum compilation
On the query complexity of selecting minimal sets for monotone predicates
Differential cryptanalysis of round-reduced \texttt{SPEEDY} family
\textsc{OptiMathSAT}: a tool for optimization modulo theories
meSAT: multiple encodings of CSP to SAT
\textit{teaspoon}: solving the curriculum-based course timetabling problems with answer set programming
Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
Encoding Treewidth into SAT
\(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
Optimal symmetry breaking for graph problems
Learning Optimal Decision Sets and Lists with SAT
PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
Intra- and interdiagram consistency checking of behavioral multiview models
Propositional proof systems based on maximum satisfiability
Cardinality Networks and Their Applications
Delegatable Functional Signatures
Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
Hard satisfiable 3-SAT instances via autocorrelation
Some computational aspects of DISTANCE SAT
A lower bound on CNF encodings of the at-most-one constraint
A SAT Approach to Clique-Width
Three-dimensional stable matching with cyclic preferences
Towards Robust CNF Encodings of Cardinality Constraints
Real-time solving of computationally hard problems using optimal algorithm portfolios
Generating extended resolution proofs with a BDD-based SAT solver
Algorithms for computing minimal unsatisfiable subsets of constraints
Propositional SAT Solving
Iterative and core-guided maxsat solving: a survey and assessment
A greater \texttt{GIFT}: strengthening \texttt{GIFT} against statistical cryptanalysis
Coupling different integer encodings for SAT
Modeling and solving staff scheduling with partial weighted maxSAT
Boosting branch-and-bound MaxSAT solvers with clause learning
A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis
New Encodings of Pseudo-Boolean Constraints into CNF
A nonexistence certificate for projective planes of order ten with weight 15 codewords
GAC Via Unit Propagation
Formal Analysis of the Entropy / Security Trade-off in First-Order Masking Countermeasures against Side-Channel Attacks
Backdoors to tractable answer set programming
Implementing Efficient All Solutions SAT Solvers
Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models
Computing properties of stable configurations of thermodynamic binding networks
Parameterized complexity classes beyond para-NP
Automatic Search of Linear Trails in ARX with Applications to SPECK and Chaskey
Encoding cardinality constraints using multiway merge selection networks
Propagation complete encodings of smooth DNNF theories
Multi-agent path finding with mutex propagation
maxSAT-based large neighborhood search for high school timetabling
Solving (Weighted) Partial MaxSAT through Satisfiability Testing
Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability
Mining top-\(k\) motifs with a SAT-based framework
Cardinality networks: a theoretical and empirical study
Computer-aided proof of Erdős discrepancy properties
Non-uniform Boolean Constraint Satisfaction Problems with Cardinality Constraint
Computing optimal hypertree decompositions with SAT
On an MCS-based inconsistency measure
Learning discrete decomposable graphical models via constraint optimization
WPM3: an (in)complete algorithm for weighted partial MaxSAT
Drawing Order Diagrams Through Two-Dimension Extension
Sequential Encodings from Max-CSP into Partial Max-SAT
Improved attacks on \texttt{GIFT-64}
Interactive portfolio selection involving multicriteria sorting 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
On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving
SAT-based optimal classification trees for non-binary data
New method for combining Matsui's bounding conditions with sequential encoding method
Improved the automated evaluation algorithm against differential attacks and its application to WARP
MiFuMax—a Literate MaxSAT Solver
Convexity of division property transitions: theory, algorithms and compact models
Balanced covering arrays: A classification of covering arrays and packing arrays via exact methods
Finding the Hardest Formulas for Resolution
Parallel SAT framework to find clustering of differential characteristics and its applications
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
CNF encodings of symmetric functions
Automated-based rebound attacks on ACE permutation
Exploring SAT for cryptanalysis: (quantum) collision attacks against 6-round SHA-3
State identification and verification with satisfaction
Clausal proofs for pseudo-Boolean reasoning
Conflict-free electric vehicle routing problem: an improved compositional algorithm
Planning with partial observability by SAT
Distinguisher and related-key attack on HALFLOOP-96

This page was built for publication: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

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