Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic

TL;DR

This paper explores methods for proving unsatisfiability in SMT problems involving quantifier-free non-linear real arithmetic, highlighting challenges and potential new local search algorithms to improve proof techniques.

Contribution

It analyzes the limitations of existing formal methods and suggests that local search algorithms could provide a more effective approach for this domain.

Findings

Traditional formal proofs are complex and not straightforward.

Past formalisation attempts are insufficient for this domain.

Local search algorithms may offer a promising new direction.

Abstract

We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit trivial proofs and how past formalisation attempts are not sufficient. We note that the new breed of local search based algorithms for this domain may offer an easier path forward.