同値 ⇔ とは

C言語的には＝＝、　論理学的には　⇔　です。　
 論理回路的には、XOR（排他的論理和）の否定になります。

命題 P	命題 Q	P ⇔ Q
真	真	真
真	偽	偽
偽	真	偽
偽	偽	真

命題 P	命題 Q	P ⊻ Q
真	真	偽
真	偽	真
偽	真	真
偽	偽	偽

では、同値をどのように実装するかというと、排他的論理和の否定からすると
~(~P& Q| P&~Q)
=P&~Q & ~P&Q
となります。または、真理値表から、P＆Q|　~P&~Q でもよいですね。
これをPythonで記述すればよいです。
下のようになります。sは、制約名になります。排他的論理和も同様にして記述できます。
<基数制約の難しさ＞
ちなみにSAT界における基数制約（OR界における基本制約である線形加算不等式制約）も、AND　OR　NOTを用いて、理論的には記述可能です。やってみれば直ぐわかるのですが、加算器というのは、論理回路で普通に合成すると排他的論理和XORのSeaofGatesで、とんでもない量の加算器が必要になります。この原因は、組み合わせ解空間がとんでもなく広いということにあります。ですから基数制約を記述するには、用意されている専用の制約関数を用いることになります。しかし、専用の制約関数はあるのですが、それを用いるからといって、そもそもの組み合わせ解空間が狭くなる訳ではありません。依然としてそのままあります。ですから、基数制約を記述しなくて済むならば、そちらがベターです。
＜UnitPropagation＞
SAT界では、UnitPropagationが重要ですが、EXOR系（同値も）の記述では、これが上手くいきません。ですので、次のような記述の順序が推奨されます。

EXORを含まない論理記述　> 基数制約> EXOR系

下の記述を用いて、かなり難しい制約例を紹介するのですが、あと一回背景知識が必要となります。

def 等号制約(a,b,s):
    sc3.AddHard( (a|~b) &(~a|b),s)