full-disclosure - Re: help fuzzing/finding Horn CNF formula

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <20100221154908.100A.1@paddy.troja.mff.cuni.cz>
Date: Sun, 21 Feb 2010 16:38:29 +0100 (CET)
From: Pavel Kankovsky <peak@...o.troja.mff.cuni.cz>
To: Georgi Guninski <guninski@...inski.com>
Cc: full-disclosure@...ts.grok.org.uk
Subject: Re: help fuzzing/finding Horn CNF formula

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/