Stochastic Search For Proofs
GSAT: start with random truth assignment (size linear in N), and try to “fix” it.
Proposal for UNSAT: start with random proof structure, and try to fix it.
Completely unfeasible if the structure that we’re fixing has trillions of nodes (exponential in N).
We need short proofs! (O(N) or something...) (Using abstractions / symmetrries?)