Exact Algorithms for General CNF SAT
Exact Algorithms for General CNF SAT
复制标题
通用 CNF SAT 的精确算法
DOI：
10.1007/978-1-4939-2864-4_133
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
E. Hirsch
中科院分区：
文献类型：
--
作者：
E. Hirsch
合取范式中的公式是一组子句（理解为这些子句的合取），子句是一组文字（理解为这些文字的析取），文字可以是布尔变量，也可以是布尔变量的否定。真值赋值将布尔值（假或真）分配给一个或多个变量。赋值被缩写为在此赋值下为 true 的文字列表（例如，将 false 分配给 x 并将 true 分配给 y 由 :x; y 表示）。将赋值 A 应用到公式 F（表示为 F ŒA ）的结果是通过从 F 中删除包含真实文字的子句并删除
A formula in conjunctive normal form is a set of clauses (understood as the conjunction of these clauses), a clause is a set of literals (understood as the disjunction of these literals), and a literal is either a Boolean variable or the negation of a Boolean variable. A truth assignment assigns Boolean values (false or true) to one or more variables. An assignment is abbreviated as the list of literals that are made true under this assignment (e.g., assigning false to x and true to y is denoted by :x; y). The result of the application of an assignment A to a formula F (denoted F ŒA ) is the formula obtained by removing the clauses containing the true literals from F and removing the