# convert biconditional to pseudo-boolean (inequality / equation) constraints

I am working with pseudo-Boolean and I want to convert the bi-conditional $$(a \land b) \iff c$$ to inequality or equation.

my attempt was.

First, convert the bi-conditional to two implies $$((a \land b) \to c) \land (c \to (a \land b))$$ Then $$(\lnot(a \land b) \lor c ) \land (\lnot c \lor (a \land b))$$ Then, the left side part become $$(\lnot a \lor\lnot b\lor c)$$ and the right hand side part become $$((\lnot c \lor a) \land (\lnot c \lor b))$$ but to convert the right hand side part to constraints effected negatively on the pseudo-Boolean results.

So, my question is, am I correct in these previous steps or not?

A pseudo Boolean constraint is a constraint of the form, where $$w_i$$ are the weights, $$x_i$$ the Boolean variables, $$k$$ some comparison value and $$\#$$ some comparison operator:

$$\sum_{i=1}^n w_i x_i\,\#\,k$$

Since disjunction $$x_1 \lor .. \lor x_n$$ corresponds to the pseudo Boolean constraint $$1 x_1 + ... + 1 x_n \geq 1$$ and taking the negation of a boolean variable $$x$$ amounts to computing $$1-x$$ we can translate your Boolean formula into multiple pseudo Boolean constraints.

Since in conjunctive normal form your Boolean formula $$(a \land b) \iff c$$ amounts to the Boolean formula $$(\lnot a\lor\lnot b\lor c)\land(\lnot c\lor a)\land(\lnot c\lor b)$$ we can translate each clause and get:

$$(1-a)+(1-b)+c\geq 1$$

$$(1-c)+a\geq 1$$

$$(1-c)+b\geq 1$$

Or braught in the weighted sum form:

$$-1 a + -1 b + 1 c\geq -1$$

$$1 a + -1 c\geq 0$$

$$1 b + -1 c\geq 0$$

I dont know whether the alternate form, disjunctive normal form would be useful at all.

So, my question is, am I correct in these previous steps or not?

You are correct. By definition $$X\leftrightarrow Y\equiv (\lnot X\lor Y)\land(\lnot Y\lor X)$$, so... $$(a\land b)\leftrightarrow c ~\equiv~ (\lnot a\lor\lnot b\lor c)\land(\lnot c\lor a)\land(\lnot c\lor b)$$

Using the alternate definition that $$X\leftrightarrow Y \equiv (X\land Y)\lor(\lnot X\land\lnot Y)$$, will give... $$(a\land b)\leftrightarrow c ~\equiv~ ( a\land b\land c)\lor(\lnot a\land\lnot c)\lor(\lnot b\land\lnot c)$$