New Encodings of Pseudo-Boolean Constraints into CNF
From MaRDI portal
Publication:3637167
DOI10.1007/978-3-642-02777-2_19zbMath1247.68246MaRDI 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
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Related Items
Shared aggregate sets in answer set programming, On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving, Rewriting optimization statements in answer-set programs, Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints, Exact and approximate determination of the Pareto front using minimal correction subsets, Exploiting subproblem optimization in SAT-based maxsat algorithms, Cardinality networks: a theoretical and empirical study, WPM3: an (in)complete algorithm for weighted partial MaxSAT, \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT, SAT encodings for pseudo-Boolean constraints together with at-most-one constraints, Constrained pseudo-propositional logic, A Boolean satisfiability approach to the resource-constrained project scheduling problem, Improving the Normalization of Weight Rules in Answer Set Programs, Optimal Base Encodings for Pseudo-Boolean Constraints, BDDs for Pseudo-Boolean Constraints – Revisited, Propositional SAT Solving, PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
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