On the decision trees with symmetries

Abstract

We introduce a propositional proof system based on decision trees utilizing symmetries of formulas. We refer to this proof system as decision trees with symmetries (SDT). SDT can be polynomially simulated by the proof system SR-I introduced by Krishnamurthy [7]; SR-I extends Resolution with the symmetry rule. We show that there are polynomial-size proofs of the functional pigeonhole principle ([Formula Present]) and of an encoding of the clique coloring principle (CLIQUE-COLORINGn,k). On the other hand we show that any SDT for the pigeonhole principle ([Formula Present]) has size [Formula Present] despite that [Formula Present] has a lot of symmetries. In 1999 Urquhart [11] showed that [Formula Present] has a polynomial-size SR-I refutation. Thus SDT is strictly weaker than SR-I. The smallest decision tree for [Formula Present] has size 2Ω(n log n); we show that there exists an SDT for [Formula Present] of size [Formula Present].