B-Cubing: New Possibilities for Efficient SAT-Solving

SAT (Boolean satisfiability) has become the primary Boolean reasoning engine for many EDA (electronic design automation) applications, so the efficiency of SAT-solving is of great practical importance. B-cubing is our extension and generalization of Goldberg et al.'s supercubing, an approach to...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computers 2006-11, Vol.55 (11), p.1315-1324
Main Authors: Babic, D., Bingham, J., Hu, A.J.
Format: Article
Language:English
Subjects:
Algorithms
Benchmarks
Boolean algebra
Boolean satisfiability
Electronics
Pruning
SAT
search space pruning
Solvers
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:SAT (Boolean satisfiability) has become the primary Boolean reasoning engine for many EDA (electronic design automation) applications, so the efficiency of SAT-solving is of great practical importance. B-cubing is our extension and generalization of Goldberg et al.'s supercubing, an approach to pruning in SAT-solving completely different from the standard approach used in leading solvers. We have built a B-cubing-based solver that is competitive with, and often outperforms, leading conventional solvers (e.g., ZChaff II) on a wide range of EDA benchmarks. However, B-cubing is hard to understand and even the correctness of the algorithm is not obvious. This paper presents the theoretical basis for B-cubing, proves our approach correct, details our implementation and experimental results, and maps out other correct possibilities for further improving SAT-solving
ISSN:0018-9340
1557-9956
DOI:10.1109/TC.2006.175