Convert propositional logic formulas to mathematical constraints

Question

Brief introduction

In all boolean (or more generally mixed-integer) linear programs, constraints are represented as a matrix $A$, a support vector $b$ and is computed by $A^T x \leq b$, where $x$ is a boolean vector one wants to optimize in some way. Another way of formulating the problem is to say that one wants to select a set of items such that a bunch of logic formulas are satisfied while optimizing some function. In my setting, I have all the soon-to-be-constraints in a list of propositional logic formulas. So, to be able to compute and solve using some kind of ILP-solver, I need to convert all logic formulas into mathematical constraints.

Straight-forward conversion from logic formula constraints

The most straight-forward way to convert from a propositional logic formula into mathematical constraints is to first convert the formula into Conjunctive normal form (CNF for short) and then from the CNF create one constraint for each and-clause. For example, let $q$ be formulated as the logical formula $$q = (a \lor b) \rightarrow c$$, then $q$ is converted to CNF $$q_{cnf} = (c \lor \neg a) \wedge (c \lor \neg b)$$ Now, for each conjunction clause we will have one constraint and for each variable in each disjunction we'll set $(1-x)$ if a variable $x$ is negated and just $x$ otherwise:

$$ (1-a)+c > 0 \wedge (1-b)+c > 0 \Rightarrow \\ c-a > -1 \wedge c-b > -1 \Rightarrow \\ c-a \geq 0 \wedge c-b \geq 0 \Rightarrow \\ a-c \leq 0 \wedge b-c \leq 0 $$

which we'll represent by a matrix $A$ and a vector $b$

$$ A= \begin{bmatrix} 1 & 0 & -1 \\ 0 & 1 & -1 \end{bmatrix} $$ $$ b= \begin{bmatrix} 0 & 0 \end{bmatrix} $$ where each column index in $A$ represents each variable of $a, b, c$, and we can now easily compute and solve for some optimization problem using all kinds of solvers.

Question

In the general case, a propositional logic formula is converted into many mathematical constraints. For some cases, the formula could be converted into just one constraint. For example, $a \wedge (b \lor c)$ can be represented in one line as $-2a - b - c \leq -3$ whereas $(a \wedge b) \lor c$ cannot be represented by one constraint.

Is there a method for determine if a formula can be represented as one constraint or not? And in the best case, is there even a method for converting into that one constraint if it exists or many otherwise?

Answer 1

Functions which can be described using a single constraint are known as halfspaces or linear threshold functions. They are also the functions computable using a single threshold gate.

Checking whether a function of this form exists is a linear programming problem: you look for a set of weights $w_1,\ldots,w_n,C$ such that if $f(x_1,\ldots,x_n) = 1$ then $$ \sum_i w_i x_i \geq C + 1, $$ and if $f(x_1,\ldots,x_n) = -1$ then $$ \sum_i w_i x_i \leq C - 1. $$

More efficient algorithms exist. For example, Maass and Turán gave a famous such algorithm in their paper "How fast can a threshold gate learn?".