Boolean satisfiability

Abstract

There are many alternative ways to define a Boolean expression, but for our discussion, we must fix one of them. We define a string to be a Boolean expression if it is generated by the following context-free grammar G, with start symbol S: Let BOOL be the language of all strings generated by G. S → !S (logical not) S → S ⇒ S (implies) S → S ≡ S (logical equal) S → S = S (logical not equal) S → S * S (logical and) S → S + S (logical or) S → (S) S → I (I generates all identifiers) I → AN (The first symbol of an identifier must be a letter) A → a|b|c|d|e|f |g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z N → AN |0N |1N |2N |3N |4N |5N |6N |7N |8N |9N |λ S → 0 S → 1 The strings generated by I are called identifiers. An assignment of a Boolean expression E is an assignment of each identifier in I to a logical value, either 0 (false) or 1 (true). We say that an assignment satisfies E the if evaluation of E yields 1, after repacing each identifier by its assigned value. Otherwise, E is not satisfiable, i.e., a contradiction. Evaluation uses the rules of precedence of C++. Definition 1 A language L is N P-complete if there is a P-time reduction of any given N P-time language to L. We define an instance of the Boolean satisfiability problem to be a Boolean expression, E ∈ BOOL, where E ∈ SAT if E is satisfiable. Theorem 1 Every N P-time language has a P-time reduction to SAT. Thus, by definition, SAT is N P-complete. You can find the proof of Theorem 1 on the internet. Conjunctive Normal Form We say that a Boolean expression E is in conjunction normal form, or CNF, if E is the conjunction of clauses, each of which consists of the disjunction of terms, each of which is a variable or the negation of a variable. We say that E ∈ CNF is in 3CNF if each of its clauses has three terms. That is, E = C 1 * C 2 * · · · * C k where C i = (t i1 + t i2 + t i3), and where each term t ij is a variable or the negation of a variable. 2CNF, 4CNF, etc. are defined similarly.