Narrowing Extended Resolution

Extended Resolution (i.e., Resolution incorporating the extension rule) is a more powerful proof system than Resolution because it can find polynomially bounded refutations of some SAT instances where Resolution alone cannot (and at the same time, every proof with resolution is still a valid proof with extended resolution). However it is very difficult to put it into practice because the extension rule is an additionnal source of combinatorial explosion, which tends to lengthen the time to discover a refutation. We call a restriction of Resolution forbiding the production of resolvents of size greater than 3 Narrow Resolution. We show that Narrow Extended Resolution p-simulates (unrestricted) Extended Resolution. We thus obtain a proof system whose combinatorics is highly reduced but which is still as powerful as before. However, the algorithms based on Resolution cannot be easily modified to accommodate this restriction on the resolution rule. This is why we define Splitting Resolution, a variant of Narrow Extended Resolution suitable for integrating into any resolution-based solver.