SAT solvers use CNF (conjuction of disjunctions). DNF-SAT can be trivially solved in O(n), because each clause directly encodes a solution (except for clauses

SAT solvers use CNF (conjuction of disjunctions). DNF-SAT can be trivially solved in O(n), because each clause directly encodes a solution (except for clauses that are contradictory, of course). But there's no known way to "convert" arbitrary formulas to DNF in polynomial time, so such a solver is not useful.