+++
title = "SAT Solvers"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2d"]
forwardlinks = ["2d2"]
zettelid = "2d1"
+++

SAT is a mathematical problem whereby the question is asked whether a
logical formula is satisfiable, meaning there is a combination of inputs
that will satisfy the sentence. This logical formula is often expressed
in conjunctive normal form (CNF).

SAT solvers are programs that can solve these problems automatically.
Even though it is an intractable problem and is in O(2^n^) for the
number of variables present in the sentence, there are efficient
algorithms that will work well most of the time.