Z3統計的解釋

我從Z3的運行中獲得了幾個統計。我需要明白這些意思。我相當生疏，並沒有最新的SAT和SMT解決方案的最新發展，因此我試圖自己找到解釋，我可能是錯誤的。所以我的問題主要是：Z3統計的解釋

1）這些措施的名字是什麼意思？

2）如果錯了，你能給我指點，以更好地理解它們指的是什麼嗎？

其他意見如下，概念上屬於上述兩個問題。在此先感謝！

我的解釋如下。

DPLL。下面的所有指標都是DPLL算法的術語，它是大多數解算器的基礎。
- ：決定
  - 的決定的數量
- ：的傳播
  - 數的傳播的（我猜單元的傳播）
- ：二進制的傳播，：三元的傳播兩個
  - 的傳播，並在一次
- 3種文字：衝突的衝突
  - 數
解決方案。大致來說，操作將條款解釋爲集合;從解決方案中獲得的技術是解決SAT問題的另一個範例。
- ：納入
- ：包容分辨率
  - 是什麼上述兩者的區別？
- ：DYN-包容分辨率
  - 應該在這裏說明：學習動態歸入由哈馬迪等。
其他技術
- ：最小化，雙牀
  - 沒有清晰的概念。它可能與子句學習有關嗎？
- ：探診分配
  - 我猜它計算分配的號碼進行時「探測」，我的猜測是某種前瞻技術。
- ：琳，文字：琳從句：德爾子句
  - 刪除的條款（？是什麼原因冗餘）
- 數elim- bool-vars：elim-blocked-clause
  - 刪除後的實體數量爲elim-。這些度量指代特定的SAT解決技術（參見參考阻止第消除，通過M.Järvisalo等人）
- ：重新啓動
  - 重啓的次數。
其它方面
- ：MK-布爾-VAR：MK-二進制子句：MK-三元子句：MK-子句
  - 布爾變量和二進制數，創建了三元和一般條款。
- ：所使用的內存存儲器
  - 最大金額。
- ：GC-條款
  - 垃圾收集條款...？
  - 這種解釋，根據我的實驗是可行的，因爲它總是情況下
    - ：GC-條款 < =：德爾子句;在我的情況下，不平等是嚴格的。
  - 它並不總是的情況是
    - ：GC-子句 < =：琳子句;它也可以是：GC-條款>：琳子句

2013-08-28 gapag

這是一個很好的問題（以及部分答案），這些問題在其他問題上完全沒有涉及，但這裏有一些相關的問題可能會有用：http://stackoverflow.com/questions/17856574/how- to-interpret-statistics-z3 http://stackoverflow.com/questions/10949633/z3-real-arithmetic-and-statistics http://stackoverflow.com/questions/7340888/z3-statistics-what-does-time-衡量http://stackoverflow.com/questions/6841193/which-statistics-indicate-an-efficient-run-of-z3 – Taylor

恐怕這是一個開放式的問題。 Z3公開許多以不同方式收集的計數器。儘管許多捕獲抽象概念，但它們的含義最終基於代碼的實現行爲，其基本意義爲。

幸運的是，源代碼可用並提供了完整的上下文以瞭解每個計數器的行爲。因此，沒有任何一個跟蹤計數器含義的文檔，但源代碼可用於提供完整的上下文。

來源

2013-09-06 15:24:56

回答

相關問題