New Encodings of Pseudo-Boolean Constraints into CNF

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

zbMATH Keywords

pseudo-Boolean; SAT translation

Mathematics Subject Classification ID

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

• Pueblo
• PBS

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