求可求解布尔方程组的软件及clpb自动处理结果的方法

问题背景 #

我正在寻找可求解布尔方程组的软件，已知这是NP难问题，但部分方程可在多项式时间内求解，希望软件能实现指定算法。当前方程组以AND和反相器（AIGER）形式编写，可转换为其他格式。我关注到clpb库，不过在自动提取结果、批量生成解方面有疑问，同时想了解其他可用工具。

CLPB使用问题解答 #

1. 直接判断输入是否全为无关项 #

无需构建真值表，可利用CLPB的taut/1谓词检查约束是否对所有输入组合都成立。将电路逻辑转化为布尔表达式后，验证其永真性即可：

:- use_module(library(clpb)).

% 直接定义id00040对应的布尔表达式
id00040_expr(R1, INP1, INP3, Z, Expr) :-
    Expr = (Z =:= ~INP1 * R1 * ~INP3).

% 检查当R1=0、Z=0时，所有输入是否都满足条件
check_dont_care :-
    id00040_expr(0, INP1, INP3, 0, Expr),
    taut(Expr, IsTautology),
    (IsTautology = true -> writeln("所有输入均为无关项") ; writeln("输入存在约束")).

运行check_dont_care.即可直接得到结论，无需枚举所有解。

2. 自动生成所有解 #

使用Prolog的findall/3谓词收集所有解，再批量输出，避免手动触发：

:- use_module(library(clpb)).
and_gate(X, Y, Z) :- sat(Z =:= (X*Y)).
inverter_gate(X, Z) :- sat(Z =:= ~(X)).

id00040(R1, INP1, INP3, Z) :- 
    inverter_gate(INP1, T1),
    inverter_gate(INP3, T2),
    and_gate(T1, R1, T3),
    and_gate(T2, T3, Z).

generate_all_solutions :-
    findall([INP1, INP3], (id00040(0,INP1,INP3,0), labeling([INP1,INP3])), Solutions),
    writeln("所有解："),
    maplist(writeln, Solutions).

执行generate_all_solutions.会自动打印所有满足条件的输入组合。

其他可用软件包 #

• ABC：专注于AIGER格式布尔电路的工具，支持等价性检查、化简、求解，内置多种高效算法，适合处理大规模电路。
• SAT4J：Java实现的SAT求解库，支持CNF格式，可将AIGER转换为CNF后求解，适合嵌入Java应用。
• Z3定理证明器：通用定理证明工具，支持布尔逻辑、整数、实数等多种理论，可直接处理布尔方程组，提供多语言API（Python、C++等）。
• MiniSat：轻量级高效SAT求解器，是众多工具的基础，需将AIGER转换为CNF格式后使用。

内容的提问来源于stack exchange，提问作者user2317179