CODEWITHSUNDEEP
combinationscombinatoricsor-toolscp-sat
gozwei
gozwei

Reputation: 730

Efficient way of finding all feasible solutions to set of Boolean constrains

I'm solving the following problem with cp_model from ortools.sat.python in Python, but I'm looking for a more efficient solver.

Problem:

Let's have n boolean variables A, B, C, ...

The goal is to find all possible/feasible combinations on boolean values that satisfy a set of rules. There are 3 types of rules:

  1. One and only one of (A, B) might be true. I'm applying this as:
model.AddBoolXOr([A,B])
model.Add(A == False).OnlyEnforceIf(B)
model.Add(B == False).OnlyEnforceIf(A)
  1. At most one of (C, D, E) might be true. I'm applying this as:
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)
  1. F is only possible when (A and ~C) or (B and (C or E)). First I'm converting this to CNF: (A or B) and (B or ~C) and (A or C or E). Then I insert that to the model:
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()])

The result for above looks like:

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

Since my problem is big, I'm looking for a more efficient solution. I found minisat but I'm not sure if it is possible to express the above constraints in the DIMACS form and make minisat calculate all feasible solutions (by default it finds first and stops).

Is there any there solver capable of solving such a problem?

Upvotes: 0

Views: 197

Answers (1)

Laurent Perron
Laurent Perron

Reputation: 11014

what a convoluted way of writing the model.

1)

model.Add(a + b == 1)

or

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

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

or

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())

Create 1 bool var for each and

(A and ~C) <=> G

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

then F is only possible if x1 or x2 or x3

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

Upvotes: 1

Related Questions