支持正方形交叉的幾何定理證明器

Question

我試圖自動地證明/反駁一些與正方形相關的幾何定理，如「對於7個不相交正方形的每3個集合，可以從每個集合中選擇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中如何解決這個問題？

Answer 1

我是唯一一個將此視爲算法問題的人嗎？

• 是標題和問題的開始是有點混亂，但
• 我明白的問題是（或應該是）如何實現證明幾何聲明。
• 一些重新編輯/重新標籤，將有利於它，我覺得

我會做這樣的（不會使用任何語言或框架，因爲它是不相關的）：

1 .dataset定義

• 總和/大小/計數用於定理幾何實體（點，線，rects，...）
• 總和的全部條件/約束爲輸入數據

2.dataset代

• 可隨機+扔掉無效的實體（不匹配1）
• 或可以將部分精度位置/尺寸範圍內產生的所有有效的可能性...

• 但那是因爲時間和空間複雜度真是可惡

• 這是最困難的部分

• 必須表現/意義之間選擇
• 恐怕這個任務不能表現令人滿意自動化
• 相反，你必須寫一些腳本生成每個定理

3.theorem聲明

• 這是最簡單的一部分
• 只是檢查定理適用於當前的數據
• 如果不定理無效
• 如果數據集是隨機使用足夠大的測試計數...

你得有發言的問題「廣場A和二次B相交」

• 我想你說，它產生
• 數據集後這僅僅是子彈1
• 另一個條件因此您的數據集生成器必須生成相交的A，B方塊
• A - 按原樣生成

• 放乙 - 啓動內部A（隨機地或在中間或任何）點

• 另一種選擇是從數據集

• 選擇只相交方格經過所有的i = 1..N平方（A）
• 然後再通過1 + 1..N廣場，如果兩個相交的那是你的乙方

希望我不是太遠離你想要做什麼......

Answer 2

我試圖反駁您的定理使用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在45ms後出現「UNSAT」。