How to find optimal solution( with least number of True value ) from set of solution ?

[CS17B011]

I am using this tool to automate APIs. For that, we are defining some rules using boolean expressions. For example, say these are the rules :

A iff (B or C)
B impl not C
D impl E,
F iff (G or H)

Now I am putting each symbol as constrain as 1, and trying to find a solution that satisfies all the rules. For that I am creating a final rule by joining them with 'and'.

Let's say I put A = 1, so I want a solution that has minimal 1's. Example

A=1,B=1,C=0,D=0,E=0,F=0,G=0,H=0

But from your module I am getting this solution after using sat_one() method:

A=1,B=1,C=0,D=0,E=1,F=0,G=0,H=0

How to find the optimal one? Also, I have large number of operands so looping through each solution is not possible. Please help me on this topic.

[welchbj]

So I think I understand your goal. Let me know if this is achieving what you want (using latest ttable from PyPI on CPython 3.8):

>>> import itertools
>>> from tt import BooleanExpression
>>>
>>> clauses = ['A iff (B or C)', 'B impl not C', 'D impl E', 'F iff (G or H)']
>>> expr_str = ' and '.join(f'({clause})' for clause in clauses)
>>> expr = BooleanExpression(expr_str)
>>> expr
<BooleanExpression "(A iff (B or C)) and (B impl not C) and (D impl E) and (F iff (G or H))">
>>>
>>> base_constraints = dict(A=1)
>>> free_symbols = [s for s in expr.symbols if s not in base_constraints.keys()]
>>> free_symbols
['B', 'C', 'D', 'E', 'F', 'G', 'H']
>>>
>>> for i in range(len(free_symbols), 0, -1):
...     for combo in itertools.combinations(free_symbols, i):
...         constraints = {symbol: 0 for symbol in combo}
...         constraints.update(base_constraints)
...         with expr.constrain(**constraints):
...             sol = expr.sat_one()
...             if sol is not None:
...                 print(sol)
...                 break
...     else:
...         continue
...     break
...
A=1, B=0, C=1, D=0, E=0, F=0, G=0, H=0

This is at least further constraining the search space before finding solutions rather than iterating over all solutions to find the global minimum with respect to your criteria, which should be more performant than iterating over the entire solution space with sat_all().

[welchbj]

I'm going to close this, feel free to re-open if needed.