טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentKoifman Maya
SubjectAn Approach to Extracting a Small Unsatisfiable Core
DepartmentDepartment of Quality Assurance and Reliability
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

The thesis addresses the problem of finding a small unsatisfiable core of an unsatisfiable CNF formula. The proposed algorithm, Core Trimmer , iterates over each internal node d in the resolution graph that `consumes' a large number of clauses M (i.e. a large number of original clauses are present in the unsatisfiable core only for proving d) and attempts to prove them without the M clauses. If this is possible, it transforms the resolution graph into a new graph that does not have the M clauses at its core. Core Trimmer can be integrated into a fixpoint framework. Experimental evaluation on a large number of industrial CNF unsatisfiable formulas shows that Core Trimmer in the fixpoint framework doubles, on average , the number of reduced clauses in comparison to existing tools. It is also better when used as a component in a bigger system that enforces short timeouts .