Some Challenges
Fast incomplete strategies for UNSAT (deduction)?
Need for short proofs. Human proofs O(N)? Need automatic discovery of abstractions, symmetries, useful lemmas...
Need for more model-based reformulations:
Where solutions are compact structures --- allowing for randomized local search strategies.
Can we syntactically characterize the class of instances solved by incomplete, stochastic methods? Running algorithm may be the best and only characterization!