Full Disclosure
mailing list archives
help fuzzing/finding Horn CNF formula
From: Georgi Guninski <guninski () guninski com>
Date: Fri, 19 Feb 2010 10:56:20 +0200
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 "Pcomplete", 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://wwwsr.informatik.unituebingen.de/~sinz/CardConstraints/cp2005.pdf
_______________________________________________
FullDisclosure  We believe in it.
Charter: http://lists.grok.org.uk/fulldisclosurecharter.html
Hosted and sponsored by Secunia  http://secunia.com/
By Date
By Thread
Current thread:
 help fuzzing/finding Horn CNF formula Georgi Guninski (Feb 19)
