Ask Jeremy Brown, he's a pro. http://jbrownsec.blogspot.com/
2010/2/19 Georgi Guninski <gunin...@guninski.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/ >
_______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.grok.org.uk/full-disclosure-charter.html Hosted and sponsored by Secunia - http://secunia.com/
