问题标签 [horn]

我最近听到了一些关于 HORN 的消息，想知道它可以解决什么问题，或者在现实生活中使用它有什么好处。

http://code.google.com/p/hornget/

最近 NHibernate 2.1 的升级使一个令人头疼的问题浮出水面。

似乎大多数项目默认构建为签名程序集。例如 fluentnhibernate 引用密钥文件 fluent.snk。

Nhibernate.search 从我可以收集的内容中构建无符号并且不会构建签名，也就是说，如果您引用生成的密钥文件，您会收到错误：

引用的程序集“Lucene.Net”没有强名称

这意味着像 castle.activerecord 这样具有 nhibernate.search 作为依赖项的项目将不会构建，因为您会收到可怕的错误引用程序集 nhibernate.search 没有强名称：

相当多的项目使用 caslte.activerecord 所以它的构建非常重要。

有没有人知道在这里做什么，因为我完全没有想法？

这是完全的疯狂。

我只是对喇叭子句的定义感到困惑。“~A=>B”是喇叭子句吗？如果我们将其转换为析取形式，它将是“AvB”，它不是喇叭子句。

所以我想知道它是否是一个喇叭子句。谢谢。

我知道证明喇叭公式是否可满足更容易。我的问题是：为什么使用喇叭公式而不是普通 CNF 更容易？

我的目标是创造一种效果，就像在这个 codepen 上找到的效果一样。在背景视频上有一个透明的 SVG。到目前为止，我有一个从 Photoshop 导出的带有路径形状的 AI 文档。理想情况下，我希望路径内部是透明的，但其余部分是白色的，就像示例中一样。我怎样才能达到这样的效果？

看起来它与这行代码有关，但我肯定误解了一些东西。

我认为我的 SVG 还没有准备好成为一条路径，就好像我将它导出一样，它显示为空白，如果我在路径上放置一个笔划，除了笔划是透明的，或者它没有以任何透明度出现一点也不。

通常，我作为 Web 开发人员的工作流程从来没有让我深入使用 SVG 进行这项工作，所以我有点卡在这个问题上。

基本上我想获得高度.r-side并将其应用于高度，.l-side以便即使调整窗口大小并定位在彼此之上，这两个元素也始终具有相同的高度。我不确定我的 jQuery 有什么问题。

这是我得到的：

$(window).load(function(){ $(".l-side").css({'height':($(".r-side").height()+'px')}); });

使用 jQuery 3.1.1。这是我遇到的问题的 jsFiddle 。

我对 jQuery 以外的其他方法持开放态度来实现这一点，但在我的研究中，我只找到了特定于列的解决方案，并且这些 div 需要直接放置在彼此之上。

我正在使用 Z3 和扩展的 SMT-LIB2 语法来解决我的角子句。我知道 horn 子句的 head 应该是一个未解释的谓词；但是，我想知道如何将以下子句重写为一组喇叭子句。

Z3 抱怨(> a 0)不能成为喇叭子句的头。我可以将最后一个子句改写如下：

但是，子句变得如此弱，以至于我没有得到不变量的预期模型inv。我想知道是否有更好的方法来做到这一点。

就像在这个文件中规则中的“最多”关键字一样：

horn1.smt2（来自 Z3 github 存储库示例/python/data）

似乎关键字“最多”的含义是六个字面量（LKJIHG）中只有五个字面量可以同时为真，或者它意味着什么，我想不通。如果有任何好人可以帮助我，我真的很感激。

对于某些受限类的逻辑公式，可满足性问题可以在多项式时间甚至线性时间内有效地解决。一类是霍恩公式，它仅由霍恩从句组成，最多有一个正面文字。我听说可以使用图表在线性时间内解决 Horn SAT，但找不到此类解决方案的任何实现。现在我真的很感兴趣它是否可能，如果是的话，算法会是什么样子？