Abstract
We propose a notion of hints, clauses that are not necessarily consistent with the input formula. The goal of adding hints is to speed up the SAT solving process. For this purpose, we provide an efficient general mechanism for hint addition and removal. When a hint is determined to be inconsistent, a hint-based partial resolution-graph of an unsatisfiable core is used to reduce the search space. The suggested mechanism is used to boost performance by adding generated hints to the input formula. We describe two specific hint-suggestion methods, one of which increases performance by 30% on satisfiable SAT’13 competition instances and solves 9 instances not solved by the baseline solver.
Cite
CITATION STYLE
Kalechstain, J., Ryvchin, V., & Dershowitz, N. (2015). Hints revealed. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9340, pp. 71–87). Springer Verlag. https://doi.org/10.1007/978-3-319-24318-4_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
