Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction

Abstract. Beside the important progresses observed in SAT solving, a number of applications explicitly rely on incremental SAT solving only. In this paper, we focus on refining the incremental SAT Solver Glucose, from the SAT en-gine perspective, and address a number of unseen problems this new use of SAT solvers opened. By playing on clause database cleaning, assumptions manage-ments and other classical parameters, we show that our approach immediately and significantly improves an intensive assumption-based incremental SAT solv-ing task: Minimal Unsatisfiable Set. We believe this work could bring immediate benefits in a number of other applications relying on incremental SAT.