Basic definitions and terminology

A propositional logic formula, also called Booleanexpression, is built from variables, operators AND (conjunction, also denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬),and parentheses. A formula is said to be satisfiable if it can be madeTRUE by assigning appropriate logicalvalues (i.e. TRUE, FALSE) to its variables. The Boolean satisfiabilityproblem (SAT) is, given a formula, to check whether it issatisfiable. This decision problem is of central importance invarious areas of computer science, including theoretical computer science, complexity theory, algorithmics,cryptographyand artificial intelligence.

命题逻辑公式（也称为布尔表达式），由变量、与运算符∧、或运算符∨、非运算符¬和括号组成。设定适当的逻辑变量值使逻辑表达式的值为真，就说逻辑表达式是能够满足的。布尔可满足性问题（SAT）就是检查逻辑表达式是否是可满足的。这个判定问题是计算机科学，包括计算机理论、复杂性理论、算法、密码学和人工智能众多领域的核心重要问题。

There are several special cases of the Boolean satisfiabilityproblem in which the formulas are required to have a particular structure. A literalis either a variable, then called positive literal, or the negation of avariable, then called negative literal. A clause is a disjunctionof literals (or a single literal). A clause is called Horn clause if it contains at most one positive literal. A formula is in conjunctive normal form (CNF) ifit is a conjunction of clauses (or a single clause). For example, x₁is a positive literal, ¬x₂ is a negative literal, x₁∨ ¬x₂ is a clause, and (x₁ ∨ ¬x₂)∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁is a formula in conjunctive normal form, its 1st and 3rd clause are Hornclauses, but its 2nd clause is not. The formula is satisfiable, choosing x₁ = FALSE,x₂ = FALSE, and x₃ arbitrarily,since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x₃) ∧ ¬FALSEevaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x₃) ∧ TRUE, andin turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula a∧ ¬a, consisting of two clauses of one literal, is unsatisfiable, sincefor a=TRUE and a=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e. toFALSE) and FALSE ∧ ¬FALSE (i.e. again to FALSE), respectively.

一些具体情况下，布尔满足性问题表达式要求有特定的结构。逻辑变量叫正文字，它的非运算形式叫反文字，子句是它们的或运算形式（包括一个文字）。最多有一个正文字的子句叫强子句。子句进行与运算的表达式叫合取范式（CNF）。例如，x₁是正文字，¬x₂是反文字，x₁ ∨ ¬x₂就是一个子句。而(x₁ ∨ ¬x₂) ∧ (¬x₁∨ x₂ ∨ x₃) ∧ ¬x₁是合取范式。此式的第一和第三子句是强子句，第二个子句不是。选择x₁ = 假, x₂ = 假, x₃任意，从 (假∨ ¬假) ∧ (¬假∨假∨ x₃) ∧ ¬假，得出 (假∨ 真) ∧ (真 ∨假∨ x₃) ∧ 真, 子句值运算为 真 ∧ 真 ∧ 真 (即结果为真)。

批注：真够啰嗦的！