An Incremental Simplex Algorithm with Unsatisfiable Core Generation

Filip Marić, Mirko Spasić, René Thiemann

Archive of Formal Proofs 2018.


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 unsatisfiable cores, incremental assertion of constraints and backtracking. 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 implementa-tion. Symmetries present in the algorithm are handled with special care.


   AFP entry


author = {Filip Mari\'c and Mirko Spasi\'c and Ren\'e Thiemann},
title = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation},
journal = {Archive of Formal Proofs},
month = aug,
year = 2018,
note = {\url{}, Formal proof development},
ISSN = {2150-914x},
Nach oben scrollen