It is well-known that tree-like resolution refutations correspond to decision trees solving the associated false clause search problem. We describe this connection and some lower bounds using this. Then we discuss variants of tree-like resolution (resolution with parities and AND-resolution) along with the corresponding decision tree models, and lifting in this setting.
