What's CNF for "n of m variables true?"

code.py

from sympy import symbols
import sympy.logic.boolalg as form
from itertools import combinations
from functools import reduce
from textwrap import indent
import time
import operator
import pycosat
import json

def no_more_than(num_true, total):
    print(f"{num_true} true of {total} total:")
    strs = map(str,range(1, total+1))
    symbs = symbols(",".join(strs))
    exprs = []

    # enumerate the ways for there to be _num_true + 1_ true variables
    for one_too_many in combinations(symbs, num_true + 1):
        exprs.append(reduce(operator.and_, one_too_many))

    # or them together and negate the result
    unaltered = ~reduce(operator.or_, exprs)
    print("  expr:")
    print(indent(str(unaltered), prefix="    "))

    # convert to cnf
    before = time.time()
    altered = form.to_cnf(unaltered, simplify=True, force=True)
    after = time.time()
    duration = after - before
    print(f"  cnf ({duration} sec):")
    print(indent(str(altered), prefix="    "))

    # convert to solver format
    cnfstr = str(altered)
    for target, result in [("(", "["), (")", "]"), ("|", ","), ("&", ","), ("~", "-")]:
        cnfstr = cnfstr.replace(target, result)
    solviter = pycosat.itersolve(json.loads("[{}]".format(cnfstr)))

    # print solutions
    print("  solutions:")
    solutions = []
    try:
        while(True):
            soln = next(solviter)
            simp = [x for x in soln if x > 0]
            solutions.append(simp)
    except StopIteration:
       pass
    print(solutions)
    print()

no_more_than(2,4)
no_more_than(3,9)

output.txt

2 true of 4 total:
  expr:
    ~((1 & 2 & 3) | (1 & 2 & 4) | (1 & 3 & 4) | (2 & 3 & 4))
  cnf (0.040136098861694336 sec):
    (~1 | ~2 | ~3) & (~1 | ~2 | ~4) & (~1 | ~3 | ~4) & (~2 | ~3 | ~4)
  solutions:
[[], [4], [3], [3, 4], [2, 3], [2, 4], [2], [1, 2], [1], [1, 4], [1, 3]]

