计算机数理逻辑-命题逻辑-SAT

1. SAT 布尔可满足性问题

可满足性（英语：Satisfiability）是用来解决给定的真值方程式，是否存在一组变量赋值，使问题为可满足。布尔可满足性问题（Boolean satisfiability problem；SAT ）属于决定性问题，也是第一个被证明属于NP完全的问题

决定性问题，亦称判定问题，（英语：Decision problem）是一个在某些形式系统回答“是”或“否”的问题

A computer program that searches for a model for a propositional formula is called a SAT Solver.

可以这么理解sovler：

  • decide: 确定sat/unsat/unsure
  • solve: 给出models

2. Properties of Clausal Form

Let S, S′ be sets of clauses.

  • S≈S′相似 denotes that S is satisfiable if and only if S′ is satisfiable. (并没说要有同样的解model)
  • It is important to understand that S≈S′ does not imply that S≡S′ (S is logically equivalent to S′)

2.1. Pure Literals 纯字面量

Let S be a set of clauses.** A pure literal in S is a literal l that appears in at least one clause of S, but its complement lc does not appear in any clause of S**

  • 该字面量出现至少一次，且取反的字面量不存在

Let S be a set of clauses and let l be a pure literal in S. Let S′ be obtained from S by deleting every clause containing l. Then S≈S′

  • 也就是删除纯字面量，set of clauses的完备性不改变

2.2. Unit Clauses 单位子句

Let {l}∈S be a unit clause and let S′ be obtained from S by deleting every clause containing $l$ and by deleting $l^c$ from every (remaining) clause. Then S≈S′.

  • 单位子句就是只有一个字面量的
  • 删除包含l的子句，删除子句中包含的lc，set of clauses的完备性不改变

2.3. Empte Clauses

  • □ is unsatisfiable
    • 根据Unit Clauses的定理显然

2.4. Renaming

Let $S$ be a set of clauses and $U$ a set of atomic propositions. $R_U(S)$, the renaming of S by U, is obtained from S by replacing each literal l on an atomic proposition in U by $l^c$

3. Davis-Putnam Algorithm 戴维斯–普特南算法

The Davis-Putnam (DP) algorithm was one of the first algorithms proposed for deciding satisfiability

戴维斯-普特南（DP）算法是最早提出的用于决定可满足性的算法之一

  • Input: A formula A in clausal form.

  • Output: Report that A is satisfiable or unsatisfiable.

  • Perform the following rules repeatedly, but the third rule is used only if the first two do not apply

    • Unit-literal rule

      If there is a unit clause {l}, delete all clauses containing l and delete all occurrences of $l^c$ from all other clauses

    • Pure-literal rule （可以视作UP特例）

      If there is a pure literal l, delete all clauses containing l

    • Eliminate a variable by resolution:

      Choose an atom p and perform all possible resolutions on clauses that clash on $p$ and $\bar{p}$. Add these resolvents解析器 to the set of clauses and then delete all clauses containing $p$ or $\bar{p}$

  • Terminate the algorithm under the following conditions:

    • If empty clause □ is produced, report that the formula is unsatisfiable.
    • If no more rules are applicable适用, report that the formula is satisfiable.

  • 注意delete clause不会造成empty clause，但delete literal可能会（运用up时）

Example

  • ${ p, \bar{p}q, \bar{q}r, \bar{r}st }$

    Performing the unit-literal rule on p leads to the creation of a new unit clause q upon which the rule can be applied again. This leads to a new unit clause r and applying the rule results in the singleton set of clauses {st}. Since no more rules are applicable, the set of clauses is satisfiable.

Repeatedly applying the unit-literal rule until it is no longer applicable is called unit propagation or Boolean constraint propagation（BCP）. 单位传播或布尔约束传播

4. Davis-Putnam-Logemann-Loveland(DPLL)

  • DPLL is a decision procedure for propositional clausal logic

解决 CNF-SAT 问题

