Forced Satisfiable Problems

From: Ke Xu (kexu_at_nlsde.buaa.edu.cn)
Date: 02/27/04 

Date: 26 Feb 2004 21:10:45 -0800

Dear All,

Recently, I proposed a new method to generate random hard satisfiable
SAT benchmarks, i.e. all benchmarks are forced to be satisfiable with
a planted solution. According to the experimental results of ours and
some other researchers, these benchmarks are (almost surely) very hard
to solve for state-of-the-art SAT solvers when the problem size is
only moderately large (e.g. 1000 variables and 60000 clauses). For
more information, please see the following paper

K. Xu and W. Li. Many Hard Examples in Exact Phase Transitions with
Application to Generating Hard Satisfiable Instances. Technical Report
cs.CC/0302001, Computing Research Repository (CoRR), 2003.
Available at http://www.nlsde.buaa.edu.cn/~kexu/papers/hard-csp-abstract.htm
OR http://arxiv.org/abs/cs/0302001

In some sense, forced satisfiable problems are similar to factoring
problems. So, I would like to know if such a method of generating hard
satisfiable formulas is of interest to people working in cryptography
or related areas, and if so, how it can be applied to these areas.

Thnx in advance...

Best regards,
Ke Xu
http://www.nlsde.buaa.edu.cn/~kexu/