# Binarization of Constraints

I am trying to solve a Constraint Satisfaction Problem that involves lots of n-ary constraints. But the solver I have implemented only works with algorithms for binary constraints.

I've been reading into the topic of the biniraztion of constraints (http://ktiml.mff.cuni.cz/~bartak/constraints/binary.html) but I am still not entirely sure how that would work. I thought if someone could help me convert one of the real-world constraints I am dealing with, this could help my understanding.

More specifically:

I have a set of variables: {C1, C2, C3, P}.

Each variable has a domain {0, 1}.

And a constraint: (C1 → (¬C2 ∧ ¬C3 ∧ P)) ∨ (C2 → (¬C1 ∧ ¬C3 ∧ P)) ∨ (C3 → (¬C1 ∧ ¬C2 ∧ P))

How can I convert this constraint into multiple binary constraints?

Introduce a new variable $Q$, whose domain is $\{0000,0001,0010,\dots,1111\}$. It represents the value of $C1,C2,C3,P$. For instance, if $Q=0001$, that means that $C1=0$, $C2=0$, $C3=1$, $P=0$. Then, you add a constraint that the first bit of $Q$ is equal to $C1$ (that's a binary constraint), a constraint that the second bit of $Q$ is equal to $C2$ (another binary constraint), and so on.