I have a set of $m$ inequalities with $n$ variables: $$I_j: \sum_{i=1}^n c_ix_i \leq b_i \ , j=1\dots m$$ with the following restrictions: $$x_i \in \{0, 1\}, \ c_i \geq 1, \ b_i \geq 0$$
I want to transform this set into a boolean expression that retains their properties.
For example, given $\ I_1: x_1 + x_2 + x_3 \leq 2 \ $, it can be transformed into $\varphi_1 = ¬x1 \ || \ ¬x2 \ || \ ¬x3$, because the inequality can be read as at most 2 variables must be 1 (or at least 1 variable must be false), therefore, in the boolean expression, at most 2 variables must be true for the expression to be satisfied.
The particular case where $c_i = 1$ is fairly intuitive to encode (I have used a ROBDD to sketch an expression that basically encodes the paths in the tree), but when $c_i \gt 1$, a special relation between variables must be also encoded.
For example, given: $$x + 2y + 3z \leq 5$$ Extra variables might be added: $$x \rightarrow R(x_1) \\ 2y \rightarrow R(x_2, x_3) \\ 3z \rightarrow R(x_4,x_5,x_6)$$ where $R$ is a relation over the smaller subsest of variables (e.g. when $x_2$ is set to some value, $x_3$ is also set to that value).
That was my approach / intuition to this problem, can you give some pointers starting from this?
Typically it takes more than one logic expression to express an inequality.
You need to construct a truth table to extract the logic expressions in conjunctive normal form (CNF) or disjunctive normal form (DNF).
\begin{array}{|c|c|c|c|} \hline z & y & x & x + 2y + 3z \leq 5 \\ \hline 0 & 0 & 0 & 1 \\ \hline 0 & 0 & 1 & 1 \\ \hline 0 & 1 & 0 & 1 \\ \hline 0 & 1 & 1 & 1 \\ \hline 1 & 0 & 0 & 1 \\ \hline 1 & 0 & 1 & 1 \\ \hline 1 & 1 & 0 & 1 \\ \hline 1 & 1 & 1 & 0 \\ \hline \end{array}
Look at the failed values: $z \wedge y \wedge x = 1$ gives a fail ($0$)
Using De Morgan's laws invert the condition so it is not true: $\overline{z \wedge y \wedge x} = \overline{z} \vee \overline{y} \vee \overline{x}$
$\overline{z} \vee \overline{y} \vee \overline{x} = 1$
So if any bit $x,y \, or \, z$ is $0$ the expression will be satisfied.
If there was more than one $0$ in the far right column then that logic expression would have to be ANDed with the first i.e. CNF. e.g. $(\overline{z} \vee \overline{y} \vee \overline{x}) \wedge (expression2) = 1$
In disjunctive normal form (DNF) you OR all the successful conditions:
e.g. $(\overline{z} \wedge \overline{y} \wedge \overline{x}) \vee (\overline{z} \wedge \overline{y} \wedge x) \dots \vee (z \wedge y \wedge \overline{x}) = 1$ only the last table entry fails and is excluded.