2

ブール関数を扱う特定の値の計算を必要とするプログラムを作成しようとしています。カバー F によって与えられる単一出力のブール関数 f が与えられた場合、関数の密度を、関数が値 1 を持つすべての入力ベクトルの割合として定義するとします。

たとえば、cover F = ab'+c' で定義される特定の関数 f(a, b, c) を渡すとします。関数には 5 つの ON セット最小項と合計 8 つの最小項があるため、その密度は d(f) = 5/8 = 0.625 です。キューブ ab' は 2 つの最小項をカバーし、キューブ c' は 4 つの最小項をカバーしますが、それらの最小項の 1 つが両方のキューブによってカバーされることに注意してください。

これを処理するための優れたアルゴリズムを考えられる人はいますか? 再帰的に表現するのが最善であるという強い疑いがありますが、効率的なものを特定するのに苦労しています。

4

2 に答える 2

5

The bad news: there's no hope for an algorithm that is always fast.

Namely, this problem:

Given a boolean formula in a conjunctive normal form (product of sums), decide if there is an assignment of the free variables such that the formula yields true

is NP-complete. This means that if you find a polynomial-time algorithm that solves it, you can solve some of the world's hardest problems (knapsack, travelling salesman problem, hamiltonian cycle problem just to name a few) in polynomial time as well. No-one really expects that to be possible.

This problem is, in fact, equivalent to this problem:

Given a boolean formula in a disjunctive normal form (sum of products), decide if its density is 100%

The good news:

The input size is likely to be very small. At three variables, you don't really care for speed. At thirty input variables, you still are more likely to run out of memory (using some algorithms) than to run unbearably long.

Algorithm #1: O(2^v*i) time, few lines of code, v= number of variables; i=length of the input.

  • if any clause is inconsistent (A & !A), drop it.
  • sort the clauses by size, largest (fewest variables) first.
  • for every minterm in the universal set
    • for every clause in the input
      • for every literal in the term
        • if the minterm is not covered by the literal, continue to the next clause
      • The minterm is covered by the clause:
      • Count the minterm as covered, and continue to the next minterm.
    • The minterm is not covered by any literal; continue to the next minterm.
  • let density = [#covered terms]/[#terms]

If you want to run faster, you will need to hope for a good input. You can try to use binary decision diagrams (BDDs) to encode the current set of encoded minterms, and try to update the binary decision diagram as you add clauses from the input.

A binary decision diagram is a rooted directed acyclic graph such that every node is either a decision node (test a single variable, then take either the false branch or the true branch) or a leaf node (either true or false). For example, XOR can be expressed with this binary decision diagram:

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

Algorithm #2 (Lazy-expanding BDD, more complicated but potentially faster for large amount of variables):

  • if any clause is inconsistent (A & !A), drop it.
  • sort the clauses by size, largest (fewest variables) first.
  • start with an empty BDD (root = false)
  • for every clause
    • update the BDD: start on the root.
    • for every variable:
      • if the clause has no more literals, replace the current node with true (only at the edge along which you came)
        • if the immediate sibling is also true, replace the common parent with true, and repeat this test for the new node.
      • if the current node is true
        • continue to the next clause or recursion branch, or join the sibling thread.
      • if the variable is in the clause and in the current BDD node,
        • descend to the child that intersects the clause.
      • if the variable is in the clause but not in the current BDD node.
        • create a new BDD node
        • set both children to the current node
        • replace the current node with the new node (only at the edge along which you came)
        • descend to the child that intersects the clause.
      • if the variable is in the BDD but not in the clause
        • descend to both children in turn recursively. Alternatively, descend to both children in parallel in separate threads.
      • if the variable is neither in the BDD nor in the clause
        • do nothing.
  • let density = 0/(2^variables) (the denominator signifies the suggested scale for integer computation)
  • every leaf node is either true or false. For every path in the BDD
    • if the leaf node is true
      • let length be the number of non-leaf nodes encountered along the path.
      • add 1/(2^length) to density.
于 2013-02-27T00:12:57.187 に答える