Abstract
Let k-CNF∆ be a formulation of k-CNF where distinct formulas have disjoint sets of variables, and k-SAT∆ the satisfiable formulas in k-CNF∆. A property of k-CNF∆ formulas is symmetric if it is preserved under complementation of variables. The main theorem says that no symmetric property of k-CNF∆ formulas can force an algorithm for k-SAT∆ to take superlinear time. This result is based on observations of Ryan Williams from 2010.