|||
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, x1is a positive literal, ¬x2 is a negative literal, x1∨ ¬x2 is a clause, and (x1 ∨ ¬x2)∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1is a formula in conjunctive normal form, its 1st and 3rd clause are Hornclauses, but its 2nd clause is not. The formula is satisfiable, choosing x1 = FALSE,x2 = FALSE, and x3 arbitrarily,since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x3) ∧ ¬FALSEevaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x3) ∧ 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)。例如,x1是正文字,¬x2是反文字,x1 ∨ ¬x2就是一个子句。而(x1 ∨ ¬x2) ∧ (¬x1∨ x2 ∨ x3) ∧ ¬x1是合取范式。此式的第一和第三子句是强子句,第二个子句不是。选择x1 = 假, x2 = 假, x3任意,从 (假∨ ¬假) ∧ (¬假∨假∨ x3) ∧ ¬假,得出 (假∨ 真) ∧ (真 ∨假∨ x3) ∧ 真, 子句值运算为 真 ∧ 真 ∧ 真 (即结果为真)。
批注:真够啰嗦的!
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2025-1-5 17:40
Powered by ScienceNet.cn
Copyright © 2007-2025 中国科学报社