|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
2009 21st IEEE International Conference on Tools with Artificial Intelligence
Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness
Newark, New Jersey
November 02-November 04
ISBN: 978-0-7695-3920-1
| ASCII Text | x | ||
| Anbulagan, John Slaney, "Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness," 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, pp. 99-106, 2009 21st IEEE International Conference on Tools with Artificial Intelligence, 2009. | |||
| BibTex | x | ||
| @article{ 10.1109/ICTAI.2009.47, author = { Anbulagan and John Slaney}, title = {Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness}, journal ={2012 IEEE 24th International Conference on Tools with Artificial Intelligence}, volume = {0}, year = {2009}, issn = {1082-3409}, pages = {99-106}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICTAI.2009.47}, 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 - Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness SN - 1082-3409 SP99 EP106 A1 - Anbulagan, A1 - John Slaney, PY - 2009 KW - CNF Simplifier KW - Satisfiability Problem KW - Real-world benchmarks VL - 0 JA - 2012 IEEE 24th International Conference on Tools with Artificial Intelligence ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICTAI.2009.47
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-the-art clause learning and lookahead based SAT solvers when solving both satisfiable and unsatisfiable instances of many real-world hard combinatorial problems.
Index Terms:
CNF Simplifier, Satisfiability Problem, Real-world benchmarks
Citation:
Anbulagan, John Slaney, "Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness," ictai, pp.99-106, 2009 21st IEEE International Conference on Tools with Artificial Intelligence, 2009
Usage of this product signifies your acceptance of the Terms of Use.
