References to publications on representation of any boolean function as a system of linear inequalities

Question

It is known that any boolean function may be represented, in some sense, as a system of linear inequalities. But my rather intensive literature search brought a little references. I will appreciate any relevant references! I'm looking for references to sci. books, papers etc. on the subject!

The thing is that recently, I understood how to represent any boolean function $f(\mathbf{x})$ as an irreducible system of linear inequalities in the following sense. Let $B^n\doteq\left\{(x_1,x_2,\ldots, x_n): x_k\in\{0,1\}\right\}\subset R^n$ be a set of all vertices of an $n$-dimensional unit cube, i.e. the set of all 0-1 arguments of some boolean function $f: B^n\to\{0,1\}$.

Then there exists a system of linear inequalities of $n+1$ variables $(\mathbf{x},y)$: $$S(\mathbf{x},y)=\{a_i+l_i(\mathbf{x}) + b_iy \geqslant 0: i=1,\ldots,m\}$$ (where $a_i, b_i$, $b_i\neq0$ are scalars, and $l_i(\mathbf{x})$ are linear functions of $n$ variables) such that $$\forall\mathbf{x}\in B^n:\left\{f(\mathbf{x})=y\right\}\iff\left\{a_i+ l_i(\mathbf{x})+b_iy \geqslant 0:i=1,\ldots,m\right\}$$ i.e. for any $\mathbf{x}\in B^n$, $f(\mathbf{x})=y$ if and only if $S(\mathbf{x},y)$ holds.

It is important that we do not need to assume that $y$ is a discrete, 0-1, variable! For any 0-1 vector $\mathbf{x}$, the system $S(\mathbf{x},y)$ has the only solution $(\mathbf{x}, y=f(\mathbf{x}))$.

And I can explicitly produce the system $S(\mathbf{x},y)$ (in vector-matrix form) for any function $f(\mathbf{x})$ defined either by a formula or in tabular form.

The main drawback of the approach is that I need to calculate values of boolean function for all (!) 0-1 arguments ($2^n$ for n-variant function). Of course, there are another computing limitations for a large number of variables, but we can always express $f(\mathbf{x})$ as a composition of functions of a fewer number of variables.

Can you give me any references on this subject? Can you recommend something else, beyond the "realm of SAT"?

Wenxia Guo, etc. An Efficient Method to Transform a SAT problem to a Mixed Integer Linear Programming Problem, 2018

Ruirning Li, etc. Satisfiability and integer programming as complementary tools, 2004

Answer 1

If I understand correctly, you can obtain the desired linear constraints via conjunctive normal form. Explicitly, suppose $f(\bar{x}_1,\dots,\bar{x}_n)=1$, and let $S_0 = \{j\in\{1,\dots,n\}:\bar{x}_j = 0\}$ and $S_1 = \{j\in\{1,\dots,n\}:\bar{x}_j = 1\}$. You want to enforce $$\left[\left(\bigwedge_{j\in S_0} \lnot x_j\right) \bigwedge \left(\bigwedge_{j\in S_1} x_j\right)\right] \implies y.$$ Equivalently, $$\lnot\left[\left(\bigwedge_{j\in S_0} \lnot x_j\right) \bigwedge \left(\bigwedge_{j\in S_1} x_j\right)\right] \lor y \\ \left[\lnot\left(\bigwedge_{j\in S_0} \lnot x_j\right) \bigvee \lnot\left(\bigwedge_{j\in S_1} x_j\right)\right] \lor y \\ \left[\left(\bigvee_{j\in S_0} x_j\right) \bigvee \left(\bigvee_{j\in S_1} \lnot x_j\right)\right] \lor y \\ \sum_{j\in S_0} x_j + \sum_{j\in S_1} (1-x_j) + y \ge 1 \\ $$

Similarly, if $f(\bar{x}_1,\dots,\bar{x}_n)=0$, you want to enforce $$\left[\left(\bigwedge_{j\in S_0} \lnot x_j\right) \bigwedge \left(\bigwedge_{j\in S_1} x_j\right)\right] \implies \lnot y,$$ yielding linear constraint $$\sum_{j\in S_0} x_j + \sum_{j\in S_1} (1-x_j) - y \ge 0$$

This approach yields $2^n$ constraints.