loading...
 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," Tools with Artificial Intelligence, IEEE International Conference on, 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 ={Tools with Artificial Intelligence, IEEE International Conference on},
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 - Tools with Artificial Intelligence, IEEE International Conference on
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 - Tools with Artificial Intelligence, IEEE International Conference on
ER -
 
P. Chatalic, Lab. de Recherche en Inf., Univ. de Paris-Sud, Orsay, France
L. Simon, Lab. de Recherche en Inf., Univ. de Paris-Sud, Orsay, France
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.