[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <64fcd9051002190210m68a389efm6b0d151d547bb2ab@mail.gmail.com>
Date: Fri, 19 Feb 2010 21:10:42 +1100
From: Jeff Williams <jeffwillis30@...il.com>
To: Georgi Guninski <guninski@...inski.com>
Cc: full-disclosure@...ts.grok.org.uk
Subject: Re: help fuzzing/finding Horn CNF formula
Ask Jeremy Brown, he's a pro.
http://jbrownsec.blogspot.com/
2010/2/19 Georgi Guninski <guninski@...inski.com>
>
> i know i am dumb.
>
> i am looking for a HORN CNF that is SAT if and only if |x != y| ($x \ne y$)
> for boolean x,y.
>
> using the Horn constraints in [1] (at most k '1's) + the sought
> inequality/negation, it might be possible to encode Exact Sat (XSAT) to fast
> Horn CNF (md5 preimage falls in this case)
>
> i am not sure if such CNF formula exists though current academics claim
> Horn Sat is "P-complete", i.e. powerful enough for the formula.
>
> note that the size of the CNF doesn't matter much (it cares about just 2
> variables, the other vars are temp).
>
> i failed fuzzing it :)
>
> [1] Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
> C Sinz
> http://www-sr.informatik.uni-tuebingen.de/~sinz/CardConstraints/cp2005.pdf
>
> _______________________________________________
> Full-Disclosure - We believe in it.
> Charter: http://lists.grok.org.uk/full-disclosure-charter.html
> Hosted and sponsored by Secunia - http://secunia.com/
>
Content of type "text/html" skipped
_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/
Powered by blists - more mailing lists