Создание булевой формулы на Python

Есть задача поиска максимальных внутренне устойчивых множеств графа методом Магу(дискретная математика в вузе). Задаю граф матрицей смежности(уже реализовал), далее требуется составить булевы формулы где будет конъюнкция всех дизъюнкций отрицаний смежных вершин. То есть например если есть путь из V1 в V2 и из V1 в V3, то в формулу будет включаться (!V1 v !V2) & (!V1 v !V3). Затем данное выражение преобразуется в сокращенную ДНФ, и дальше уже можно смотреть, какие вершины графа отсутствуют в каждой скобке - те вершины как раз образуют данные максимальные внутренне устойчивые множества. Как раз вопрос заключается в том, как составить эту первоначальную булеву формулу, и с помощью чего можно потом упростить эту формулу до сокращенной ДНФ? Предполагаю, что надо пользоваться библиотекой sympy, но я не могу найти какую-то конкретную информацию по моему вопросу... Код на данный момент

import numpy as np
from sympy import *
from sympy.logic.boolalg import And
from sympy.logic.boolalg import Or

print("Введите количество узлов графа:")
amount = int(input())
matrix = np.zeros((amount, amount))
i = 0
j = 0

while i < amount:
    while j < amount:
        print("Введите элемент матрицы", i, j, ":")
        matrix[i, j] = int(input())
        j += 1
    j = 0
    i += 1
print(matrix)