Средство доказательства геометрических теорем с поддержкой пересечения квадратов

Я пытаюсь автоматически доказать/опровергнуть некоторые теоремы геометрии, связанные с квадратами, такие как «Для каждых 3 наборов из 7 непересекающихся квадратов можно выбрать 1 квадрат из каждого набора, так что 3 представителя являются внутренними непересекающимися?».

Я попытался использовать OpenGeoProver и получил следующее описание квадрата:

    <!-- define a 'free' point - the south-western corner of the square: -->
    <pfree       label="square1southwest"/>

    <!-- define a line that is parallel to the x axis and goes throught that point - the southern boundary: -->
    <lparallel   label="square1south" point="square1southwest" baseline="xaxis" />

    <!-- define a random point on the southern line, which will be the south-eastern corner: -->
    <prandline   label="square1southeast" line="square1south" />

    <!-- rotate the south-eastern corner 90 degrees around the south-western corner, to create the north-western corner: -->
    <protated    label="square1northwest" origpt="square1southeast" center="square1southwest" angmeasure="-90"/>

    <!-- translate the north-western corner by the vector between the two southern corners, to create the north-eastern corner of the square: -->
    <ptranslated label="square1northeast" origpt="square1northwest" point1="square1southwest" point2="square1southeast"/>

Вот где я застрял: как определить простое утверждение «квадрат A и квадрат B пересекаются»?

Как можно решить эту проблему в Z3?


geometry computational-geometry z3 theorem-proving
person Erel Segal-Halevi    schedule 21.01.2014    source источник
comment
Я думаю, что это не по теме SE, потому что это рекомендация по покупкам .   -  person Palec    schedule 21.01.2014
comment
Этот вопрос кажется не по теме, потому что он касается математики.   -  person Rowland Shaw    schedule 21.01.2014
comment
Описываю проблему и то, что уже сделано для ее решения. Можно ли открыть заново?   -  person Erel Segal-Halevi    schedule 21.01.2014

Ответы (2)


arrow_upward
2
arrow_downward

Я попытался опровергнуть вашу теорему, используя MiniZinc:

int: noOfCollections = 3;
int: noOfDisjoints = 7;
int: noOfSquares = noOfCollections * noOfDisjoints;
set of int: Squares = 1..noOfSquares;
int: maxDim = 10000;  %  somewhat arbitrary limit!
int: maxLeft = maxDim;
int: maxRight = maxDim;
int: maxTop = maxDim;
int: maxBottom = maxDim;
int: maxHeight = maxBottom - 1;
int: maxWidth = maxRight - 1;

array[Squares] of var 1..maxLeft: Left;
array[Squares] of var 1..maxTop: Top;
array[Squares] of var 1..maxHeight: Height;
array[Squares] of var 1..maxWidth: Width;
array[Squares] of var bool: Representative;
array[Squares] of 1..noOfCollections: 
      Collection = [1 + (s mod noOfCollections) | s in Squares];

%  Squares must fit in the overall frame
constraint
    forall(s in Squares)(
        (Left[s] + Width[s] - 1 <= maxRight) /\
        (Top[s] + Height[s] - 1 <= maxBottom)
    );

predicate disjoint(var int: s1, var int: s2) =
    (Left[s1] + Width[s1] - 1 < Left[s2]) \/
    (Left[s2] + Width[s2] - 1 < Left[s1]) \/
    (Top[s1] + Height[s1] - 1 < Top[s2]) \/
    (Top[s2] + Height[s2] - 1 < Top[s1]);

%  Squares in a collection must be disjoint
constraint
    forall(s1 in Squares, s2 in Squares 
           where (s1 > s2) /\ (Collection[s1] == Collection[s2]))(
        disjoint(s1, s2)
    );

%   Exactly one Representative per Collection
constraint
    1 == sum(c in 1..noOfCollections, s in Squares 
             where c == 1 + (s mod noOfCollections))
           (bool2int(Representative[s]));

%   Is it possible to select 1 square from each collection such 
%   that the 3 representatives are interior disjoint?
constraint
    forall(s1 in Squares, s2 in Squares, s3 in Squares
           where (Collection[s1] == 1) /\
                 (Collection[s2] == 2) /\
                 (Collection[s3] == 3))(
        disjoint(s1, s2) /\
        disjoint(s1, s3) /\
        disjoint(s2, s3) /\
        Representative[s1] /\
        Representative[s2] /\
        Representative[s3]
    );

solve satisfy;

MiniZinc выдает «UNSAT» через 45 мс.

person Axel Kemper    schedule 25.02.2014

arrow_upward
0
arrow_downward

Я единственный, кто видит в этом алгоритмическую проблему?

  • да, заголовок и начало вопроса немного сбивают с толку, но
  • насколько я понимаю, вопрос заключается (или должен быть) в том, как добиться доказательства утверждения геометрии.
  • Я думаю, что для этого будет полезно некоторое повторное редактирование / повторное тегирование

Я бы сделал это так (не буду использовать какой-либо язык или фреймворк, потому что это не имеет значения):

1.определение набора данных

  • сумма/размер/количество геометрических объектов, используемых в теореме (точки, линии, прямоугольники,...)
  • сумма всех условий/ограничений для входных данных

2.генерация набора данных

  • может быть случайным + отбрасывать недопустимые объекты (которые не соответствуют 1)
  • или вы можете сгенерировать все допустимые возможности с некоторой точностью для положения/размера...

  • но это действительно противно из-за временной и пространственной сложности

  • это сложная часть

  • вы должны выбрать между производительностью/релевантностью
  • Боюсь, что эту задачу нельзя автоматизировать с удовлетворительной производительностью
  • вместо этого вам нужно написать сценарий генерации для каждой теоремы

3. утверждение теоремы

  • это самая легкая часть
  • просто проверьте, верна ли теорема для текущего набора данных
  • если нет теорема недействительна
  • если набор данных является случайным, используйте достаточно большое количество тестов...

У вас возникла проблема с утверждением "квадрат A и квадрат B пересекаются"

  • Я предполагаю, что вы заявили об этом после создания набора данных
  • это просто еще одно условие для пули 1
  • поэтому ваш генератор набора данных должен генерировать пересекающиеся квадраты A, B
  • A - генерировать как есть

  • поместите B - начальную точку внутри A (случайно или посередине или что-то еще)

  • другой вариант - выбрать только пересекающиеся квадраты из набора данных

  • пройти через все i=1..N квадраты (A)
  • затем пройдите i+1..N квадратов, и если они пересекаются, то это ваш квадрат B

надеюсь, я не слишком далек от того, что вы хотели сделать...

person Spektre    schedule 25.02.2014
comment
Ваше предложение создать случайный набор данных и проверить, верна ли теорема, на самом деле очень хорошо подходит для опровержения теорем. Я использовал его много раз, чтобы найти нетривиальные контрпримеры к теоремам. Но чтобы доказать теорему, нужно проверить все возможные случаи, что может быть невозможно, потому что количество различных квадратов бесконечно... - person Erel Segal-Halevi; 25.02.2014
comment
да ... поэтому вы можете моделировать бесконечные возможности только с помощью некоторой сетки точности для размеров и позиций ... или делать некоторые неприятные эвристики ограничений теоремы и генерировать только те случаи, которые имеют значение - person Spektre; 25.02.2014