Linear Programming Formulation of Boolean Satisfiability Problem

Abstract

It was investigated the Boolean satisfiability (SAT) problem defined as follows: given a Boolean formula, check whether an assignment of Boolean values to the propositional variables in the formula exists, such that the formula evaluates to true. If such an assignment exists, the formula is said to be satisfiable; otherwise, it is unsatisfiable. With using of analytical expressions of multi-valued logic 2SAT boolean satisfiability was formulated as linear programming optimization problem. The same linear programming formulation was extended to find 3SAT and kSAT boolean satisfiability for k greater than 3. So, using new analytic multi-valued logic expressions and linear programming formulation of boolean satisfiability proposition that kSAT is in P and could be solved in linear time was proved.

List of Symbols and Abbreviations

$\lnot$ :

Logical NOT

$\vee$ :

Logical OR

$\wedge$ :

Logical AND

$\in$ :

in

$\mathbb {Z}^+$ :

Set of positive integer numbers

$g_k^n\left( a\right)$ :

Integer function of argument $a$

$\forall$ :

for all

$\mathbb {R}$ :

Set of real numbers

$\lfloor a \rfloor$ :

Floor round of $a$

$\pmod n$ :

Modulus of $n$ function

$\rho$ :

Multi-valued logic function of one argument

$i_0,i_1,i_2,\ldots$ :

Corresponding integer indexes

$\mu$ :

Multi-valued logic function of two arguments

$i_{0,0}, i_{0,1}, i_{0,2},\ldots$ :

Corresponding integer indexes

$\prod$ :

Product

$\times$ :

Multiplication

$\sum$ :

Summation

$+$ :

Summation of two numbers

$\le$ :

Less equal

$<$ :

Less

$\ge$ :

Greater equal

$>$ :

Greater

$=$ :

Equal

$X_i$ :

Integer variables

$i$ :

Integer index

$v$ :

Amount of vertexes

$e$ :

Amount of edges

$O(m)$ :

Big $O$ notation

$\max$ :

Maximum function

$k$ :

Number of variables in clause

$n$ :

Total number of variables

$m$ :

Total number of clauses

$\exists$ :

Exist

LP:

Linear programming

CNF:

Conjunctive normal form

SAT:

Boolean satisfiability