+++
title = "Verifying the decidability of SAT"
date = "2023-04-28"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3k"]
forwardlinks = ["3c3m", "3c3l1"]
zettelid = "3c3l"
+++

One proof that is necessary for the current scheduling proof development
is the proof that SAT is decidable, meaning a proof that the algorithm
terminates in a definite answer. This allows for various simplifications
in the proof itself, such as being able to define an equivalence
relation around semantic equivalence of formulas. These can then
drastically simplify the proofs themselves.