问题标签 [dpll]

是否有任何直接的方法可以在可合成的 Verilog 中实现全数字锁相？一切（包括 VCO）都应该被合成。我要锁定的信号约为系统时钟频率的 0.1-1%。我正在使用我从 1980 年的 IEEE 论文中重建的一个，但它的表现不如宣传的那么好。

为简单起见，锁可以在二进制脉冲信号上工作。

我正在尝试在 C++ 中实现DPLL算法，我想知道哪种数据结构最适合解决此类递归问题。现在我正在使用向量，但是代码又长又丑。有什么建议吗？

最近，我在Haskell中实现了一个朴素的DPLL Sat Solver，改编自 John Harrison 的实用逻辑和自动推理手册。

DPLL 是多种回溯搜索，因此我想尝试使用Oleg Kiselyov 等人的Logic monad。但是，我真的不明白我需要改变什么。

这是我得到的代码。

• 我需要更改哪些代码才能使用 Logic monad？
• 奖励：使用 Logic monad 是否有任何具体的性能优势？

如维基百科中所述，我正在 C++ 中实现DPLL算法：

但表现糟糕。在这一步中：

目前我试图避免创建副本，Φ而是添加lornot(l)到一个且唯一的副本，并在 /if的 returnΦ时删除它们。这似乎破坏了给出错误结果的算法（即使集合是）。DPLL()falseUNSATISFIABLESATISFIABLE

有关如何在此步骤中避免显式复制的任何建议？

这是我的 Makefile

我的 OCaml 文件是这样的（dpll 的一部分）。

我收到以下错误：

那么我该如何链接呢？

非常感谢

我从 Z3 的运行中获得了一些统计数据。我需要明白这些是什么意思。对于 sat 和 SMT 解决方案的最新发展，我相当生疏和不了解最新情况，因此我试图自己寻找解释，但我可能大错特错。所以我的问题主要是：

1) 措施的名称是什么意思？

2）如果错了，你能给我指点以更好地理解他们所指的吗？

其他观察如下，概念上属于上述两个问题。提前致谢！

我的解释如下。

• 锁相环。以下所有指标均参考 DPLL 算法的行话，这是大多数求解器的基础。

  • ：决定
    • 决定数
  • :传播
    • 传播次数（我猜是单位传播）
  • :binary-propagations, :三元传播
    • 一次传播两个和三个文字
  • ：冲突
    • 冲突数

• 解决方案。粗略地说，操作将解释子句作为集合；从分辨率中提取的技术是解决 SAT 的另一种范式。

  • : 包含
  • :subsumption-resolution
    • 以上两者有什么区别？
  • :dyn-subsumption-resolution
    • 应该在这里描述：学习动态包容，Hamadi 等人。

• 其他技术

  • :minimized-lits
    • 没有明确的想法。它可能与从句学习有关吗？
  • :probing-assigned
    • 我猜它计算了“探测”时所做的分配数量，我猜这是某种前瞻技术。
  • :del 子句
    • 删除子句的数量（出于什么原因？冗余？）
  • : elim-literals : elim-clauses : elim-bool-vars : elim-blocked-clauses
    • 消除后的实体数量。这些指标指的是特定的 SAT 求解技术（参见 M.Järvisalo 等人的 Blocked Clause Elimination，以获取参考）
  • :重启
    • 重启次数。

• 其他方面

  • :mk-bool-var : mk-binary-clause : mk-ternary-clause : mk-clause
    • 创建的布尔变量和二元、三元和通用子句的数量。
  • ：记忆
    • 使用的最大内存量。
  • :gc 子句
    • 垃圾回收条款...？
    • 根据我的实验，这种解释是合理的，因为情况总是如此
      • : gc-clause <= : del-clause ; 就我而言，不平等是严格的。
    • 并非总是如此
      • : gc-clause <=: elim-clauses ; 它也可以是：gc-clause > : elim-clauses

我正在尝试设计方法来提高 z3 在我的问题上的性能。我知道 CAV'06论文和技术报告。z3 v4.3.1 的相关部分是否与这些文档中描述的内容不同，如果不同，有何不同？此外，z3 中默认遵循的策略是什么，用于决定何时检查线性实数算术中与已决定（和传播）命题文字相对应的理论原子的一致性？

我是 Haskell 的一名普通人，我正在尝试使用 DPLL 编写一个简单的 SAT 求解器。

我有一个函数 expand ，它采用从模式(A1 and A2 ...) Or (B1 and B2 ...)到合取范式：(A1 or B1) and (A1 or B2) and ... (A2 or B2) and ....

我已经将我的表达式数据类型表示如下

（我不关心否定，因为我可以用 -x 表示 Not(x)）

但是现在，写扩展，构造函数标签看起来真的很难看。

我可以让这段代码更干净吗？

I have profiled my problems, which are in (pseudo-nonlinear) integer real fragment using the profiler gprof (stats here including the call graph) and was trying to separate out the time taken into two classes:

I)The SAT solving part (including [purely] boolean propagation and [purely] boolean conflict clause detection, backjumping, any other propositional manipulation)

II)The theory solving part (including theory consistency checks, generation of theory conflict-clauses and theory propagation).

Do lines 3280-3346 in smt_context.cpp within bounded_search() constitute the top-level DPLL(X) loop?

I believe it is easier to sum-up the time in SAT solver functions (since they are fewer) and then the rest can be considered as theory solvers's time. I am trying to figure out which functions I should consider as falling under class I above? Are they smt::context::decide(), smt::context::bcp() within smt::context::propagate()? Any others? smt::context: resolve_conflict() seems to be mixed with calls to theory solver?

Is it correct that smt::context::propagate() seems to be mostly theory propagation (class II) except its bcp() function? Also, smt::context::final_check() seems to be purely in class II.

Any hints greatly appreciated. Thanks.

Z3 的算术求解器是基于 DPLL(T) 和 Simplex（在本文中描述）开发的。而且我不明白Z3在生成冲突解释时如何执行回溯。我举个例子：

线性算术公式为：

(2x1+x2≤200 OR 3x1+x2≤250) AND (2x1+x2+x3≤200 OR 4x1+2x2+x3≤400) AND x1≥50 AND x2≥50 AND x3≥60

在断言2x1+x2≤200, 2x1+x2+x3≤200, x1≥50,x2≥50之后x3≥60，它产生了一个冲突解释集{2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}。

我的问题是，当这个冲突集生成时，如何执行回溯？