4

我试图自动证明/反驳一些与正方形相关的几何定理，例如“对于每 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 中如何解决这个问题？

4

2 回答 2

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 在 45 毫秒后出现“UNSAT”。

于 2014-02-25T15:29:48.337 回答
0

我是唯一一个认为这是算法问题的人吗？

  • 是的，问题的标题和开头有点令人困惑，但是
  • 据我了解，问题是（或应该是）如何实现几何陈述的证明。
  • 我认为一些重新编辑/重新标记会对它有好处

我会这样做（不会使用任何语言或框架，因为它不相关）：

1.数据集定义

  • 用于定理的几何实体的总和/大小/计数（点、线、矩形、...）
  • 输入数据的所有条件/约束的总和

2.数据集生成

  • 可以是随机的 + 丢弃无效实体（不匹配 1）
  • 或者您可以在位置/大小的某个精度内生成所有有效的可能性......

  • 但这真的很讨厌，因为时间和空间的复杂性

  • 这是困难的部分

  • 您必须在性能/相关性之间进行选择
  • 恐怕这项任务无法以令人满意的性能自动化
  • 相反，您必须为每个定理编写一些生成脚本

3.定理陈述

  • 这是最简单的部分
  • 只需检查该定理是否对当前数据集有效
  • 如果不是定理无效
  • 如果数据集是随机的，请使用足够多的测试...

您对“正方形 A 和正方形 B 相交”的语句有疑问

  • 我假设您在生成数据集后说明了这一点
  • 这只是子弹 1 的另一个条件
  • 因此您的数据集生成器必须生成相交的 A、B 正方形
  • A - 按原样生成

  • 将 B - 起点放在 A 内（随机或在中间或其他）

  • 另一个选项是从数据集中仅选择相交的正方形

  • 遍历所有 i=1..N 方格 (A)
  • 然后通过 i+1..N 方格，如果两者相交，那么它就是你的 B 方格

希望我离你想做的事情不会太远......

于 2014-02-25T13:35:02.827 回答