DocumentCode
1906355
Title
Extending Resolution by Dynamic Substitution of Boolean Functions
Author
Jabbour, Said ; Lonlac, Jerry ; Sais, Lakhdar
Author_Institution
CRIL, Univ. Lille-Nord de France, Lens, France
Volume
1
fYear
2012
fDate
7-9 Nov. 2012
Firstpage
1029
Lastpage
1034
Abstract
This paper presents a dynamic substitution technique of Boolean functions. It first recovers a set of Boolean functions from Boolean formula in conjunctive normal form (CNF). Then these functions are used to reduce the size of the learnt clauses by substituting the input arguments by the output ones. Preliminary experiments show the feasibility of our approach on some classes of SAT instances taken from the recent SAT Race and competitions.
Keywords
Boolean functions; computability; Boolean formula; Boolean functions; CNF; SAT competitions; SAT instances; SAT race; conjunctive normal form; dynamic substitution technique; input arguments; resolution extension; Boolean functions; Cognition; Databases; Encoding; Input variables; Semantics; Standards;
fLanguage
English
Publisher
ieee
Conference_Titel
Tools with Artificial Intelligence (ICTAI), 2012 IEEE 24th International Conference on
Conference_Location
Athens
ISSN
1082-3409
Print_ISBN
978-1-4799-0227-9
Type
conf
DOI
10.1109/ICTAI.2012.145
Filename
6495161
Link To Document