Sciweavers

SAT
2015
Springer

Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data

7 years 11 months ago
Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data
Abstract. In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores. In most settings in which incremental satisfiability is applied, many of the instances along the sequence of formulas being solved are unsatisfiable. We show that in such cases, with a P-time analysis of the proof, we can compute a set of literals that are logically implied by the next instance. By adding those literals as assumptions, we accelerate the search.
Alexander Ivrii, Vadim Ryvchin, Ofer Strichman
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAT
Authors Alexander Ivrii, Vadim Ryvchin, Ofer Strichman
Comments (0)