Abstract: |
We present an Isabelle/HOL formalization and total correctness proof
for the incremental version of the Simplex algorithm which is used in
most state-of-the-art SMT solvers. It supports extraction of
satisfying assignments, extraction of minimal unsatisfiable cores, incremental
assertion of constraints and backtracking. The formalization relies on
stepwise program refinement, starting from a simple specification,
going through a number of refinement steps, and ending up in a fully
executable functional implementation. Symmetries present in the
algorithm are handled with special care. |
BibTeX: |
@article{Simplex-AFP,
author = {Filip Marić and Mirko Spasić and René Thiemann},
title = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation},
journal = {Archive of Formal Proofs},
month = aug,
year = 2018,
note = {\url{http://isa-afp.org/entries/Simplex.html},
Formal proof development},
ISSN = {2150-914x},
}
|