New Encodings of Pseudo-Boolean Constraints into CNF
From MaRDI portal
Publication:3637167
DOI10.1007/978-3-642-02777-2_19zbMath1247.68246OpenAlexW4301887518MaRDI QIDQ3637167
Olivier Roussel, Yacine Boufkhad, Olivier Bailleux
Publication date: 7 July 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02777-2_19
Related Items (17)
PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF ⋮ Propositional SAT Solving ⋮ Shared aggregate sets in answer set programming ⋮ Improving the Normalization of Weight Rules in Answer Set Programs ⋮ WPM3: an (in)complete algorithm for weighted partial MaxSAT ⋮ Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints ⋮ Exact and approximate determination of the Pareto front using minimal correction subsets ⋮ A Boolean satisfiability approach to the resource-constrained project scheduling problem ⋮ Rewriting optimization statements in answer-set programs ⋮ Constrained pseudo-propositional logic ⋮ Optimal Base Encodings for Pseudo-Boolean Constraints ⋮ BDDs for Pseudo-Boolean Constraints – Revisited ⋮ Exploiting subproblem optimization in SAT-based maxsat algorithms ⋮ Cardinality networks: a theoretical and empirical study ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ SAT encodings for pseudo-Boolean constraints together with at-most-one constraints ⋮ On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A linear-time transformation of linear inequalities into conjunctive normal form
- GAC Via Unit Propagation
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Formalizing Dangerous SAT Encodings
- Principles and Practice of Constraint Programming – CP 2003
This page was built for publication: New Encodings of Pseudo-Boolean Constraints into CNF