1
$\begingroup$

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

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Dear Robert, I did not use CNF or DNF representation of boolean function at all. I use general purpose polyhedra handling application. As a result I get irreducible (in some sense) linear system. But I can not give evaluation of the number of inequalities as you did. Another drawback of my approach is that I need to calculate values of boolean function for all (!) 0-1 arguments. But my question was not about EXISTENCE of linear system equvalent to the boolean function. It is well known fact. I'm looking for references to sci. books, papers etc. on the subject! $\endgroup$ May 7 at 20:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.