Lazy Decomposition for Distributed Decision Procedures

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


PDF file

In  Proceedings of the 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'11)

Publisher  Electronic Proceedings in Theoretical Computer Science


> Publications > Lazy Decomposition for Distributed Decision Procedures