一个朴素的回溯算法会检查所有可能的赋值，直到找到一个解；而 DPLL 算法 则会利用 BCP 来删掉一些不可能满足公式的赋值，缩小搜索树。当遇到冲突时，它会回溯到上一个并非由 BCP 作出的决定，选择另一种可能的值

Creating all possible resolvents on an atom is very inefficient. The DPLL algorithm improves on the DP algorithm by replacing the variable elimination step with a search for a model of the formula

The DPLL algorithm recursively extends a partial interpretation by adding an assignment to some atom that has not yet been assigned a truth value. The current set of clauses is evaluated using the new partial interpretation and simplified by unit propagation. If the set of clauses contains a conflict clause (例如p vs not p), there is no need to continue extending this partial interpretation and the search backtracks递归回溯 to try another one

The DPLL algorithm can be summarized in the following pseudocode, where $Φ$ is the CNF formula:

1
2
3
Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A truth value indicating whether Φ is satisfiable.
1
2
3
4
5
6
7
8
9
10
11
function DPLL(Φ)
    while there is a unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    while there is a literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    if Φ is empty then
        return true;
    if Φ contains an empty clause then
        return false;
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});
  • “←” denotes assignment. For instance, “largest ← item” means that the value of largest changes to the value of item.
  • When the formula contains an empty clause, the clause is vacuously false because a disjunction requires at least one member that is true for the overall set to be true

Example

简化版表达

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
DPLL:
  Run BCP on the formula.
  If the formula evaluates to True, return True.
  If the formula evaluates to False, return False.
  If the formula is still Undecided:
    Choose the next unassigned variable.
    Return (DPLL with that variable True) || (DPLL with that variable False)

DPLL:
  在公式上执行 BCP。
  如果公式的值一定为真，返回真。
  如果公式的值一定为假，返回假。
  如果公式的值仍不确定:
    选择下一个未决定的字面量
    猜测该字面量为真，然后执行 DPLL
    如果 DPLL 的结果为真，返回真
    否则猜测该字面量为假，然后执行 DPLL 并返回结果
  • 某种程度上看，DDLP = Unit Propagation + Decision

书面写法

Unit Propagation is a polynomial-time多项式时间 decision procedure for the fragment of Horn clauses.

  • 这也意味着ddlp还要加入decide（以及backtrack递归回溯）环节使得其可以全面覆盖所有类型的子句

Example

5. Conflict Driven Clause Learning(CDCL)

  • CDCL=DPLL + Backjumping后跳 + Lemma Learning推理学习

DPLL 有三个缺点。首先，它的决策是朴素（naive）的。其次，它遇到冲突的时候，只知道当前的部分赋值会导致冲突，除此之外学不到任何东西。第三，它每次只会回溯一层，因此会把大量时间浪费在一片必定会失败的搜索空间中

