Stochastic Search For Proofs

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?)

Previous slide

Next slide

Back to the first slide

View Graphic Version