scholarly journals Generating Extended Resolution Proofs with a BDD-Based SAT Solver

2021 ◽  
pp. 76-93
Author(s):  
Randal E. Bryant ◽  
Marijn J. H. Heule
Keyword(s):  
Binary Decision Diagrams ◽  
Boolean Satisfiability ◽  
Logical Framework ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Sat Solvers ◽  
Sat Solver ◽  
Resolution Proofs ◽  
Existential Quantification ◽  
Checkable Proof

AbstractIn 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in theextended resolutionlogical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such proofs indicate that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it.We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a prototype solver to obtain polynomially sized proofs on benchmarks for the mutilated chessboard and pigeonhole problems—ones that are very challenging for search-based SAT solvers.

scholarly journals Building free Binary Decision Diagrams using SAT solvers

2007 ◽  
Vol 20 (3) ◽  
pp. 381-394 ◽  
Author(s):  
Robert Wille ◽  
Görschwin Fey ◽  
Rolf Drechsler
Keyword(s):  
Boolean Functions ◽  
Binary Decision Diagrams ◽  
Compact Representation ◽  
Decision Diagrams ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Sat Solvers ◽  
Free Binary Decision Diagrams ◽  
Sat Solver ◽  
Open Question

Free Binary Decision Diagrams (FBDDs) are a data structure for the representation of Boolean functions. In contrast to Ordered Binary Decision Diagrams (OBDDs) FBDDs allow different variable orderings along each path. Thus, FBDDs are the more compact representation while most of the properties of OBDDs are kept. However, how to efficiently build small FBDDs for a given function is still an open question. In this work we propose FBDD construction with the help of SAT solvers. "Recording" the single steps of a SAT solver during the search process leads to an FBDD. Furthermore, by exploiting approaches for identifying isomorphic sub-graphs, i.e. cutlines or cutsets reduced FBDDs are constructed.

NC-ALGORITHMS FOR OPERATIONS ON BINARY DECISION DIAGRAMS

1993 ◽  
Vol 03 (01) ◽  
pp. 3-12 ◽  
Author(s):  
DETLEF SIELING ◽  
INGO WEGENER
Keyword(s):  
Binary Decision Diagrams ◽  
Pattern Generation ◽  
Decision Diagrams ◽  
Equivalence Test ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Verification Test ◽  
Logical Synthesis ◽  
Redundancy Test ◽  
Nc Algorithms

(Ordered) binary decision diagrams are a powerful representation for Boolean functions and are widely used in logical synthesis, verification, test pattern generation or as part of CAD tools. NC-algorithms are presented for the most important operations on this representation, e.g. evaluation for a given input, minimization, satisfiability, redundancy test, replacement of variables by constants or functions, equivalence test and synthesis. The algorithms have logarithmic run time on CRCW COMMON PRAMs with a polynomial number of processors.

scholarly journals Optimal ordered binary decision diagrams for read-once formulas

2000 ◽  
Vol 103 (1-3) ◽  
pp. 237-258 ◽  
Author(s):  
Martin Sauerhoff ◽  
Ingo Wegener ◽  
Ralph Werchner
Keyword(s):  
Binary Decision Diagrams ◽  
Decision Diagrams ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision

ORDERED BINARY DECISION DIAGRAMS AND THEIR SIGNIFICANCE IN COMPUTER-AIDED DESIGN OF VLSI CIRCUITS

1999 ◽  
Vol 09 (03n04) ◽  
pp. 181-198 ◽  
Author(s):  
CHRISTOPH MEINEL ◽  
THORSTEN THEOBALD
Keyword(s):  
Integrated Circuits ◽  
Computer Aided Design ◽  
Binary Decision Diagrams ◽  
Basic Research ◽  
Vlsi Circuits ◽  
Decision Diagrams ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Computer Aided ◽  
Aided Design

Many problems in computer-aided design of highly integrated circuits (CAD for VLSI) can be transformed to the task of manipulating objects over finite domains. The efficiency of these operations depends substantially on the chosen data structures. In the last years, ordered binary decision diagrams (OBDDs) have proven to be a very efficient data structure in this context. Here, we give a survey on these developments and stress the deep interactions between basic research and practically relevant applied research with its immediate impact on the performance improvement of modern CAD design and verification tools.

Sign in / Sign up

Export Citation Format

Share Document