Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis

This work presents a memory-efficient All-SAT engine which, given a propositional formula over sets of important and non-important variables, returns the set of all the assignments to the important variables, which can be extended to solutions (satisfying assignments) to the formula. The engine is built using elements of modern SAT solvers, including a scheme for learning conflict clauses and non-chronological backtracking. Re-discovering solutions that were already found is avoided by the search algorithm itself, rather than by adding blocking clauses. As a result, the space requirements of a solved instance do not increase when solutions are found. Finding the next solution is as efficient as finding the first one, making it possible to solve instances for which the number of solutions is larger than the size of the main memory. We show how to exploit our All-SAT engine for performing image computation and use it as a basic block in achieving full reachability which is purely SATbase...

• Type: Conference
• Year: 2004
• Where: FMCAD
• Authors: Orna Grumberg, Assaf Schuster, Avi Yadgar
• Keywords: All-SAT Engine, FMCAD 2004, Formal Methods, Sat Solver, Solutions