lists.openwall.net  lists / announce owlusers owldev johnusers johndev passwdqcusers yescrypt popa3dusers / osssecurity kernelhardening musl sabotage tlsify passwords / cryptdev xvendor / Bugtraq FullDisclosure linuxkernel linuxnetdev linuxext4 linuxhardening linuxcveannounce PHC  
Open Source and information security mailing list archives
 

MessageID: <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: fulldisclosure@...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 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/
Powered by blists  more mailing lists