## brief introduction

In all boolean linear programs (or more generally mixed integers), the constraints are represented as an array $ A $, a support vector $ b $ and is calculated by $ A ^ T x leq b $, where $ x $ it is a boolean vector that one wants to optimize in some way. Another way to formulate the problem is to say that one wants to select a set of elements so that a lot of logical formulas are satisfied while optimizing some function. In my environment, I have all the constraints that will soon become a list of propositional logical formulas. So in order to calculate and solve using some kind of ILP solver, I need to convert all logical formulas into mathematical constraints.

## Direct conversion from logical formula constraints

The most direct way to convert a propositional logical formula into mathematical constraints is to first convert the formula to normal conjunctive form (CNF for short) and then from the CNF create a constraint for each clause y. For example, let's $ q $ be formulated as the logical formula $$ q = (a lor b) rightarrow c $$, so $ q $ converts to CNF $$ q_ {cnf} = (c lor neg a) wedge (c lor neg b) $$ Now, for each conjunction clause we will have a restriction and for each variable in each disjunction we will establish $ (1-x) $ if a variable $ x $ is denied and fair $ 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

$$

that we will represent in a matrix $ A $ and a vector $ b $

$$

A =

begin {bmatrix}

1 and 0 and -1 \

0 and 1 and -1

end {bmatrix}

$$

$$

b =

begin {bmatrix}

0 and 0

end {bmatrix}

$$

where each column index in $ A $ represents each variable of $ a, b, c $, and now we can easily calculate and solve some optimization problems using all kinds of solvers.

## Question

In the general case, a propositional logical formula becomes many mathematical constraints. For some cases, the formula could become a single constraint. For example, $ a wedge (b lor c) $ can be represented on a line as $ -2a – b – c leq -3 $ While $ (a wedge b) lor c $ cannot be represented by a restriction.

**Is there a method to determine if a formula can be represented as a constraint or not? And at best, is there even a method of converting that one constraint if it exists or if there aren't many?**