Academic
Publications
Multi-resolution on compressed sets of clauses

Multi-resolution on compressed sets of clauses,10.1109/TAI.2000.889839,IEEE Transactions on Applications and Industry,Philippe Chatalic,Laurent Simon

Multi-resolution on compressed sets of clauses   (Citations: 47)
BibTex | RIS | RefWorks Download
This paper presents a system based on new operators for handling sets of propositional clauses represented by mean s of ZBDDs. The high compression power of such data struc- tures allows efficient encodings of structured instances. A specialized operator for the distribution of sets of clause s is introduced and used for performing multi-resolution on clause sets. Cut eliminations between sets of clauses of ex- ponential size may then be performed using polynomial size data structures. TheZRES system, a new implementation of the Davis-Putnam procedure of 1960, solves two hard prob- lems for resolution, that are currently out of the scope of th e best SAT provers.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...The TRIE representation [4] and clause resolution can be extended to a ZBDD representation and multi-resolution [1, 18]...

    Alexandre Papadopouloset al. Compiling All Possible Conflicts of a CSP

    • ...An internal node can be denoted by Δ(x, n1, n2 ) where x is the label and n1, n2 stand for its two children [7]...
    • ...Fig. 1. The Subsume difference operator (Adopted from [7]) 716 M. Ghasemzadeh and C. Meinel...

    Mohammad Ghasemzadehet al. An Operator for Removal of Subsumed Clauses

    • ...Some solvers employ compact representations for clause sets or sets of assignments, based on BDDs or ZDDs, in the spirit of [31]...

    Marco Benedettiet al. QBF-Based Formal Verification: Experience and Perspectives

    • ...Resolution based solvers have several inherent limitations, the most famous being their need for exponential time to perform simple counting arguments such as “n + 1 objects cannot be placed injectively into n holes” [21, 47, 14, 7, 39, 5]. Motivated by the weaknessses of resolution-based solvers, a number of algorithms for solving Boolean satisfiability using ordered binary decision diagrams have been proposed [10, 46, 19, 12, 13, 1, 36, ...
    • ...These results do not clearly apply to a third class of OBDD-based satisfiability algorithms, “compressed resolution” or “compressed search” techniques [12, 13, 35, 36, 37], as those techniques construct OBDDs in variables different from those of the input CNF...

    Nathan Segerlind. On the Relative Efficiency of Resolution-Like Proofs and Ordered Binar...

    • ...A large number of OBDD-based algorithms have been implemented for solving the Boolean satisfiability problem [6, 42, 18, 10, 11, 1, 34, 33, 2, 14, 36, 22, 3, 24]...
    • ...A well-known example of this method is multiresolution, developed by Chatalic and Simon [10, 11]...
    • ...To the best of our knowledge, no non-trivial size lower bounds are known for any of the compressed methods [10, 11, 33, 34, 35]...

    Nathan Segerlind. Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Eliminati...

Sort by: