QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers

Description

This paper introduces QuAPI, an easy to use library for enabling efficient assumption-based reasoning for arbitrary SAT or QBF solvers. The users of QuAPI only need access to an executable of these solvers. The only requirement on the solvers is to use standard C library functions, either wrapped or directly, for reading input files in the standard DIMACS or QDIMACS format. No source code or library access is necessary, also not for API-less solvers. Our library allows applications to benefit from assumptions and thus incremental solving matching the native support of a standard incremental interface such as IPASIR, but without the need to implement it. This feature is particularly valuable for applications of QBF solving as most state-of-the-art solvers do not support assumption-based reasoning, with some not providing any API at all. We present the architecture of QuAPI and discuss crucial implementation details in depth. Our extensive performance evaluation shows substantial speedup compared to using unmodified solver binaries on similar incremental reasoning tasks.

Period	14 Sept 2022
Event title	14th Alpine Verification Meeting
Event type	Conference
Location	GermanyShow on map