# Converting Mathematical Statements to SAT Formulas

Is it possible to write a mathematical statement (like Goldbach's conjecture, for example) as a nontrivial 3-SAT formula that is satisfiable iff that statement is true? iff it is false? iff it is independent of the axioms of ZFC? So, for any statement, you would have (at most) 3 formulas, for which only one can be satisfiable. Is there any work in this field (you can use the Pythagorean Theorem as a more simpler example)?

If you want to know whether there exists a general method/algorithm which can convert any given mathematical statement (by which you mean statements written in logic (say first-order logic, second-order logic ... etc)) to a SAT formula which is True iff that statement is True, then the answer is No.

The reason being that evaluating whether an SAT formula is true or false is decidable (in exponential time if not faster), whereas these logics are usually undecidable. So, no such algorithm can exist.

Of course, there are logics which are decidable, and the statement of those logic can be converted to SAT formula (maybe trivial ones like True or False as mentioned by @D.W) by a specific algorithm. See: http://www.lsv.fr/~haase/documents/h18.pdf

• No, what I mean is that can you make a SAT formula that is satisfiable iff the statement is true or make a formula that is satisfiable iff the statement is false or a formula that is satisfiable iff the statement is undecidable (or independent). So, for any decision statement, there would be (at most) 3 formulas, and only one could be true (I think). – Quote Dave May 15 at 20:52
• What do you mean by make? Does make means a general algorithm for this conversion? If yes, then the answer given above applies. If not, then you need to clarify this term. – prime_hit May 15 at 20:54
• Oh, right, sorry. I guess you deserve a +1 from me (though I'm going to hold off of the checkmark until some time later). – Quote Dave May 15 at 21:32
• Though could you give an example of converting a statement in a decidable logic to a nontrivial SAT formula? Just to get an idea about how it works? – Quote Dave May 16 at 20:26
• Formal Verification (en.wikipedia.org/wiki/Formal_verification) usually involves automated verification of algorithms. It indeed involves writing the algorithm in a decidable logic (en.wikipedia.org/wiki/Satisfiability_modulo_theories) and then converting it SAT formulas using algorithms like DPLL(T) etc. The formula are completely non-trivial and this is used in practice too. I will encourage you to explore this field if it interests you. See also: decision-procedures.org – prime_hit May 16 at 20:53

It depends on the mathematical statement. If it has the form

$$\exists x_1 \in S_1 \cdots \exists x_n \in S_n . \varphi(x_1,\dots,x_n)$$

where $$\varphi(x_1,\dots,x_n)$$ is some condition on $$x_1,\dots,x_n$$ and $$S_1,\dots,S_n$$ are finite sets, then yes, it can be expressed as a 3CNF formula in a straightforward way.

However, statements like $$\exists x \in S_1 \forall y \in S_2 . \varphi(x,y)$$ or $$\exists x_1 \in \mathbb{R} \cdots \exists x_n \in \mathbb{R} . \varphi(x_1,\dots,x_n)$$ are harder.

There is a trivial sense in which the answer is yes: every mathematical statement is either true or false, so it corresponds to either the 3CNF formula $$\text{True}$$ (i.e., $$(x_1 \lor \neg x_1)$$) or the 3CNF formula $$\text{False}$$ (i.e., $$(x_1) \land (\neg x_1)$$). This reduction is nonconstructive and might not be computable, though.

You might be interested in https://en.wikipedia.org/wiki/Existential_theory_of_the_reals.

Undecidable is a property of languages, not of mathematical statements. Perhaps you mean "independent of the axioms of ZFC".