Hard instance generation for SAT
<|reference_start|>Hard instance generation for SAT: We propose an algorithm of generating hard instances for the Satisfying Assignment Search Problem (in short, SAT). The algorithm transforms instances of the integer factorization problem into SAT instances efficiently by using the Chinese Remainder Theorem. For example, it is possible to construct SAT instances with about 5,600 variables that is as hard as factorizing 100 bit integers.<|reference_end|>
@article{horie1998hard,
    title={Hard instance generation for SAT},
    author={Satoshi Horie and Osamu Watanabe},
    journal={In the Proc. of ISAAC'97, Lecture Notes in CS, Vol.1350, 22-31,
  1997},
    year={1998},
    number={TR98-0007},
    archivePrefix={arXiv},
    eprint={cs/9809117},
    primaryClass={cs.CC}
}