If you want to get information about the SAT NP Complete Boolean satisfiability problem, then here I am telling you about it as you want.


Boolean satisfiability problem
In computer science, the Boolean Satisfiability Problem (sometimes called Propositional Satisfiability Problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.


Using the laws of Boolean algebra, every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer.

For example, transforming the formula
(x1∧y1) ∨ (x2∧y2) ∨ ... ∨ (xn∧yn) into conjunctive normal form yields (x1∨x2∨…∨xn) ∧ (y1∨x2∨…∨xn) ∧ (x1∨y2∨…∨xn) ∧ (y1∨y2∨…∨xn) ∧ ... ∧ (x1∨x2∨…∨yn) ∧ (y1∨x2∨…∨yn) ∧ (x1∨y2∨…∨yn) ∧ (y1∨y2∨…∨yn); while the former is a disjunction of n conjunctions of 2 variables, the latter consists of 2n clauses of n variables.


Here I am providing you a file, which is containing followings;

Why is SAT important?
Theoretical importance:
First NP-complete problem (Cook, 1971)

Many practical applications:
Model Checking
Automatic Test Pattern Generation
Combinational Equivalence Checking
Planning in AI
Automated Theorem Proving
Software Verification



An Example
• Inputs to SAT solvers are usually
represented in CNF
(a + b + c) (a’ + b’ + c) (a + b’ + c’) (a’ + b + c’)

Attached Files

SAT NP Complete Boolean satisfiability problem.pdf (204.2 KB, 531 views)