Between proof construction and SAT-solving

TL;DR

This paper explores using provability in implicational intuitionistic propositional logic as a natural framework for expressing and solving problems in Pspace, offering a new perspective beyond traditional SAT-solving methods.

Contribution

It introduces a novel approach linking IIPC provability to Pspace problems and demonstrates practical decision procedures with efficient performance in most cases.

Findings

Provability in IIPC can express Pspace problems effectively.

Reduction of full IPC provability to implicational formulas of order three.

Experimental results show fast decision procedures in most cases.

Abstract

The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (with all connectives) can be reduced to provability of implicational formulas of order three. Another advantage is a convenient interpretation in terms of simple alternating automata. Additionally, we distinguish some natural subclasses of IIPC corresponding to the complexity classes NP and co-NP. Our experimental results show that a simple decision procedure requires a significant amount of time only in a small fraction of cases.