An important subset of the Satisfiability problem is the pro

An important subset of the Satisfiability problem is the problem of determining whether a collection of Horn Clauses can be satisfied. This subset of the SAT problem can be solved in linear time. In particular, a Horn Clause is a disjunction (OR) of literals where at most one of the literals is not negated. For example, the following clause is a Horn clause.

(x1 OR NOT x2 OR NOT X3)

For your assignment, you will be given an input file that consists of a boolean formula that is a conjunction of Horn clauses. Your program will determine whether or not the formula is satisfiable. If the formula is satisfiable, your program will produce a satisfying assignment.

For example, on input

(A OR NOT B) AND (B OR NOT C) your program should output “Satisfiable A=TRUE; B=FALSE; C=FALSE”. Likewise, on input

(NOT A) AND (A)

your program should output “NOT Satisfiable”.

Solution

3 down vote accepted

A horn clause is a disjunction with at most one positive literal, e.g.

¬X1¬X2…¬XnY

The implication XY

can be written as disjunction ¬XY (proof by truth table). If X=¬X1¬X2…¬Xn, then ¬X is equivalent to X1X2…Xn

(De Morgan\'s law). Therefore, the above clause is logically equivalent to

(X1X2…Xn)Y

A Prolog program basically is a (large) list of horn clauses. A Prolog clause (called rule) is of the form head :- tail., which in logic notation is headtail

. Therfore, any horn clause

¬X1¬X2…¬XnY

is written in Prolog notation as Y :- X1, X2, X3, ..., Xn.

A horn clause containing no positive literal , e.g. ¬X1¬X2…¬Xn

can be rewritten as (X1X2…Xn)

, which is :- X1, X2, X3, ..., Xn. in Prolog notation.

Regarding your examples:

X Y Loves(X,Y)

That nested extential quantifier can be eleminated by Skolemization, which is introducing a new function for the extential quantifier inside the universal quantifier: X Loves(X,p(x))

, which in Prolog notation is loves(X,p(X)).

Explanation:

A Horn clause with exactly one positive literal is a definite clause; a definite clause with no negative literals is sometimes called a fact; and a Horn clause without a positive literal is sometimes called a goal clause (note that the empty clause consisting of no literals is a goal clause). These three kinds of Horn clauses are illustrated in the following propositional example:

In the non-propositional case, all variables in a clause are implicitly universally quantified with scope the entire clause. Thus, for example:

¬ human(X) mortal(X)

stands for:

X( ¬ human(X) mortal(X) )

which is logically equivalent to:

X ( human(X) mortal(X) )

Horn clauses play a basic role in constructive logic and computational logic. They are important in automated theorem proving by first-order resolution, because the resolvent of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiencies in proving a theorem (represented as the negation of a goal clause).