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
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;
Conference_Titel :
Tools with Artificial Intelligence (ICTAI), 2012 IEEE 24th International Conference on
Conference_Location :
Athens
Print_ISBN :
978-1-4799-0227-9
DOI :
10.1109/ICTAI.2012.145
