An incremental SAT solving library and its applications

Remarkable improvements on SAT solvers over the last decade have led the success of SAT-based solvers. However, existing SAT-based solvers cannot efficiently solve optimization and enumeration problems since those solvers invoke SAT solvers multiple times from scratch and do not reuse search information such as learnt clauses. Recently, incremental SAT method has been proposed to efficiently solve these problems. In addition, such incremental SAT API is proposed in SAT Race 2015. In this paper, we propose iSAT Library, an extended incremental SAT API, and describe its application. This proposed API allows users to implement SAT-based systems concisely and within Java. We show the effectiveness of using iSAT Library through experimental results on shop-scheduling, N-queens, and Hamiltonian cycle problems.