This paper addresses the interaction between randomization, with restart strategies, andl earning, an often crucial technique for proving unsatisfiability. We use instances of SAT from the hardware verification domain to provide evidence that randomization can indeed be essential in solving real-worldsat isfiable instances of SAT. More interestingly, our results indicate that randomized restarts and learning may cooperate in proving both satisfiability andu nsatisfiability. Finally, we utilize and expand the idea of algorithm portfolio design to propose an alternative approach for solving harduns atisfiable instances of SAT.
CITATION STYLE
Baptista, L., & Marques-Silva, J. (2000). Using randomization and learning to solve hard real-world instances of satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1894, pp. 489–494). Springer Verlag. https://doi.org/10.1007/3-540-45349-0_36
Mendeley helps you to discover research relevant for your work.