# An Incremental Simplex Algorithm with Unsatisfiable Core Generation

 Title: An Incremental Simplex Algorithm with Unsatisfiable Core Generation Authors: Filip Marić (filip /at/ matf /dot/ bg /dot/ ac /dot/ rs), Mirko Spasić (mirko /at/ matf /dot/ bg /dot/ ac /dot/ rs) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) Submission date: 2018-08-24 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{https://isa-afp.org/entries/Simplex.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Farkas Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.