3 true of 9 total:
  expr:
    ~((1 & 2 & 3 & 4) | (1 & 2 & 3 & 5) | (1 & 2 & 3 & 6) | (1 & 2 & 3 & 7) | (1 & 2 & 3 & 8) | (1 & 2 & 3 & 9) | (1 & 2 & 4 & 5) | (1 & 2 & 4 & 6) | (1 & 2 & 4 & 7) | (1 & 2 & 4 & 8) | (1 & 2 & 4 & 9) | (1 & 2 & 5 & 6) | (1 & 2 & 5 & 7) | (1 & 2 & 5 & 8) | (1 & 2 & 5 & 9) | (1 & 2 & 6 & 7) | (1 & 2 & 6 & 8) | (1 & 2 & 6 & 9) | (1 & 2 & 7 & 8) | (1 & 2 & 7 & 9) | (1 & 2 & 8 & 9) | (1 & 3 & 4 & 5) | (1 & 3 & 4 & 6) | (1 & 3 & 4 & 7) | (1 & 3 & 4 & 8) | (1 & 3 & 4 & 9) | (1 & 3 & 5 & 6) | (1 & 3 & 5 & 7) | (1 & 3 & 5 & 8) | (1 & 3 & 5 & 9) | (1 & 3 & 6 & 7) | (1 & 3 & 6 & 8) | (1 & 3 & 6 & 9) | (1 & 3 & 7 & 8) | (1 & 3 & 7 & 9) | (1 & 3 & 8 & 9) | (1 & 4 & 5 & 6) | (1 & 4 & 5 & 7) | (1 & 4 & 5 & 8) | (1 & 4 & 5 & 9) | (1 & 4 & 6 & 7) | (1 & 4 & 6 & 8) | (1 & 4 & 6 & 9) | (1 & 4 & 7 & 8) | (1 & 4 & 7 & 9) | (1 & 4 & 8 & 9) | (1 & 5 & 6 & 7) | (1 & 5 & 6 & 8) | (1 & 5 & 6 & 9) | (1 & 5 & 7 & 8) | (1 & 5 & 7 & 9) | (1 & 5 & 8 & 9) | (1 & 6 & 7 & 8) | (1 & 6 & 7 & 9) | (1 & 6 & 8 & 9) | (1 & 7 & 8 & 9) | (2 & 3 & 4 & 5) | (2 & 3 & 4 & 6) | (2 & 3 & 4 & 7) | (2 & 3 & 4 & 8) | (2 & 3 & 4 & 9) | (2 & 3 & 5 & 6) | (2 & 3 & 5 & 7) | (2 & 3 & 5 & 8) | (2 & 3 & 5 & 9) | (2 & 3 & 6 & 7) | (2 & 3 & 6 & 8) | (2 & 3 & 6 & 9) | (2 & 3 & 7 & 8) | (2 & 3 & 7 & 9) | (2 & 3 & 8 & 9) | (2 & 4 & 5 & 6) | (2 & 4 & 5 & 7) | (2 & 4 & 5 & 8) | (2 & 4 & 5 & 9) | (2 & 4 & 6 & 7) | (2 & 4 & 6 & 8) | (2 & 4 & 6 & 9) | (2 & 4 & 7 & 8) | (2 & 4 & 7 & 9) | (2 & 4 & 8 & 9) | (2 & 5 & 6 & 7) | (2 & 5 & 6 & 8) | (2 & 5 & 6 & 9) | (2 & 5 & 7 & 8) | (2 & 5 & 7 & 9) | (2 & 5 & 8 & 9) | (2 & 6 & 7 & 8) | (2 & 6 & 7 & 9) | (2 & 6 & 8 & 9) | (2 & 7 & 8 & 9) | (3 & 4 & 5 & 6) | (3 & 4 & 5 & 7) | (3 & 4 & 5 & 8) | (3 & 4 & 5 & 9) | (3 & 4 & 6 & 7) | (3 & 4 & 6 & 8) | (3 & 4 & 6 & 9) | (3 & 4 & 7 & 8) | (3 & 4 & 7 & 9) | (3 & 4 & 8 & 9) | (3 & 5 & 6 & 7) | (3 & 5 & 6 & 8) | (3 & 5 & 6 & 9) | (3 & 5 & 7 & 8) | (3 & 5 & 7 & 9) | (3 & 5 & 8 & 9) | (3 & 6 & 7 & 8) | (3 & 6 & 7 & 9) | (3 & 6 & 8 & 9) | (3 & 7 & 8 & 9) | (4 & 5 & 6 & 7) | (4 & 5 & 6 & 8) | (4 & 5 & 6 & 9) | (4 & 5 & 7 & 8) | (4 & 5 & 7 & 9) | (4 & 5 & 8 & 9) | (4 & 6 & 7 & 8) | (4 & 6 & 7 & 9) | (4 & 6 & 8 & 9) | (4 & 7 & 8 & 9) | (5 & 6 & 7 & 8) | (5 & 6 & 7 & 9) | (5 & 6 & 8 & 9) | (5 & 7 & 8 & 9) | (6 & 7 & 8 & 9))
  cnf (66.46701049804688 sec):
    (~1 | ~2 | ~3 | ~4) & (~1 | ~2 | ~3 | ~5) & (~1 | ~2 | ~3 | ~6) & (~1 | ~2 | ~3 | ~7) & (~1 | ~2 | ~3 | ~8) & (~1 | ~2 | ~3 | ~9) & (~1 | ~2 | ~4 | ~5) & (~1 | ~2 | ~4 | ~6) & (~1 | ~2 | ~4 | ~7) & (~1 | ~2 | ~4 | ~8) & (~1 | ~2 | ~4 | ~9) & (~1 | ~2 | ~5 | ~6) & (~1 | ~2 | ~5 | ~7) & (~1 | ~2 | ~5 | ~8) & (~1 | ~2 | ~5 | ~9) & (~1 | ~2 | ~6 | ~7) & (~1 | ~2 | ~6 | ~8) & (~1 | ~2 | ~6 | ~9) & (~1 | ~2 | ~7 | ~8) & (~1 | ~2 | ~7 | ~9) & (~1 | ~2 | ~8 | ~9) & (~1 | ~3 | ~4 | ~5) & (~1 | ~3 | ~4 | ~6) & (~1 | ~3 | ~4 | ~7) & (~1 | ~3 | ~4 | ~8) & (~1 | ~3 | ~4 | ~9) & (~1 | ~3 | ~5 | ~6) & (~1 | ~3 | ~5 | ~7) & (~1 | ~3 | ~5 | ~8) & (~1 | ~3 | ~5 | ~9) & (~1 | ~3 | ~6 | ~7) & (~1 | ~3 | ~6 | ~8) & (~1 | ~3 | ~6 | ~9) & (~1 | ~3 | ~7 | ~8) & (~1 | ~3 | ~7 | ~9) & (~1 | ~3 | ~8 | ~9) & (~1 | ~4 | ~5 | ~6) & (~1 | ~4 | ~5 | ~7) & (~1 | ~4 | ~5 | ~8) & (~1 | ~4 | ~5 | ~9) & (~1 | ~4 | ~6 | ~7) & (~1 | ~4 | ~6 | ~8) & (~1 | ~4 | ~6 | ~9) & (~1 | ~4 | ~7 | ~8) & (~1 | ~4 | ~7 | ~9) & (~1 | ~4 | ~8 | ~9) & (~1 | ~5 | ~6 | ~7) & (~1 | ~5 | ~6 | ~8) & (~1 | ~5 | ~6 | ~9) & (~1 | ~5 | ~7 | ~8) & (~1 | ~5 | ~7 | ~9) & (~1 | ~5 | ~8 | ~9) & (~1 | ~6 | ~7 | ~8) & (~1 | ~6 | ~7 | ~9) & (~1 | ~6 | ~8 | ~9) & (~1 | ~7 | ~8 | ~9) & (~2 | ~3 | ~4 | ~5) & (~2 | ~3 | ~4 | ~6) & (~2 | ~3 | ~4 | ~7) & (~2 | ~3 | ~4 | ~8) & (~2 | ~3 | ~4 | ~9) & (~2 | ~3 | ~5 | ~6) & (~2 | ~3 | ~5 | ~7) & (~2 | ~3 | ~5 | ~8) & (~2 | ~3 | ~5 | ~9) & (~2 | ~3 | ~6 | ~7) & (~2 | ~3 | ~6 | ~8) & (~2 | ~3 | ~6 | ~9) & (~2 | ~3 | ~7 | ~8) & (~2 | ~3 | ~7 | ~9) & (~2 | ~3 | ~8 | ~9) & (~2 | ~4 | ~5 | ~6) & (~2 | ~4 | ~5 | ~7) & (~2 | ~4 | ~5 | ~8) & (~2 | ~4 | ~5 | ~9) & (~2 | ~4 | ~6 | ~7) & (~2 | ~4 | ~6 | ~8) & (~2 | ~4 | ~6 | ~9) & (~2 | ~4 | ~7 | ~8) & (~2 | ~4 | ~7 | ~9) & (~2 | ~4 | ~8 | ~9) & (~2 | ~5 | ~6 | ~7) & (~2 | ~5 | ~6 | ~8) & (~2 | ~5 | ~6 | ~9) & (~2 | ~5 | ~7 | ~8) & (~2 | ~5 | ~7 | ~9) & (~2 | ~5 | ~8 | ~9) & (~2 | ~6 | ~7 | ~8) & (~2 | ~6 | ~7 | ~9) & (~2 | ~6 | ~8 | ~9) & (~2 | ~7 | ~8 | ~9) & (~3 | ~4 | ~5 | ~6) & (~3 | ~4 | ~5 | ~7) & (~3 | ~4 | ~5 | ~8) & (~3 | ~4 | ~5 | ~9) & (~3 | ~4 | ~6 | ~7) & (~3 | ~4 | ~6 | ~8) & (~3 | ~4 | ~6 | ~9) & (~3 | ~4 | ~7 | ~8) & (~3 | ~4 | ~7 | ~9) & (~3 | ~4 | ~8 | ~9) & (~3 | ~5 | ~6 | ~7) & (~3 | ~5 | ~6 | ~8) & (~3 | ~5 | ~6 | ~9) & (~3 | ~5 | ~7 | ~8) & (~3 | ~5 | ~7 | ~9) & (~3 | ~5 | ~8 | ~9) & (~3 | ~6 | ~7 | ~8) & (~3 | ~6 | ~7 | ~9) & (~3 | ~6 | ~8 | ~9) & (~3 | ~7 | ~8 | ~9) & (~4 | ~5 | ~6 | ~7) & (~4 | ~5 | ~6 | ~8) & (~4 | ~5 | ~6 | ~9) & (~4 | ~5 | ~7 | ~8) & (~4 | ~5 | ~7 | ~9) & (~4 | ~5 | ~8 | ~9) & (~4 | ~6 | ~7 | ~8) & (~4 | ~6 | ~7 | ~9) & (~4 | ~6 | ~8 | ~9) & (~4 | ~7 | ~8 | ~9) & (~5 | ~6 | ~7 | ~8) & (~5 | ~6 | ~7 | ~9) & (~5 | ~6 | ~8 | ~9) & (~5 | ~7 | ~8 | ~9) & (~6 | ~7 | ~8 | ~9)
  solutions:
