Download PDFOpen PDF in browser

Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited

EasyChair Preprint 154

14 pagesDate: May 22, 2018

Abstract

Pseudo-Boolean constraints constitute an important class of constraints. Despite extensive studies of SAT encodings for PB constraints, there are no generally accepted SAT encodings for PB constraints. In this paper we revisit encoding PB constraints into SAT via binary adders and BDDs. For the binary adder encoding, we present an optimizing compiler that incorporates preprocessing, decomposition, constant propagation, and common subexpression elimination techniques tailored to PB constraints. For encoding via BDDs, we compare three methods for converting BDDs into SAT, namely, path encoding, 6-clause node encoding, and 2-clause node encoding. We experimentally compare these encodings on three sets of benchmarks. Our experiments revealed surprisingly good and consistent performance of the optimized adder encoder in comparison with other encoders.

Keyphrases: BDD, Constraint Programming, PB constraints, SAT encoding

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:154,
  author    = {Neng-Fa Zhou and Håkan Kjellerstrand},
  title     = {Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited},
  doi       = {10.29007/wh86},
  howpublished = {EasyChair Preprint 154},
  year      = {EasyChair, 2018}}
Download PDFOpen PDF in browser