|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'00)
Multi-resolution on compressed sets of clauses
Vancouver, British Columbia, Canada
November 13-November 15
ISBN: 0-7695-0909-6
| ASCII Text | x | ||
| P. Chatalic, L. Simon, "Multi-resolution on compressed sets of clauses," 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, pp. 0002, 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'00), 2000. | |||
| BibTex | x | ||
| @article{ 10.1109/TAI.2000.889839, author = {P. Chatalic and L. Simon}, title = {Multi-resolution on compressed sets of clauses}, journal ={2012 IEEE 24th International Conference on Tools with Artificial Intelligence}, volume = {0}, year = {2000}, isbn = {0-7695-0909-6}, pages = {0002}, doi = {http://doi.ieeecomputersociety.org/10.1109/TAI.2000.889839}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2012 IEEE 24th International Conference on Tools with Artificial Intelligence TI - Multi-resolution on compressed sets of clauses SN - 0-7695-0909-6 SP EP A1 - P. Chatalic, A1 - L. Simon, PY - 2000 KW - binary decision diagrams; set theory; theorem proving; data compression; data structures; computational complexity; directed graphs; computability; multi-resolution; compressed sets; compressed clauses; propositional clauses; ZBDDs; compression power; data structures; encodings; structured instances; specialized operator; clause sets; cut eliminations; polynomial size data structures; ZREs system; Davis-Putnam procedure; hard problems; SAT provers; zero-suppressed binary decision diagrams VL - 0 JA - 2012 IEEE 24th International Conference on Tools with Artificial Intelligence ER - | |||
Abstract: The paper presents a system based on new operators for handling sets of propositional clauses represented by means of ZBDDs (zero-suppressed binary decision diagrams). The high compression power of such data structures allows efficient encodings of structured instances. A specialized operator for the distribution of sets of clauses is introduced and used for performing multi-resolution on clause sets. Cut eliminations between sets of clauses of exponential size may then be performed using polynomial size data structures. The ZREs system, a new implementation of the Davis-Putnam procedure (M. Davis and H. Putnam, 1960), solves two hard problems for resolution, that are currently out of the scope of the best SAT provers.
Index Terms:
binary decision diagrams; set theory; theorem proving; data compression; data structures; computational complexity; directed graphs; computability; multi-resolution; compressed sets; compressed clauses; propositional clauses; ZBDDs; compression power; data structures; encodings; structured instances; specialized operator; clause sets; cut eliminations; polynomial size data structures; ZREs system; Davis-Putnam procedure; hard problems; SAT provers; zero-suppressed binary decision diagrams
Citation:
P. Chatalic, L. Simon, "Multi-resolution on compressed sets of clauses," ictai, pp.0002, 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'00), 2000
Usage of this product signifies your acceptance of the Terms of Use.