Lets define the simpler of two terms as the one with shortest description length on the untyped λ-calculus. Trying to find the simplest solver for a np-complete problem, I've got this:
solve_sat = (λab.(a(λcde.(c(λf.(d(λgh.(g(λij.j)(fgh))))) (c(λf.(d(λgh.(g(λij.i)(fgh)))))e)))(λcd.(c(λef.f)d)) (λcd.(c(λefg.(f(ge)))(λe.e)b(c(λefg.(f(ge)))(λe.e)b) d))(λcd.d)))
This λ-term takes 2 arguments, a church number telling the arity of a church-encoded boolean formula, and the formula itself, and returns "true" if it is satisfiable. Of course, this term is quite long, but serves as an upper ceiling. My question is: what is the shortest known term that solves an NP-complete problem?