FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited

Authors: Neng-Fa Zhou and Håkan Kjellerstrand

Paper Information

Title:Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
Authors:Neng-Fa Zhou and Håkan Kjellerstrand
Proceedings:RCRA Full papers
Editor: Marco Maratea
Keywords:SAT encoding, PB constraints, BDD, Constraint programming
Abstract:

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.

Pages:14
Talk:Jul 13 14:44 (Session 87J: Constraint Satisfiability)
Paper: