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

DOI10.1007/978-3-319-24318-4_2zbMATH Open1471.68261OpenAlexW2223094528MaRDI QIDQ3453205FDOQ3453205

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (17)

• Efficient Learning of Interpretable Classification Rules
• Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
• Optimal base encodings for pseudo-Boolean constraints
• OptiLog: a framework for SAT-based systems
• On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint
• Efficient local search for pseudo Boolean optimization
• Computing generating sets of minimal size in finite algebras
• PBLib
• 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

Uses Software

• MiniSat
• NiVER
• 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)