Convert propositional logic formulas to mathematical constraints 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 &gt; 0 \wedge (1-b)+c &gt; 0 \Rightarrow \\
  c-a &gt; -1 \wedge c-b &gt; -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 &amp; 0 &amp; -1 \\
    0 &amp; 1 &amp; -1
  \end{bmatrix}
$$
$$
b=
\begin{bmatrix}
    0 &amp; 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?
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?".