Automated benchmarking of incremental SAT and QBF solvers

DOI10.1007/978-3-662-48899-7_13zbMATH Open1471.68306arXiv1506.08563OpenAlexW3099535388MaRDI QIDQ3460052FDOQ3460052

Authors: Uwe Egly, Florian Lonsing, Johannes Oetsch 

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Abstract: Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers. Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program. We illustrate our approach by different hardware verification problems for SAT and QBF solvers.

Full work available at URL: https://arxiv.org/abs/1506.08563

Recommendations

• Verification of partial designs using incremental QBF
• Incremental QBF solving by DepQBF
• Ultimately incremental SAT
• Conformant planning as a case study of incremental QBF solving
• Theory and Applications of Satisfiability Testing

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (6)

• Verification of partial designs using incremental QBF
• Conformant planning as a case study of incremental QBF solving
• SAT race 2015
• Automated testing and debugging of SAT and QBF solvers
• SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
• Itauto: An Extensible Intuitionistic SAT Solver

This page was built for publication: Automated benchmarking of incremental SAT and QBF solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460052)