Минимизация СКНФ (совершенной конъюнктивной нормальной формы) обычно выполняется с помощью алгоритма Куайна-Мак-Класки (QM) или алгоритма Эспрессо. Вот реализация алгоритма Куайна-Мак-Класки на Python:
from itertools import combinations

def min_terms_to_binary(min_terms, n_vars):
    return [bin(mt)[2:].zfill(n_vars) for mt in min_terms]

def find_pair_groups(binary_min_terms):
    groups = [[] for _ in range(len(binary_min_terms[0]) + 1)]
    for bmt in binary_min_terms:
        groups[bmt.count('1')].append(bmt)
    return groups

def is_pairable(mt1, mt2):
    diff = 0
    for b1, b2 in zip(mt1, mt2):
        if b1 != b2:
            diff += 1
    return diff == 1

def pair(mt1, mt2):
    return ''.join([b1 if b1 == b2 else '-' for b1, b2 in zip(mt1, mt2)])

def qm_step(groups):
    new_groups = [[] for _ in range(len(groups) - 1)]
    paired = {mt: False for group in groups for mt in group}

    for i, group in enumerate(groups[:-1]):
        for mt1, mt2 in itertools.product(group, groups[i + 1]):
            if is_pairable(mt1, mt2):
                new_groups[i].append(pair(mt1, mt2))
                paired[mt1] = paired[mt2] = True

    primes = {mt for group in groups for mt in group if not paired[mt]}
    new_groups = [sorted(set(group)) for group in new_groups]

    return new_groups, primes

def qm(binary_min_terms):
    groups = find_pair_groups(binary_min_terms)
    primes = set()

    while any(groups):
        new_groups, new_primes = qm_step(groups)
        groups = new_groups
        primes |= new_primes

    return primes

def petrick_method(primes, min_terms):
    covers = [{prime for prime in primes if mt in prime} for mt in min_terms]
    product = [covers[0]]

    for cover in covers[1:]:
        new_product = []
        for prime_set1, prime_set2 in itertools.product(product, cover):
            new_product.append(prime_set1 | prime_set2)
        product = new_product

    min_cover = min(product, key=lambda x: len(x))
    return sorted(min_cover)

def binary_to_formula(binary_min_terms, variables):
    def literal(var, value):
        return var if value == '1' else f'~{var}'

    def term(binary_min_term):
        return ''.join([literal(var, value) for var, value in zip(variables, binary_min_term) if value != '-'])

    return ' + '.join([term(binary_min_term) for binary_min_term in binary_min_terms])

def minimize_sknf(formula, variables):
    min_terms = [int(mt) for mt in formula.split(' + ')]
    binary_min_terms = min_terms_to_binary(min_terms, len(variables))
    primes = qm(binary_min_terms)
    cover = petrick_method(primes, binary_min_terms)
    return binary_to_formula(cover, variables)

# Usage example:
formula = '1 + 2 + 3 + 5 + 6 + 7'
variables = ['x1', 'x2', 'x3']
minimized_formula = minimize_sknf(formula, variables)
print(minimized_formula)

Пример кода выше реализует алгоритм Куайна-Мак-Класки для минимизации СКНФ. Функция `minimize_sknf` принимает на вход формулу в виде строки и список переменных. В качестве примера использования, формула '1 + 2 + 3 + 5 + 6 + 7' будет минимизирована с использованием переменных ['x1', 'x2', 'x3'].

Обратите внимание, что алгоритм Куайна-Мак-Класки может быть неэффективным для больших и сложных формул. В таких случаях рекомендуется использовать более продвинутые алгоритмы, такие как алгоритм Эспрессо.