PBLib -- a library for encoding pseudo-Boolean constraints into CNF

DOI10.1007/978-3-319-24318-4_2MaRDI QIDQ3453205zbMATH OpenOpenAlexFDO

Authors Tobias Philipp, Peter Steinke

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24318-4_2

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• New Encodings of Pseudo-Boolean Constraints into CNF
• scientific article; zbMATH DE number 5139168
• Optimal base encodings for pseudo-Boolean constraints
• SAT encodings for pseudo-Boolean constraints together with at-most-one constraints
• scientific article; zbMATH DE number 5139167

Cites work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• A parametric approach for smaller and better encodings of cardinality constraints
• A structure-preserving clause form translation
• Algorithms for computing minimal unsatisfiable subsets of constraints
• BDDs for pseudo-Boolean constraints -- revisited
• Handbook of constraint programming.
• New Encodings of Pseudo-Boolean Constraints into CNF
• Pseudo-Boolean optimization
• Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Cited in

(17)

• Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
• Efficient Learning of Interpretable Classification Rules
• OptiLog: a framework for SAT-based systems
• Optimal base encodings for pseudo-Boolean constraints
• On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint
• Efficient local search for pseudo Boolean optimization
• PBLib
• Computing generating sets of minimal size in finite algebras
• SAT race 2015
• A SAT encoding to compute aperiodic tiling rhythmic canons
• Coupling different integer encodings for SAT
• New Encodings of Pseudo-Boolean Constraints into CNF
• SAT encodings for pseudo-Boolean constraints together with at-most-one constraints
• Generation of synchronizing state machines from a transition system: a region-based approach
• The TPTP problem library. CNF release v1. 2. 1
• Encoding cardinality constraints using multiway merge selection networks
• SAT competition 2020

Describes a project that uses

Uses Software

• npSolver
• BoolVar/PB
• NiVER
• MiniSat

This page was built for publication: PBLib -- a library for encoding pseudo-Boolean constraints into CNF

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