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  (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
Full-Disclosure - We believe in it.
Hosted and sponsored by Secunia - http://secunia.com/
- help fuzzing/finding Horn CNF formula Georgi Guninski (Feb 19)