TY - GEN
T1 - Towards a generic CNF simplifier for minimising structured problem hardness
AU - Anbulagan,
AU - Slaney, John
PY - 2009
Y1 - 2009
N2 - CNF simplifiers play a very important role in minimising structured problem hardness. Altough they can be used in an in-search process, most of them serve in a pre-search phase and rely on one form or another of resolution. Based on our understanding about problem structure, in the paper, we extend the single pre-search process to a multiple one in order to further simplify the hard structure in a problem. This extension boosts the performance of state-of-theart clause learning and lookahead based SAT solvers when solving both satisfiable and unsatisfiable instances of many real-world hard combinatorial problems.
AB - CNF simplifiers play a very important role in minimising structured problem hardness. Altough they can be used in an in-search process, most of them serve in a pre-search phase and rely on one form or another of resolution. Based on our understanding about problem structure, in the paper, we extend the single pre-search process to a multiple one in order to further simplify the hard structure in a problem. This extension boosts the performance of state-of-theart clause learning and lookahead based SAT solvers when solving both satisfiable and unsatisfiable instances of many real-world hard combinatorial problems.
UR - http://www.scopus.com/inward/record.url?scp=77949499553&partnerID=8YFLogxK
U2 - 10.1109/ICTAI.2009.47
DO - 10.1109/ICTAI.2009.47
M3 - Conference contribution
SN - 9781424456192
T3 - Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI
SP - 99
EP - 106
BT - ICTAI 2009 - 21st IEEE International Conference on Tools with Artificial Intelligence
T2 - 21st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2009
Y2 - 2 November 2009 through 5 November 2009
ER -