2

我正在尝试编写一个程序，该程序需要计算处理布尔函数的特定值。给定一个由覆盖 F 给出的单输出布尔函数 f，假设我将函数的密度定义为函数值为 1 的所有输入向量的分数。

例如，假设我传入给定的函数 f(a, b, c)，它由覆盖 F = ab'+c' 定义。该函数有 5 个 ON-set 最小项，总共有 8 个最小项，因此其密度为 d(f) = 5/8 = 0.625。应该注意的是，立方体 ab' 覆盖了 2 个最小术语，而立方体 c' 覆盖了 4 个最小术语，但其中一个最小术语被两个立方体覆盖。

谁能想到一个好的算法来处理这个问题？我强烈怀疑它最好以递归方式表达，但我无法确定有效的东西。

4

2 回答 2

5

坏消息：永远快的算法是没有希望的。

即，这个问题：

给定一个合取范式（和的乘积）的布尔公式，确定是否存在自由变量的赋值，使得公式产生真

是NP完全的。这意味着，如果您找到解决它的多项式时间算法，您也可以在多项式时间内解决一些世界上最困难的问题（背包、旅行商问题、哈密顿循环问题等等）。没有人真正期望这是可能的。

这个问题其实等价于这个问题：

给定一个析取范式（乘积之和）的布尔公式，确定其密度是否为 100%

好消息：

输入大小可能非常小。在三个变量中，您并不真正关心速度。在 30 个输入变量处，您仍然更有可能耗尽内存（使用某些算法）而不是运行时间过长。

