Generation of hard non-clausal random satisfiability problems
AAAI(2005)
摘要
We present the results from experiments with a new family of random formulas for the satisfiability problem. Our proposal is a generalisation of the random k-SAT model that introduces non-clausal formulas and exhibits interesting features such as experimentally observed sharp phase transition and the easy-hard-easy pattern. The experimental results provide some insights on how the use of different clausal translations can affect the performance of satisfiability solving algorithms. We also expect our model to provide diverse and challenging benchmarks for developers of SAT procedures for non-clausal formulas.
更多查看译文
关键词
satisfiability,phase transition
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络