Sciweavers

FMCAD
2004
Springer

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

14 years 2 months ago
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...
Orna Grumberg, Assaf Schuster, Avi Yadgar
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where FMCAD
Authors Orna Grumberg, Assaf Schuster, Avi Yadgar
Comments (0)