Full Disclosure
mailing list archives
Re: help fuzzing/finding Horn CNF formula
From: Pavel Kankovsky <peak () argo troja mff cuni cz>
Date: Sun, 21 Feb 2010 16:38:29 +0100 (CET)
On Fri, 19 Feb 2010, Georgi Guninski wrote:
i am looking for a HORN CNF that is SAT if and only if x != y ($x \ne
y$) for boolean x,y.
Lemma: Let F(x_1, x_2, ...) be a Horn formula and A a B vectors assigning
truth values to its propositional variables x_1, .... If F is satisfied by
both A and B then F is satisfied by A&B where (A&B)_i = A_i & B_i
= min(A_i, B_i).
Proof: Let C be any clause of F. It can be a fact, a rule or a constraint:
1. If C == x_i is a fact: both A_i and B_i must be 1, (A&B)_i = 1,
therefore C is satisfied by A&B.
2. If C == ~x_i \/ ~x_j \/ ... \/ x_k is a rule: If (A&B)_k = 1 then C
is satisfied by A&B. If (A&B)_k = 0 then A_k = 0 or B_k = 0. Let's
assume A_k = 0 without loss of generality: C is satisfied by A
therefore at least one of A_i, A_j, ... must be 0 too. This
implies at least one of (A&B)_i, (A&B)_j, ... is 0 as well
and C is satisfied by A&B.
3. If C = ~x_i \/ ~x_j \/ ... is a constraint: C is satisfied by A
therefore at least one of A_i, A_j, ... must be 0. This implies
at least one of (A&B)_i, (A&B)_j, ... is 0 as well
and C is satisfied by A&B.
QED.
Consequence of lemma: Let F be a Horn formula satisfied by vectors
(0, 1, A) and (1, 0, B). Then F is satisfied by (0, 0, A&B).
In other words, there is no Horn formula F(x, y, ...) satisfiable if and
only if x and y are assigned different truth values.
This result does not contradict Pcompleteness of HORNSAT because the
transformation of the original problem is allowed to make changes to its
inputsuch as to negate one of variables and turn a question of
nonequivalence into a question of equivalence (expressible with a Horn
formula).

Pavel Kankovsky aka Peak / Jeremiah 9:21 \
"For death is come up into our MS Windows(tm)..." \ 21st century edition /
_______________________________________________
FullDisclosure  We believe in it.
Charter: http://lists.grok.org.uk/fulldisclosurecharter.html
Hosted and sponsored by Secunia  http://secunia.com/
By Date
By Thread
Current thread:
