Lazy Decomposition for Distributed Decision Procedures

TL;DR

This paper introduces a lazy distributed decision procedure framework for first-order logic problems using Craig interpolation, which outperforms traditional methods on challenging SAT problems without extra resources.

Contribution

It proposes a novel lazy distribution approach for decision procedures based on Craig interpolation, avoiding costly decomposition algorithms.

Findings

Outperforms traditional SAT solving techniques on challenging problems

Effective reconciliation of potential models using Craig interpolants

Operates efficiently without additional computational resources

Abstract

The increasing popularity of automated tools for software and hardware verification puts ever increasing demands on the underlying decision procedures. This paper presents a framework for distributed decision procedures (for first-order problems) based on Craig interpolation. Formulas are distributed in a lazy fashion, i.e., without the use of costly decomposition algorithms. Potential models which are shown to be incorrect are reconciled through the use of Craig interpolants. Experimental results on challenging propositional satisfiability problems indicate that our method is able to outperform traditional solving techniques even without the use of additional resources.