算法#1：O(2^v*i)时间，几行代码，v=变量数；i=输入的长度。

  • 如果任何子句不一致（A & !A），则删除它。
  • 首先按大小对子句进行排序，最大（变量最少）。
  • 对于全集中的每一个最小项
    • 对于输入中的每个子句
      • 对于术语中的每个文字
        • 如果 minterm 没有被字面量覆盖，则继续下一个子句
      • minterm 包含在以下子句中：
      • 计算涵盖的最小术语，并继续下一个最小术语。
    • minterm 没有被任何文字覆盖；继续下一个学期。
  • 让density = [#covered terms]/[#terms]

如果你想跑得更快，你需要希望有一个好的输入。您可以尝试使用二元决策图 (BDD) 对当前编码的最小项集进行编码，并在您从输入中添加子句时尝试更新二元决策图。

二元决策图是有根有向无环图，每个节点要么是决策节点（测试单个变量，然后采用假分支或真分支）或叶节点（要么 要么true）false。例如，XOR可以用这个二元决策图表示：

     |
     A
    / \
   /   \
  B     B
 / \   / \
0   1 1   0

算法 #2（延迟扩展 BDD，更复杂但对于大量变量可能更快）：

  • 如果任何子句不一致（A & !A），则删除它。
  • 首先按大小对子句进行排序，最大（变量最少）。
  • 从一个空的 BDD 开始（root = false）
  • 对于每个子句
    • 更新 BDD：从根目录开始。
    • 对于每个变量：
      • 如果该子句没有更多文字，请将当前节点替换为true（仅在您来的边缘）
        • 如果直接兄弟也是true，则用 替换公共父true节点，并对新节点重复此测试。
      • 如果当前节点是true
        • 继续下一个子句或递归分支，或加入同级线程。
      • 如果变量在子句中并且在当前 BDD 节点中，
        • 下降到与子句相交的孩子。
      • 如果变量在子句中但不在当前 BDD 节点中。
        • 创建一个新的 BDD 节点
        • 将两个子节点都设置为当前节点
        • 用新节点替换当前节点（仅在您来的边缘）
        • 下降到与子句相交的孩子。
      • 如果变量在 BDD 中但不在子句中
        • 依次递归地下降到两个孩子。或者，在单独的线程中并行下降到两个孩子。
      • 如果变量既不在 BDD 中也不在子句中
        • 没做什么。
  • 让density = 0/(2^variables)（分母表示建议的整数计算比例）
  • 每个叶节点都是true或false。对于 BDD 中的每条路径
    • 如果叶节点是true
      • 让length是沿路径遇到的非叶节点的数量。
      • 添加1/(2^length)到density.
于 2013-02-27T00:12:57.187 回答
0

令 f 和 g 为布尔表达式。

递归分解

d(f and g) = d(f)d(g|f)
d(f or g) = d(f) + d(g) - d(f and g)
for d(g|f) you do unit/expression propergation of f in g

E.g. d(x' + y | x) = d(y)     (I do not have a way to implement it for non single literals on right side of | apart from brute force)

d(g|f) can also be read as what is the density of g in the true area of f.

示例 1：

d(ab'+c)
= d(ab') + d(c) - d(ab'c)
= d(a)d(b) + d(c) - d(a)d(b')d(c)
= 0.5*0.5 + 0.5 - 0.5*0.5*0.5
= 0.625

示例 2：

d((a+b)(a+c))
= d(a+b)d(a+c|a+b)
= (d(a) + d(b) - d(a)*d(b))*(d(a|a+b) + d(c|a+b) - d(ac|a+b))
= 0.75*((2/3) + 0.5 - (1/3))
= 0.625

可能不比蛮力好，但它是递归的。

d(g|f)如果f是立方体或文字，也更容易做到。所以下面的身份可以用来交换边：

d(g|f)d(f) = d(f|g)d(g)

另一个使用上述标识的解析示例（用于将 args 交换到给定的运算符）

d((a+b)(a'+b))
= d(a+b)d(a'+b|a+b)
= 0.75(d(a'|a+b) + d(b|a+b) - d(a'b|a+b))
= 0.75(d(a+b|a')d(a')/d(a+b) + d(a+b|b)d(b)/d(a+b) - d(a+b|a'b)d(a'b) / d(a+b))
= 0.75(d(b)d(a') + d(1)d(b) - d(1)*d(a')*d(b))/d(a+b)
= 0.75*(0.5*0.5 + 1*0.5 - 1*0.5*0.5)/0.75
= 0.5

一个有趣的模式发生在 2/3 电路中：

d((a+b)(b+c)(c+a))
= d(a+b)d((b+c)(c+a)|a+b)
. . . skipping many steps . . .
= d((a+b)(b+c)|c)d(c) + d((a+b)(b+c)|a)d(a) - d((a+b)(b+c)|ca)d(ca)
= d(a+b)d(c) + d(b+c)d(a) - d(1)d(c)d(a)
= 0.75*0.5 + 0.75*0.5 - 1*0.5*0.5
= 0.5

还有一个技巧，为了减少分支，可以使用以下恒等式：

d(a+b) = 1 - d(a'b')

这基本上是用于不同目的的德摩根理论。现在，不再分支 3 种方式来处理 OR，而是只分支了一种方式。

再次显示您的示例，显示所有步骤并使用 demorgans 身份：

d(ab'+c')
= 1 - d((ab')'c')
= 1 - d((ab')')d(c'|(ab')')
= 1 - (1 - d(ab'))d((ab')'|c')d(c) / d((ab')')
= 1 - (1 - d(ab'))(1 - d(ab'|c'))d(c') / (1 - d(ab'))
= 1 - (1 - 0.25)(1 - d(ab'))*0.5 / (1 - 0.25)
= 1 - (1 - 0.25)(1 - 0.25)*0.5 / (1 - 0.25)
= 0.625

为常见的子表达式添加缓存也应该提供速度提升。

玩了一会之后。我提出了一个很好的递归表达式，用于以合取范式表示布尔表达式的密度。

let f be the first CNF clause
let g be the remaining clauses
d(fg) = d(g) - d(g|f')d(f')

每个递归在左侧分支中剥离一个子句并从右侧分支中剥离三个变量（对于 3CNF）。（d(f') 是常数时间，因为它是单子句）

这是最后一个表达式在 Rust 中的样子。

pub fn cnf_density(mut cnf: CnfFormula) -> f64 {
    if cnf.is_empty() {
        return 1.0;
    }
    // d(fg) = d(g) - d(g|f')d(f')
    let clause1 = cnf.remove(0);
    let mut cnf2 = cnf.clone();
    for lit in &clause1 {
        // unit propergation of f' in g|f'
        cnf2.assign_lit(lit.negated());
    }
    let d1 = cnf_density(cnf);
    let d2 = cnf_density(cnf2);
    d1 - d2 * 2.0_f64.powf(-(clause1.len() as f64))
}

又发现了一个窍门。您可以从旧的密度开始f=1然后d(f) = 1计算新的密度，同时添加子句来构建您的 CNF 表达式：

d(f(a+b)) = d(f) - d(f|!a!b)d(!a!b)

如果您希望获得任何性能，您需要对其输入的任何技术进行有限的密度函数缓存。它仍然是指数级的。该d(f(a+b)) = d(f) - d(f|!a!b)d(!a!b)技术的伟大之处在于它为您提供了一个递减的上限。所以你可以在任何时候终止它，并且仍然告诉你密度会小于什么。如果有一个类似的技巧来增加下限，那就太好了。

Rust 的最后一招：

pub fn cnf_density(&mut self, cnf: CnfFormula, lvl: usize) -> f64 {
    if cnf.is_empty() {
        return 1.0;                                                                         }
    if cnf.len() == 1 && cnf[0].is_empty() {
        return 0.0;
    }
    if let Some(d) = self.cache.get(&cnf) {
        return *d;
    }                                                                                       // d(f(a+b)) = d(f) - d(f|!a!b)d(!a!b)
    let mut f = 1.0_f64;
    let mut cnf2 = CnfFormula::new();                                                       let mut idx: usize = 0;
    if self.cache.len() > 1000 {
        self.cache.clear();
    }
    for clause in &cnf {
        idx += 1;
        if lvl == 0 {
            println!("{:?}", clause);
            println!("{}/{}", idx, cnf.len());
            println!("{}", self.cache.len());
            println!("d(f) = {}", f);
        }
        let mut cnf3 = cnf2.clone();
        cnf2.push(clause.clone());
        for lit in clause {
            cnf3.assign_lit(lit.negated());
        }
        f -= self.cnf_density(cnf3,lvl+1) * 2.0_f64.powf(-(clause.len() as f64));
    }
    self.cache.insert(cnf, f);
    f
}
于 2021-01-12T13:08:46.753 回答