# FOM: Axiomatizing plane geometry - a notion of convexity?

Sat Dec 30 05:18:43 EST 2000

```Hi all,

I've got a simple problem - I want to 'encode' a set of points in the
plane in a format suitable for input to a SAT (satisfiability) solver - in
my case, I've got AND, OR, NOT, -> (implies), <-> (bi-implies) ()
(bracketing!) and boolean variables.

I've got the guarantee that moving along the set of points, one _always_
turns left or right - another way of saying this is that no three of the
points are collinear.

Now I know that there are only so many configurations of n points in the
plane (proportional to 2^n, I suspect?) - I'm guessing (hoping) the number
of boolean variables I'll need is proportional to n by some constant
factor. At any rate, what I'm *really* wondering is:

Can anyone think of a way of forming a proposition using the operations
I've listed above such that given some _assignment_ of {0,1} to the
variables (thus describing some configuration of n points in the plane),
the proposition will be true if and only if the points can form a convex
m-gon? Obviously if m=3 the propositions formed will always be true, and if
m>n they'll never be true.