找到一组布尔约束的所有可行解决方案的有效方法答案

【问题标题】：Efficient way of finding all feasible solutions to set of Boolean constrains找到一组布尔约束的所有可行解决方案的有效方法
【发布时间】：2020-11-22 02:50:13
【问题描述】：

我正在用 Python 中的 ortools.sat.python 中的 cp_model 解决以下问题，但我正在寻找更高效的求解器。

问题：

让我们有 n 布尔变量 A, B, C, ...

目标是在满足一组规则的布尔值上找到所有可能/可行的组合。有 3 种规则：

(A, B) 中只有一个可能为真。我将其应用为：

model.AddBoolXOr([A,B])
model.Add(A == False).OnlyEnforceIf(B)
model.Add(B == False).OnlyEnforceIf(A)

(C, D, E) 最多有一个可能为真。我将其应用为：

model.Add(C == False).OnlyEnforceIf(D)
model.Add(C == False).OnlyEnforceIf(E)

model.Add(D == False).OnlyEnforceIf(C)
model.Add(D == False).OnlyEnforceIf(E)

model.Add(E == False).OnlyEnforceIf(C)
model.Add(E == False).OnlyEnforceIf(D)

F 只有在 (A and ~C) or (B and (C or E)) 时才有可能。首先，我将其转换为 CNF：(A or B) and (B or ~C) and (A or C or E)。然后我将它插入到模型中：

model.Add(F == False).OnlyEnforceIf([A.Not(), B.Not()])
model.Add(F == False).OnlyEnforceIf([B.Not(), C])
model.Add(F == False).OnlyEnforceIf([A.Not(), C.Not(), E.Not()])

上面的结果如下：

1 0 0 0 0 0 
1 0 1 0 0 0 
1 0 0 1 0 0 
1 0 0 0 1 0 
1 0 0 0 1 1 
1 0 0 0 0 1 
1 0 0 1 0 1 
0 1 0 0 1 1 
0 1 0 0 1 0 
0 1 0 0 0 0 
0 1 0 1 0 0 
0 1 1 0 0 0 
0 1 1 0 0 1

由于我的问题很大，我正在寻找更有效的解决方案。我找到了minisat，但我不确定是否可以在 DIMACS 表单中表达上述约束并让 minisat 计算所有可行的解决方案（默认情况下它首先找到并停止）。

有没有可以解决此类问题的求解器？

【问题讨论】：

标签： combinations combinatorics or-tools sat

【解决方案1】：

编写模型的方式多么复杂。

model.Add(a + b == 1)

或

model.AddBoolOr([a, b])
model.AddImplication(a, b.Not())
model.AddImplication(b, a.Not())

model.Add(c + d + e <= 1)

或

model.AddImplication(c, d.Not())
model.AddImplication(c, e.Not())
model.AddImplication(d, c.Not())
model.AddImplication(d, e.Not())
model.AddImplication(e, c.Not())
model.AddImplication(e, d.Not())

为每个和创建 1 个布尔变量

(A 和 ~C) G

model.AddImplication(G, A)
model.AddImplication(G, C.Not())
model.AddBoolOr([A.Not(), C, G.Not())

那么 F 只有在 x1 或 x2 或 x3 时才可能

model.AddBoolOr([F.Not(), x1, x2, x3])

【讨论】：