An answer from a yes/no helper

A formula has variables x₁ … xₙ and a list of clauses. A clause is a list of literals: k means “xₖ is True” and -k means “xₖ is False”, and a clause holds when at least one of its literals holds. You are given a helper sat(formula) that answers only True or False: can some assignment make every clause of formula hold?

Return an assignment as a list of n values, answer[k - 1] for xₖ, that makes every clause hold, or None if there is none. Call sat at most n + 1 times.

find_assignment(2, [[1, 2], [-1]], sat)   # [False, True]
find_assignment(1, [[1], [-1]], sat)      # None

Each test reports two facts: whether your answer is right ('satisfied', or 'no assignment' for None), and whether sat was called at most n + 1 times. Any right assignment passes.

Limits

• Up to 60 variables, so trying all 2ⁿ assignments (n twos multiplied together) is impossible.
• Give sat a list of clauses, each a list of literals from 1 to n or −1 to −n.