冲突驱动子句学习的改进：

  • 冲突来源的子句学习（clause learning from conflicts）
  • 非时序回溯（non-chronological[ ˌ krɔnə'lɔdʒikəl ] backtracking）
  • 当CDCL学习一个子句时，它会回溯到该子句的断言层。你可以认为这意味着它回溯到影响所学子句中某一字面量的最新猜测。由于这个子句有$x_1$和$x_5$，而x1是该子句中最新被猜到的一个，所以我们回溯到我们将$x_1$设置为True的时候

5.1. 蕴含图

  • 当 CDCL 遇到冲突时，它会查看已作出的推测，以及从 BCP 得到且最终导致冲突的那些赋值。我们把这些推测和由它们推出的结论画成一个图（graph），称为蕴涵图（implication graph）

蕴含图是一个有向无环图。它的每个顶点代表对一个变量的赋值，此外还有一个代表冲突的特殊顶点。图中的边则表示赋值或冲突的理由；具体来说，如果我们有一个单位子句，并由此推出子句中唯一的那个未知变量的值，就可以从子句中每一个已知的变量对应的顶点连一条边到这个新推导出的变量对应的顶点；推出冲突的情形也类似

  • 一旦 CDCL 学到了一个子句，它就能够回溯超过一层，并把 BCP 立即应用到学到的新子句上。这种利用学到的子句回溯多层的能力就是我们前面说的非时间顺序回溯（non-chronological backtracking）

clause learning step:

  1. c4 is the clause directly responsible for the current conflict. Our partial learned clause is ¬x1 ∨ ¬x6 ∨ ¬x7.
  2. c3 is the clause responsible for the most recent BCP prior to the conflict, x7 = T. Resolving c3 and c4 gives us the partial clause of ¬x1 ∨ ¬x5 ∨ ¬x6.
  3. c2 is the clause responsible for the next most recent BCP, x6 = T. Resolving c2 with our current partial clause gives us ¬x1 ∨ ¬x5.
    1. This is our complete learned clause, because there is only one literal at decision level two within it.
    2. Since x1 has the highest decision level in our new learned clause, we backtrack to that level where we will be able to apply our newly learned clause, c9 = ¬x1 ∨ ¬x5

5.2. A note about Decision Heuristics

The version of CDCL we implemented in this article does not have any smart decision heuristics启发式决策. Better decision heuristics is often the source of breakthroughs SAT Solver performance increases and are very important to modern SAT solvers today. We only examined clause learning and non-chronological backtracking as improvements over DPLL to keep the scope of this project small.

我们在这篇文章中实现的CDCL版本没有任何智能决策启发式方法。更好的决策启发式往往是SAT求解器性能提高的突破口，对今天的现代SAT求解器非常重要。我们只研究了子句学习和非同步回溯作为对DPLL的改进，以保持这个项目的范围很小。

5.3. pseudocode

1
2
3
4
5
6
7
8
9
10
11
12
13
14
def CDCL(ϕ):     // ϕ is a CNF formula
   τ←∅
   while true:
      τ←unit-propagate(ϕ,τ) // Unit propagation
      if τ falsifies a clause:
         if at decision level 0: return unsat
         C←analyze-conflict(ϕ,τ) // Build the learned clause
         ϕ←ϕ∧C // Add it to the formula
         backjump to an earlier decision level according to C
      else
         if all variables have values: return sat
         start a new decision level
         choose a literal l such that τ(l) is undefined
         τ←τ∪{l} // "Decide" that l is true

6. Complexity 复杂度

6.1. P

  • 多项式时间复杂性类（Polynomial[ˌpɔli'nəumjəl] time）
  • 所有P问题都能被经典计算机（非量子计算机）轻松解决
  • 如果一个问题是P问题，那么它必须满足在多项式时间nc内验证一个算法问题的实例是否有解，
    • n是输入长度
    • c是个常数
  • 典型问题：
    • 这个数是否是个质数？
    • 两点之间的最短路径是什么？

6.2. np

  • 非定常多项式时间复杂性类（Nondeterministic Polynomial time）
  • 能在多项式时间验证答案正确与否的问题
  • 算起来不一定快，但对于任何答案我们都可以快速的验证这个答案对不对

The method of truth tables is a deterministic algorithm for deciding both satisfiability and validity in propositional logic. The algorithm is exponential, because the size of a formula is polynomial in $n$, the number of variables, while the truth table has $2^n$ rows.

The method of semantic tableaux is a nondeterministic algorithm for both satisfiability and validity, because at any stage of the construction, we can choose a leaf to expand and choose a formula in the label of the leaf to which a rule will be applied. Nevertheless, it can be shown that there are families of formulas for which the method of semantic tableaux is exponential, as are the David-Putnam procedure and resolution

The problems of deciding satisfiability and validity in propositional logic are almost certainly intractable: the former is in np and the latter in co-np

7. Formalising problems in propositional logic

7.1. N皇后

7.2. Encoding fixed bit-width arithmetic

7.3. Linear (in)equalities

  • 考虑$x + y = z$
  • Linear inequalities
  • Non-linear (in)equalities？

8. 参考