Sample problem solving using PySAT

simple.py

from pysat.formula import CNF, IDPool
from pysat.solvers import Minisat22

n, k = map(int, input().split())
cnf = CNF()
vpool = IDPool(start_from=1)


def bit(i):
    return vpool.id(f'v@{i}')


for i in range(1, n + 1):
    if i <= k:
        cnf.append([bit(i)])
    else:
        cnf.append([-bit(i)])

# print(f'cnf = {cnf.clauses}')

with Minisat22(bootstrap_with=cnf.clauses) as s:
    if s.solve():
        print('SAT')
        answer = ''.join(map(lambda x: '0' if x < 0 else '1', s.get_model()))
        print(answer)
    else:
        print('UNSAT')

assert answer == '1' * k + '0' * (n - k)

test.txt

10 4