Template for the "Minimal Boolean formula synthesis" problem

bf.py

from pysat.formula import CNF, IDPool
from pysat.solvers import Minisat22 as Solver
from enum import Enum

NodeType = Enum("NodeType", "VAR AND OR NOT")


class BFSynthesizer:
    def __init__(self, n: int, tt: str, P: int):
        assert len(tt) == 2 ** n, "Incorrect truth table size"

        self.n = n  # Number of variables
        self.tt = tt  # Truth table (binary string)
        self.P = P  # Parse tree size (number of nodes)
        self.vpool = IDPool(start_from=1)
        self.cnf = CNF()

    def nodeType(self, i: int, t: NodeType) -> int:
        # t -- node type
        return self.vpool.id(f"nodeType@{i}@{t.name}")

    def nodeVariable(self, i: int, x: int) -> int:
        # x -- variable index (1..n) (or 0, if node type is not VAR)
        return self.vpool.id(f"nodeInputVariable@{i}@{x}")

    def nodeParent(self, i: int, p: int) -> int:
        # p -- parent index (1..n), but it is advisable to encode (p < i)
        return self.vpool.id(f"nodeParent@{i}@{p}")

    def nodeChild(self, i: int, c: int) -> int:
        # c -- child index (1..n), but it is advisable to encode (c > i)
        return self.vpool.id(f"nodeChild@{i}@{c}")

    def nodeValue(self, i: int, u: int) -> int:
        # u -- "input" number
        # "input" = valuation of variables = truth table row
        # Examples of "input"s:
        #  (0,1,1) = 3
        #  (1,0,1) = 5
        #  (1,1,1,0,0) = 28
        return self.vpool.id(f"nodeValue@{i}@{u}")

    def declareConstraints(self) -> int:
        # TODO: self.cnf.append(...)
        # Add constraints: encode the parse tree structure and its relation with the truth table.
        # Do not forget to encode ALO/AMO (AtLeastOne/AtMostOne) for necessary variables!
        pass

    def solve(self) -> bool:
        with Solver(bootstrap_with=self.cnf.clauses) as s:
            if s.solve():
                # Here you can get model and build an actual Boolean formula from the
                # satisfying assignment, but in this problem you only have to output
                # the size of the minimal Boolean formula, not the formula itself.
                return True
            else:
                return False


def main():
    n = int(input())  # Number of variables
    tt = input()  # Truth table

    for P in range(1, 30 + 1):
        synthesizer = BFSynthesizer(n, tt, P)
        synthesizer.declareConstraints()
        if synthesizer.solve():
            print(P)
            break
    else:
        print(0)


if __name__ == "__main__":
    main()