Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Hints Revealed
verfasst von : Jonathan Kalechstain, Vadim Ryvchin, Nachum Dershowitz
Erschienen in: Theory and Applications of Satisfiability Testing -- SAT 2015
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.