Ordered Binary Decision Diagrams and the Davis-Putnam Procedure
作者： Tomás E. Uribe , Mark E. Stickel
DOI: 10.1007/BFB0016843
关键词: Structure (mathematical logic) 、 Binary decision diagram 、 Discrete mathematics 、 Functional equivalence 、 Boolean function 、 Propositional calculus 、 Domain (software engineering) 、 Boolean satisfiability problem 、 Theoretical computer science 、 Computer science 、 Constraint logic programming
摘要: We compare two prominent decision procedures for propositional logic: Ordered Binary Decision Diagrams (Obdds) and the Davis-Putnam procedure. Experimental results indicate that procedure outperforms Obdds in hard constraint-satisfaction problems, while are clearly superior Boolean functional equivalence problems from circuit domain, and, general, require schematization of a large number solutions share common structure. The methods illustrate different often complementary strengths constraint-oriented search-oriented procedures.
springer.com
sci-hub.se 参考文章(36)
Antoine Rauzy, Notes on the design of an open Boolean solver international conference on logic programming. pp. 354- 368 ,(1994)
John Slaney, Frank Bennett, Masayuki Fujita, Automatic generation of some results in finite algebra international joint conference on artificial intelligence. pp. 52- 57 ,(1993)
Sakthikumar Subramanian, A mechanized framework for specifying problem domains and verifying plans University of Texas at Austin. ,(1993)
H. Simonis, M. Dincbas, Propositional calculus problems in CHIP Proceedings of the Second International Conference on Algebraic and Logic Programming. pp. 269- 285 ,(1993) , 10.1007/3-540-53162-9_39
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Thierry Boy de la Tour, Gilles Chaminade, The Use of Renaming to Improve the Efficiency of Clausal Theorem Proving artificial intelligence: methodology, systems, applications. pp. 3- 12 ,(1990) , 10.1016/B978-0-444-88771-9.50007-6
Larry D. Auton, James M. Crawford, Experimental results on the crossover point in satisfiability problems national conference on artificial intelligence. pp. 21- 27 ,(1993)
Frédéric Benhamou, Alain Colmerauer, Constraint logic programming: selected research MIT Press. ,(1993)
Edmund M. Clarke, David Esley Long, Model checking, abstraction, and compositional verification Carnegie Mellon University. ,(1993)
M. Fujita, P.C. McGeer, J.C.-Y. Yang, Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation formal methods. ,vol. 10, pp. 149- 169 ,(1997) , 10.1023/A:1008647823331