Between proof construction and SAT-solving
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要