Approach to orchard problem (A003035)

[Rob Arthan]

On Wednesday 01 Mar 2006 5:54 pm, David Wilson wrote:
> Could instances of the orchard problem be decided via Pressburger
> arithmetic or some decidable real number theory?

The existence of a solution to the problem for n trees and r rows says that 
there is a configuration of r line segments in the plane which intersect in a 
certain way. Spelled out in coordinate terms, this gives a formula in the 
theory of the real numbers (as an ordered field), which is a decidable 
theory. As there is a known upper bound on r for each n (see the mathworld 
web page on the problem), there are only a finite number of formulae you need 
to try.

>  Is there software out
> there for decidable theories?

If you knew in advance what the end-points of the line segments were, the 
formulae would reduce to logical combinations of linear constraints and you 
could use a linear programming method. Unfortunately you don't know what the 
end-points are, and I don't think this applies.

Some automated theorem-proving systems, e.g., HOL Light, include decision 
procedures which cover this class of problem, but I don't know whether they'd 
be able to cope with the quite large formulae you are going to get. One of 
John Harrison's approaches in HOL Light uses an external semi-definite 
programming package to suggest solutions, and it may be that you could use 
such a thing directly.

>  Is it practical?

I don't know!

Regards,

Rob.