Home page logo
/

fulldisclosure logo 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 P-completeness of HORN-SAT because the
transformation of the original problem is allowed to make changes to its
input--such 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 /

_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/


  By Date           By Thread  

Current thread:
[ Nmap | Sec Tools | Mailing Lists | Site News | About/Contact | Advertising | Privacy ]