[Full-disclosure] help fuzzing/finding Horn CNF formula
jeffwillis30 at gmail.com
Fri Feb 19 10:10:42 GMT 2010
Ask Jeremy Brown, he's a pro.
2010/2/19 Georgi Guninski <guninski at 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  (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 :)
>  Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
> C Sinz
> Full-Disclosure - We believe in it.
> Charter: http://lists.grok.org.uk/full-disclosure-charter.html
> Hosted and sponsored by Secunia - http://secunia.com/
-------------- next part --------------
An HTML attachment was scrubbed...
Full-Disclosure is hosted and sponsored by Secunia.