Home page logo
/

fulldisclosure logo Full Disclosure mailing list archives

Re: help fuzzing/finding Horn CNF formula
From: Jeff Williams <jeffwillis30 () gmail com>
Date: Fri, 19 Feb 2010 21:10:42 +1100

Ask Jeremy Brown, he's a pro.

http://jbrownsec.blogspot.com/



2010/2/19 Georgi Guninski <guninski () 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/

  By Date           By Thread  

Current thread:
[ Nmap | Sec Tools | Mailing Lists | Site News | About/Contact | Advertising | Privacy ]
AlienVault