Recognition of tractable satisfiability problems through balanced polynomial representations

We consider a specific class of satisfiability (SAT) problems, the conjunctions of (nested) equivalencies (CoE). It is well known that CNF (conjunctive normal form) translations of CoE formulas are hard for branching and resolution algorithms. Tseitin proved that regular resolution requires a running time exponential in the size of the input. We review a polynomial time algorithm for solving CoE formulas, and address the problem of recognizing a CoE formula by its CNF representation. Making use of elliptic approximations of 3SAT problems, the so-called doubly balanced 3SAT formulas can be seen to be equivalent to CoE formulas. Subsequently, the notion of doubly balancedness is generalized by using polynomial representations of satisfiability problems, to obtain a general characterization of CoE formulas. We briefly address the problem of finding CoE subformulas, and finally the application of the developed theory to several DIMACS benchmarks is discussed.