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

• 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.
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• 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

(21)

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

Describes a project that uses

Uses Software

• NiVER
• MiniSat
• BoolVar/PB
• npSolver

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)