The Taub Faculty of Computer Science Events and Talks

The majority of SAT solving applications are incremental in nature, i.e., instead of solving a single formula, a sequence of (syntactically) similar formulas are solved. In most cases the elements of the sequence are generated one after another at runtime, without a-priori knowledge of future instances. It is possible to accelerate the SAT search by using information gained from solving previous instances. Until recently, such information has been limited to sharing relevant learned clauses, as well as heuristic scores such as activity and weights. A new kind of information sharing, proposed in SAT'15 with a technique called Mining of Backbone Literals (MBL), can be used to further shorten the runtime for solving future formulas. MBL extracts backbone literals for the current formula by analyzing resolution proofs generated during the solving of previous instances in the sequence of formulas. This work starts by proposing a solution to a known open issue generally encountered in backbone literal extraction; using an increasing number of backbone literals is detrimental to further extraction of more such literals - meaning there exists a negative feedback loop regarding mining of backbone literals. Having proposed a solution that tackles this open problem, we go on to describe how to extend MBL in order to develop a new SMT-like architecture, which more thoroughly leverages knowledge gained by previous SAT solving iterations.