Efficient CNF encoding of Boolean cardinality constraints
From MaRDI portal
Publication:5897193
DOI10.1007/B13743zbMATH Open1273.68332OpenAlexW2497660909MaRDI QIDQ5897193FDOQ5897193
Authors: Olivier Bailleux, Yacine Boufkhad 
Publication date: 2 March 2010
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b13743
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)
Cited In (48)
- Boolean satisfiability in quantum compilation
- Set constraint model and automated encoding into SAT: application to the social golfer problem
- Comparing integer linear programming to SAT-solving for hard problems in computational and systems biology
- Detecting cardinality constraints in CNF
- Perfect hashing and CNF encodings of cardinality constraints
- Solving satisfiability problems with preferences
- Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
- An efficient approach to solving random \(k\)-SAT problems
- SAT-boosted tabu search for coloring massive graphs
- \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
- Curriculum-based course timetabling with SAT and MaxSAT
- Learning Optimal Decision Sets and Lists with SAT
- Cardinality Networks and Their Applications
- Exact and approximate determination of the Pareto front using minimal correction subsets
- Hard satisfiable 3-SAT instances via autocorrelation
- An efficient strategy to construct a better differential on multiple-branch-based designs: application to Orthros
- Some computational aspects of DISTANCE SAT
- A lower bound on CNF encodings of the at-most-one constraint
- Circuit Based Encoding of CNF Formula
- Resizing cardinality constraints for MaxSAT
- Towards Robust CNF Encodings of Cardinality Constraints
- Parallel SAT framework to find clustering of differential characteristics and its applications
- CNF encodings of symmetric functions
- Iterative and core-guided maxsat solving: a survey and assessment
- A SAT encoding to compute aperiodic tiling rhythmic canons
- On preprocessing for weighted MaxSAT
- Weighted positive binary decision diagrams for exact probabilistic inference
- Propagation via lazy clause generation
- New Encodings of Pseudo-Boolean Constraints into CNF
- SAT encodings for pseudo-Boolean constraints together with at-most-one constraints
- Certified Core-Guided MaxSAT Solving
- A Boolean satisfiability approach to the resource-constrained project scheduling problem
- Exploiting resolution-based representations for MaxSAT solving
- GAC Via Unit Propagation
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- On using incremental encodings in unsatisfiability-based MaxSAT solving
- Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems
- Sorting nine inputs requires twenty-five comparisons
- QMaxSATpb: a certified MaxSAT solver
- Efficient Generation of Small Interpolants in CNF
- Multi-agent path finding with mutex propagation
- Cardinality networks: a theoretical and empirical study
- New core-guided and hitting set algorithms for multi-objective combinatorial optimization
- Computing optimal hypertree decompositions with SAT
- On an MCS-based inconsistency measure
- WPM3: an (in)complete algorithm for weighted partial MaxSAT
- Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems
- Efficient SAT-based encodings of conditional cardinality constraints
Uses Software
This page was built for publication: Efficient 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 Q5897193)
