PYSAT Как применить Clausify к объекту Equals при использовании объекта Equals в CNF? ⇐ Python

[Anonymous]

Я использую библиотеку PySat.
Мне нужно показать, что ограничение мощности имеет то же значение истинности, что и другой литерал.
Вот мой код,

Код: Выделить всё

from pysat.card import CardEnc, ITotalizer
from pysat.formula import *

cnf2 = ITotalizer(lits=[1,2,3], ubound=1, top_id=100).cnf
print(cnf2.clauses)
y = Atom(4)
cnf3 = Equals(cnf2, y)
cnf3.clausify()
print(cnf3.clauses)

Вывод:

[[-2, 101], [-1, 101], [-1, -2, 102], [-101, 103], [-102, 104], [-3, 103], [-3, -101, 104]]

[[-12, 4], [12, -4]]

Но равные ограничение полностью игнорирует все предложения, определенные в исходном CNF, случайным образом добавляет новый литерал с именем -12 и использует его. Я не знаю, как решить эту проблему.

Подробнее здесь: https://stackoverflow.com/questions/791 ... t-on-a-cnf