[[], [9], [8], [8, 9], [7, 8], [7, 8, 9], [7], [7, 9], [6, 7], [6, 7, 9], [6, 7, 8], [6, 8, 9], [6, 8], [6, 9], [6], [5, 6, 9], [5, 6], [5, 6, 8], [5, 6, 7], [5, 7], [5, 7, 9], [5, 7, 8], [5, 8, 9], [5, 8], [5, 9], [5], [4, 5, 9], [4, 5], [4, 5, 8], [4, 5, 7], [4, 5, 6], [4, 6], [4, 6, 9], [4, 6, 8], [4, 6, 7], [4, 7], [4, 7, 9], [4, 7, 8], [4, 8, 9], [4, 8], [4, 9], [4], [3, 4, 9], [3, 4], [3, 4, 8], [3, 4, 7], [3, 4, 6], [3, 4, 5], [3, 5], [3, 5, 9], [3, 5, 8], [3, 5, 7], [3, 5, 6], [3, 6], [3, 6, 9], [3, 6, 8], [3, 6, 7], [3, 7], [3, 7, 9], [3, 7, 8], [3, 8, 9], [3, 8], [3, 9], [3], [2, 3, 9], [2, 3], [2, 3, 8], [2, 3, 7], [2, 3, 6], [2, 3, 5], [2, 3, 4], [2, 4], [2, 4, 9], [2, 4, 8], [2, 4, 7], [2, 4, 6], [2, 4, 5], [2, 5], [2, 5, 9], [2, 5, 8], [2, 5, 7], [2, 5, 6], [2, 6], [2, 6, 9], [2, 6, 8], [2, 6, 7], [2, 7], [2, 7, 9], [2, 7, 8], [2, 8, 9], [2, 8], [2, 9], [2], [1, 2, 9], [1, 2], [1, 2, 8], [1, 2, 7], [1, 2, 6], [1, 2, 5], [1, 2, 4], [1, 2, 3], [1, 3], [1, 3, 9], [1, 3, 8], [1, 3, 7], [1, 3, 6], [1, 3, 5], [1, 3, 4], [1, 4], [1, 4, 9], [1, 4, 8], [1, 4, 7], [1, 4, 6], [1, 4, 5], [1, 5], [1, 5, 9], [1, 5, 8], [1, 5, 7], [1, 5, 6], [1, 6], [1, 6, 9], [1, 6, 8], [1, 6, 7], [1, 7], [1, 7, 9], [1, 7, 8], [1, 8, 9], [1, 8], [1, 9], [1]]

thoughts

2,3 -> 3,9 saw a 41x increase in output size, and a 165x increase in computation time
For larger expressions it will be necessary to look at sympy's output for small expressions, guess the pattern, and write code to generate it directly.
Is there a better way?

If you know how this can be done faster, please suggest a strategy here:

https://stackoverflow.com/questions/66836239/how-can-i-shortcut-a-slow-conversion-to-cnf?noredirect=1#comment118143484_66836239