I am writing a poker game, and I got mildly annoyed when I went to write the hand classification functions. There was a disparity between the specification and implementation of poker hands; I had to come up with an algorithm to match each type. I didn’t like this, I want the code to match the specification more directly.

This is quite a geeky post. The types of poker hands are very unlikely to change, and the amount of time I’ve spent thinking about this problem already is many times that of solving it directly in the first place. I.e. it would be stupid for someone to pay me by the hour to solve it this way. Still, it gives rise to an interesting generalization that could be very useful.

I decided that the way I would like to specify these things is with “set selectors” over logical expressions. That is, given a finite set U, find a subset R of U such that some logical expression holds in R (i.e. all quantifiers are bounded on R).

This has a straightforward exponential time solution. I’m trying to do better.

I started by classifying logical expressions. In the following, let *P(…)* be quantifier-free.

- is straightforward .
- More generally, is straightforward .
- is also to find the largest solution (because the empty set would satisfy it, but that’s not very interesting).
- has an obvious solution, same as . There is no unique largest solution, but there is a unique largest for each
*x*which can be found in time. It’s unclear what the library should do in this scenario. - is called the Clique problem and is NP-complete! Damn!

But the most interesting one so far is the case: . It turns out that there is a unique largest solution for this, and here is an algorithm that finds it:

Given a finite set U, find the largest subset R such that .

Let . That is, iteratively remove *x’s* from *r* that don’t have corresponding *y’s*. Then define the result .

**Lemma.** There is a natural number such that .

Proof.Follows from finite U and .

**Theorem.** .

Proof.Given Thus there exists such thatP(x,y), by the definition of .

**Theorem.** If and , then .

Proof.Pick the leastnsuch that . There is an with . The only way that could have happened is if there were noyinrwith_{n-1}P(x,y). But thereisayinR’withP(x,y), so , contradicting n’s minimality.

The time complexity of this algorithm can be made at least as good as , maybe better.

While that was interesting, it doesn’t really help in solving the general problem (which, I remind myself, is related to poker, where all quantifiers will be existential anyway!). The above algorithm generalizes to statements of the form . Each existential before the universal adds an order of magnitude, and *I think* each one after does too, but I haven’t thought it through.

In fact, I think that, because of the clique problem, any statement with two universal quantifiers will take exponential time, which means I’m “done” (in a disappointing sort of way).

Back to the real world, I don’t like that finding a flush in a hand will take time (16,807 checks for a 7-card hand, yikes), when my hand-written algorithm could do it in . I’m still open to ideas for specifying poker hands without the use of set selectors. Any ideas?