CNFs with Elementary Symmetric Clauses and their SAT Solving In this talk, we introduce elementary symmetric clauses into CNFs, explain handling the clauses in DPLL algorithm, and show experimental results.