Linear Programming Formulation of Boolean Satisfiability Problem
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
- PDF / 214,802 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 15 Downloads / 240 Views
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. Keywords Boolean satisfiability · Conjunctive normal form · Convex function Linear programming · Multi-valued logic · NP problem · Time complexity.
·
1 Introduction The Boolean satisfiability (SAT) problem [4] is 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. For a formula with n variables and m clauses the conjunctive normal form (CNF) (X 1 ∨ X 2 ) ∧ (X 3 ∨ X 4 ) ∧ · · · ∧ (X n−1 ∨ X n )
(1)
A. A. Maknickas (B) Vilnius Gediminas Technical University, Sauletekio al. 11, Vilnius, Lithuania e-mail: [email protected] G.-C. Yang et al. (eds.), Transactions on Engineering Technologies, Lecture Notes in Electrical Engineering 275, DOI: 10.1007/978-94-007-7684-5_22, © Springer Science+Business Media Dordrecht 2014
305
306
A. A. Maknickas
is most the frequently used for representing Boolean formulas, where ¬∀X i are independent and in most cases m ≥ n. In CNF, the variables of the formula appear in literals (e.g., x) or their negation [e.g., ¬x (logical NOT ¬)]. Literals are grouped into clauses, which represent a disjunction (logical OR ∨) of the literals they contain. A single literal can appear in any number of clauses. The conjunction (logical AND ∧) of all clauses represents a formula. Several algorithms are known for solving the 2-satisfiability problem; the most efficient of them take linear time [2, 7, 8]. Instances of the 2-satisfiability or 2SAT problem are typically expressed as 2-CNF or Krom formulas [8] SAT was the first known NP-complete problem, as proved by Cook and Levin in 1971 [4, 9]. Until that time, the concept of an NP-complete problem did not even exist. The problem remains NP-complete even if all expressions are written in conjunctive normal form with 3 variables per clause (3-CNF), yielding the 3SAT problem. This means the expression has the form: (X 1 ∨ X 2 ∨ X 3 ) ∧ (X 4 ∨ X 5 ∨ X 6 ) ∧ · · · ∧ (X n−2 ∨ X n−1 ∨ X n )
(2)
NP-complete and it is used as a starting point for proving that other problems are also NP-hard. This is done by polynomial
Data Loading...
