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
[<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/
```