核心的性能特征。具有多个有限域约束的逻辑

我在miniKanren学习关系编程,我决定实现一个时间调度系统。基本上,它可以归结为有限域上的三种关系。

首先,有一个时间带,它有开始、持续时间、结束和发生在一个空间中:

(l/defne stripo
  "Defines time strip relationship. Time strip start must be before end, and have a duration."
  [work] ([[start duration end _]]
          (fd/+ start duration end)))

然后,在条带列表(由4个元素组成的列表)上有一个“发生在”关系。这是两个事件的结束和开始之间的成对关系:

(l/defne happens-beforo
         "Defines a happens-before relationship between consecutive time strips in a list."
         [elements]
         ([[]])
         ([[a]])
         ([[a b . d]]
          (l/matche [a b] ([ [_ _ e _] [s _ _ _] ] (fd/<= e s)))
          (happens-beforo (l/llist b d))))

最后,存在一种非重叠关系,即当两个时间段共享同一空间时,它们不能重叠:

(l/defne non-overlappo
  "Two time strips must not overlap in time, if they share the same space"
  [a b]
  ([[_ _ _ sp1] [_ _ _ sp2]]
   (l/conde
     [(l/== sp1 sp2)
      (l/conde
        [(happens-beforo [a b])]
        [(happens-beforo [b a])])]
     [(l/!= sp1 sp2)])))

我可以运行很长的查询来查找 happens-beforo 关系,数千个时间段都可以。当我限制这些时间段的空间时,问题就开始出现了。这是一个实现这一功能的函数:

(l/defne constrain-spaceo
  "This constraint will assure that all time strips within the argument
  obey non-overlapping relationship with each other. Quadratic."
  [strips]
  ([[]])
  ([[w . ws]]
   (let [space' (l/defne space' [c a]
                  ([_ []])
                  ([_ [f . d]]
                   (non-overlappo c f)
                   (space' c d)))]
     (l/all (space' w ws) (constrain-spaceo ws)))))

对于条带q的列表,它建立了一个 non-overlappo 每两个元素之间的关系。因为它是一个双向关系,所以小于n^2。

当我使用 constrain-spaco 只需10条,搜索时间就会大大缩短,我无法生成任何结果。

到目前为止,我一直在尝试减少这一时间的方法,它似乎与争夺一个空间的条带数量有关,而不管总共有多少条。如果我创建两组条带,一组在空间0中,另一组在空间1中并应用 约束spaco 在整个条带列表上,则时间是这些条带单独计算的次数之和。

我的问题是:

1. 为什么有限域约束的数量会对时间产生如此大的影响?我的印象是,限制的数量有助于搜索时间。
2. 有没有办法缩短搜索时间?也许会改变数据表示?