Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I do a lot of research about squares, and I thought of using some automatic tool for proving / disproving some geometric conjectures.

As a simple example, consider the following Square coloring question:

There are 3 red squares and 3 blue squares.
All squares are axis-parallel.
All squares of the same color are interior-disjoint.
CONJECTURE: There always exists a red square and a blue square
    that are interior-disjoint.

Altough Abel already proved that the conjecture is true, I wanted to check if this can be proved automatically.

For this experiment I used Minion - a state-of-the-art solver for constraint-satisfaction problems. I started with a simpler problem, where there are only 2 red squares and 3 blue squares. I asked Minion to find a counter-example to the conjecture, i.e., find an arrangement of squares such that every square intersects all squares of the other color. Here is an abbreviated version of my Minion program:

**VARIABLES**
// There are 2 red squares and 3 blue squares.
// for every square, x and y are the south-west corner, and s is the side-length:
DISCRETE xred[2] {1..10}
DISCRETE yred[2] {1..10}
DISCRETE sred[2] {1..10}

DISCRETE xblu[3] {1..10}
DISCRETE yblu[3] {1..10}
DISCRETE sblu[3] {1..10}

**CONSTRAINTS**
//(Here I defined the macros "disjoint" and "intersect"; details skipped)

// Squares of the same color must be disjoint:
disjoint(red[0],red[1])
disjoint(blu[0],blu[1])
disjoint(blu[0],blu[2])
disjoint(blu[2],blu[1])

// Squares of the different colors must intersect:
intersect(red[0],blu[0])
intersect(red[0],blu[1])
intersect(red[0],blu[2])
intersect(red[1],blu[0])
intersect(red[1],blu[1])
intersect(red[1],blu[2])

I ran Minion and it returned in no time with the following nice counter-example:

enter image description here

Then I added a third red square to the program, with the relevant constraints, and ran Minion again. After 7 hours it returned saying that - as we already know - there is no solution, i.e., no counter-example.

Is this answer a sufficient proof that the conjecture is true? Probably not:

  • First, the CSP solver checked x, y and s that are integers from 1 to 10, but there are infinitely many other values.
  • Additionally, there is no formal proof that the CSP solver itself is correct. There may be a bug that prevents it from finding an existing counter-example.

So my question is: Is there a way to use an automatic program in order to prove the above conjecture (and similar such conjectures)? Is this realistic to expect a state-of-the-art automatic prover to prove such a conjecture? If so, what is the right tool for that task?

share|improve this question
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.