טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentYadgar Avraham
SubjectSolving All-SAT Problem for Reachability Analysis
DepartmentDepartment of Computer Science
Supervisors Professor Orna Grumberg
Professor Assaf Schuster


Abstract

This work presents a memory-efficient All-SAT engine which, given a propositional formula, returns the set of all the solutions (satisfying assignments) to the formula. The engine is built using elements of modern SAT solvers, including a scheme for learning conflict clauses. Re-discovering solutions that were already found is avoided by a novel stack manipulation method, rather than by adding blocking clauses as in previous All-SAT engines. As a result, the space requirements of a solved instance do not increase when solutions are found, making it as efficient to find the next set of solutions, and 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 SAT-based (no BDDs involved). We suggest a distributed scheme for our All-SAT based reachability algorithm, accelarating computation and reducing space requirements in an efficient way.


We implemented our All-SAT solver and reachability algorithm using the state-of-the-art SAT solver Chaff as a code base. The results show that our stack-based scheme significantly outperforms All-SAT algorithms that use blocking clauses, as measured by the execution time, the memory requirement, and the number of steps performed by the reachability analysis.