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
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{http://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.