私が実際にやろうとしているのは、ブール式を整数線形計画法の制約に変換することです。最初に式を CNF に変換し ( を使用)、次に CNF から制約を作成しようとしてpyedaいます (これは非常に簡単なので)。しかし、.to_ast()関数が出力している抽象構文木を理解するのに苦労しています。.to_ast()例として、式を実行すると(~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2)、出力は次のようになります。
('and', ('or', ('lit', -1), ('lit', -2), ('lit', -3)), ('or', ('lit', -1), ('lit', -2), ('lit', -4)))
-が否定であり、整数が変数の 1 つを表していることは明らかです。整数から変数へのマッピングがあるかどうかは誰にもわかりませんか? 短い質問に対する長い説明...