cl-banner

An Incremental Simplex Algorithm with Unsatisfiable Core Generation

Filip Marić, Mirko Spasić, René Thiemann

Archive of Formal Proofs 2018.

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 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

BibTeX 

@article{Simplex-AFP,
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{http://isa-afp.org/entries/Simplex.html}, Formal proof development},
ISSN = {2150-914x},
}
Nach oben scrollen