Skip to main content

All Questions

Filter by
Sorted by
Tagged with
16 votes
4 answers
1k views

Representing mathematical statements as SAT instances

The following problem (call it THEOREMS) belongs to class NP. Input: Mathematical statement $S$ (written in some formal system such as ZFC) and positive integer $n$ written in unary. Output: "Yes" if ...