An Incremental Simplex Algorithm with Unsatisfiable Core Generation (Q7361924)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Simplex
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | An Incremental Simplex Algorithm with Unsatisfiable Core Generation |
AFP entry Simplex |
Statements
24 August 2018
0 references
Filip Marić
0 references
Mirko Spasić
0 references
René Thiemann
0 references
An Incremental Simplex Algorithm with Unsatisfiable Core Generation (English)
0 references
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.
0 references
