A Polynomial Time Algorithm for HORN SAT

A Polynomial Time Algorithm for HORNSAT

Horn formula:A CNF Boolean formula in which every clause has at most one positive literal.

Each clause viewed as an implication.

A polynomial time algorithm to decide the satis?ability for Horn Formulas:

?Step1:Repeat Steps1.1and1.2below until either the formula is declared to be not satis?able in Step1.1or1.2or every clause has at least two literals:

Step1.1:In all clauses containing just one literal,assign truth values to the variables appearing in these clauses to make the clauses true.If this results in an inconsitent truth assigment then the

formula is not satis?able.Halt.

Step1.2:Simplify the formula using this new assignment.

–If any clause in the formula evaluates to false,then the formula is not satis?able.Halt.

–Eliminate all clauses which become true.

?Step2:Set all the remaining variables to false.

In Step2,every clause contains at least one negative literal.

?In Step2,every clause in the resulting formula has at least two literals;at most one of these two literals is a positive literal since Steps1.1and1.2do not increase the number of positive literals.

A Polynomial Time Algorithm for HORNSAT:Example (ˉA∨ˉB∨ˉD)∧(ˉE)∧(ˉC∨A)∧(C)∧(B)∧(ˉG∨D)∧(G).

A CNF Boolean formula in which every variable occurs at most twice.

A ploynomial time algorithm for deciding satis?ability for such formulas:

?Repeat the following simpli?cations:

–If a variable x occurs exactly once,then assign TRUE/FALSE to the variable that makes the

corresponding literal true;Remove the clause in which the variable occurred.

–If both x and?x occur in the same clause,remove that clause.

–If a variable x occurs twice,but both times either as x or as?x,then choose a value for x that

makes both literals true,and remove the corresponding clauses.

–The only interesting case is when the x occurs both as x and?x.Let(x∨y1∨y2...∨y l)and

(?x∨z1∨z2∨...∨z l )be the respective clauses.We use resolution,eliminate the two clauses

and replace it with one clause(y1∨y2∨...∨y l∨z1∨z2...∨z l ).

Note that at each step we remove one variable fromφ.If we end with x∧?x for some variable x,we output that the formula is unsatis?able.Otherwise,we say that the formula is satis?able.

Reduction from3CNFSAT:replace each occurence of a variable by the required number of new variables; for each variable x in the original formula,create new clauses to constrain x and all the new variables of x to take the same truth value.

?Letφbe a3CNFSAT formula.

?For each variable x i,let l1,l2,...,l m i be its occurrences inφeither as a positive or a negative literal (Here m i denotes the number of occurrences of x i as a literal).

?Replace each occurrence of x i by new variables{z ik|1≤k≤m i}as follows:

–If l k=x,replace it with z ik.

–If l k=?x,replace it with?z ik.

?Add the constraint that z ik’s attain the same boolean value as x i:

–Add a new set of clauses(?z i1∨z i2)∧(?z i2∨z i3)∧...∧(?z im i∨z i1).

?Note that this sub-formula is true i?the z ik’s are either all true or all false.

?Call the new formulaφ .