Python 的布尔函数优化器包

Question

我想以表格形式定义一个布尔函数（具有 n 个输入和 m 个输出）。我想找到一个实现该函数的最佳布尔表达式。这里的最佳意味着，在硬件中实现它需要尽可能少的门（可能每个门都有不同的成本）

我确信 VHDL/Verilog 合成器经常进行这种优化，我基本上出于同样的原因需要它。有某种卡诺求解器吗？或者，是否可以将问题指定为经典优化问题（SAT，整数规划）？我想用 Python 实现它，所以我主要是在寻找一个已经可以做到这一点的包。

Answer 1

寻找最佳解决方案的算法具有指数复杂度，因此通常可用的工具寻找良好的实现而不是最佳实现。我不确定你的要求有多严格，或者你的功能有多大。

一种逻辑优化算法是Quine-McCluskey。有一个 python 实现。但是，这仅涵盖单个输出情况。

$ ./qm.py -o 1,2,3
1X X1
$ ./qm.py -o 1,2
10 01
$ ./qm.py -o 0,15
1111 0000
$ ./qm.py -o 0,8,15
1111 X000

对于多个输出，最简单的策略是单独实现每个输出。它们之间可能存在一些重复的术语，可以轻松共享；构建最大化共享的逻辑更加困难。

Answer 2

Espresso 启发式逻辑最小化器是一款备受推崇的用于最小化布尔函数的工具，并支持 n-m 个输入输出。它来自 20 世纪 80 年代，用 C 语言编写，最后一次正式发布是在 1990 年代。我寻找更新的工具，但似乎这个领域相当模糊 - 我找不到同时更可靠和更可用的工具。正如您提到的，电路设计中有高质量的实现，但它们通常与综合语言相关，并且不容易独立使用。同样，Quine-McCluskey 有许多手工实现，例如使用 Petrick 方法 的一种实现，但它们缺乏功能且算法不那么健壮。

对于 Espresso，pyeda 中有一个 Python 绑定，但对我来说，与仅将 espresso 作为外部命令运行相比，该绑定似乎过于复杂且无文档（手册页 1、5）。由于我在 Linux 上，我使用了 classabbyamp/espresso-logic，但是对于 Windows，您可能会使用 Gigantua 的 Visual Studio 项目。我提到的所有存储库都显示出被遗弃的迹象。您可能需要进行一些搜索以避免位腐烂并找到可用的版本。构建二进制文件后，可以直接编写一些字符串操作以将数据传入/传出 Espresso PLA 格式，然后将 espresso 二进制文件作为外部命令运行。我必须运行大约一百个这样的问题，因此编写脚本比手动完成每个实例更好，但我仍然检查每个结果。

import subprocess

input = """
.i 3
.o 2
.type fr
11- 10
1-1 10
0-- 01
-00 01
"""

with open('input.txt', 'w') as f:
  f.write(input)

result = subprocess.run(['espresso-logic/bin/espresso', '-oeqntott', 'input.txt'], capture_output=True, text=True).stdout
print(result)
# v3.0 = (v0&v2) | (v0&v1);
# v3.1 = (!v1&!v2) | (!v0);

一个问题是 Espresso 只能找到最小乘积和形式 - 例如，它找不到像

v3.0 = (v0 & (v1 | v2))

这样的结构化公式。所以我也通过 Sympy 运行输出：

from sympy.parsing.sympy_parser import parse_expr, auto_symbol
from sympy import pretty

for var in result.splitlines():
  if var == "":
    continue
  eqn = var.split(" = ")[1][:-1].replace("!","~")
  eqn = parse_expr(eqn, transformations=(auto_symbol,))
  print(pretty(eqn.simplify()))
# v₀ ∧ (v₁ ∨ v₂)
# (¬v₁ ∧ ¬v₂) ∨ ¬v₀

如果您想将

v0

更改为更有用的东西，您可以替换 auto_symbol 挂钩。 sympy 有多种漂亮的打印机 - 这里我使用

pretty

作为示例，但很可能您会使用特定于语言的打印机，例如

ccode

。

sympy 中实际上有一个 SOP 最小化的实现，

sympy.logic.boolalg.SOPform

，但与 espresso 相比，它缺少一些功能，比如不关心输入（

-

）和多个输出，而且我不认为该算法是一样坚固。如果你想要纯Python，值得考虑。