Recursive Explore and Check Abstraction Refinement (RECAR)

VCLA hosted a talk by Daniel Le Berre

ABSTRACT

Since two decades now, the use of SAT solvers to decide problems of practical interest kept growing, since its success in planning and bounded model checking. The practical success of SAT solvers is their « adaptability » to the problem to solve: SAT solvers have become generic problem solvers for many people. There are however cases in which the translation of the original problem into a CNF is not practically possible due to space explosion. In that case, it is often the case that the full CNF is not generated upfront but incrementally derived guided by the feedback of the SAT solver (so called Counter Example Guided Abstraction Refinement, CEGAR). Space explosion especially occurs when dealing with PSPACE problems. We propose a generic framework called RECAR (Recursive Explore and Check Abstraction Refinement) to cope with structured problems which can be decided by focussing to a subproblem. Similar to CEGAR, the focus is guided by the solver, but at the original domain level. While the procedure is generic, the implementation has to be tailored for each problem. We present some results obtained while tackling modal logic K satisfiability problem.

Daniel Le Berre