<p>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:</p>

<pre><code>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)))
</code></pre>

<p>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: <strong>what is the shortest known term that solves an NP-complete problem?</strong></p>

CC BY-SA 3.0
2015-08-11T15:05:51.707Z
1. It depends on how you encode the problem. 2. This looks more like SAT solver code golf.
Huck Bennett
CC BY-SA 3.0
2015-08-13T02:43:15.563Z
The simplest one I know of is $\mu$-recursive: $\mu_x \mu_y (ax^2 + by = c)$.
Kaveh
CC BY-SA 3.0
2015-08-13T03:57:15.383Z
@Kaveh Sorry, could you elaborate? What is that?
MaiaVictor
CC BY-SA 3.0
2015-08-13T03:58:12.183Z
@HuckBennett 1. So what? 2. So what? - read your comment as: "we don't like the problem."
MaiaVictor
CC BY-SA 3.0
2015-08-13T05:26:32.543Z
1. I agree with Huck Bennett that this seems more suitable for [codegolf.se] unless you explain why this is of interest as a theoretical computer science question. 2. Quadratic Diophantine equation problem is NP-complete. My program is not in lambda calculus but in [$\mu$-recursion](https://en.wikipedia.org/wiki/%CE%9C-recursive_function).
Kaveh
<cc.complexity-theory><np-hardness><sat><lambda-calculus>
What is the simplest known solver for a np-complete problem?
MaiaVictor
# What is the simplest known solver for a np-complete problem?

(Asked by: username_0 on 2015-08-11)

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?

**Tags:** cc.complexity-theory, np-hardness, sat, lambda-calculus
> **Comments:**
> **username_1**: 1. It depends on how you encode the problem. 2. This looks more like SAT solver code golf.  
> **username_2**: The simplest one I know of is $\mu$-recursive: $\mu_x \mu_y (ax^2 + by = c)$.  
> **username_0**: @Kaveh Sorry, could you elaborate? What is that?  
> **username_0**: @HuckBennett 1. So what? 2. So what? - read your comment as: "we don't like the problem."  
> **username_2**: 1. I agree with Huck Bennett that this seems more suitable for [codegolf.se] unless you explain why this is of interest as a theoretical computer science question. 2. Quadratic Diophantine equation problem is NP-complete. My program is not in lambda calculus but in [$\mu$-recursion](https://en.wikipedia.org/wiki/%CE%9C-recursive_function).  

---

## 0 answers

