Integration of Supercubing and Learning in a SAT Solver
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{babic-hu-aspdac2005,
author = {Domagoj Babi\'{c} and Alan J. Hu},
title = {{Integration of supercubing and learning in a SAT solver}},
booktitle = {ASP-DAC'05: Proceedings of the 2005 conference on Asia
South Pacific design automation},
year = {2005},
pages = {438--444},
publisher = {ACM},
address = {New York, NY, USA},
isbn = {0-7803-8737-6},
location = {Shanghai, China},
doi = {http://doi.acm.org/10.1145/1120725.1120908},
}
Abstract:
Learning is an essential pruning technique
in modern SAT solvers, but it exploits a relatively
small amount of information that can be deduced
from the conflicts. Recently a new pruning
technique called supercubing was proposed [1]. Supercubing
can exploit functional symmetries that are
abundant in industrial SAT instances. We point out
the significant difficulties of integrating supercubing
with learning and propose solutions. Our experimental
solver is the first supercubing-based solver with
performance comparable to leading edge solvers.