# 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 > 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?

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.$$