A novel framework for systematic propositional formula simplification based on existential graphs

本文提出了一种新的命题逻辑简化演算法，该演算法源于皮尔斯的存在图规则和蕴含图。我们的规则适用于嵌套形式的命题逻辑公式，能够保持等价性，保证变量、子句和文字数量单调递减，并最大化结构问题信息的保留。我们的技术也可以看作是更高层次的SAT预处理，我们展示了其中一个规则（TWSR）如何概括和简化大部分已知的保持等价性的SAT预处理方法。此外，我们提出了一种基于我们的两个规则（EPR和TWSR）系统应用的简化程序，该程序与求解器无关，可用于简化大型布尔可满足性问题和任意形式的命题公式，并提供了其算法复杂性的正式分析，包括时间和空间。最后，我们展示了如何通过新的n元蕴含图进一步扩展我们的规则，以捕获所有已知的保持等价性的预处理程序。

该论文旨在提出一个新的命题逻辑简化计算方法，解决命题逻辑中变量、子句和文字数量过多的问题。同时，该方法也可以作为更高层次的SAT预处理，以简化大型布尔可满足性问题和命题公式。

该论文的关键思路是基于Peirce的存在图规则和蕴含图，提出了一组应用于嵌套形式命题逻辑公式的规则，这些规则保证了等价性、单调递减的变量、子句和文字数量，并最大化保留结构问题信息。

论文提出的简化计算方法是求解大型布尔可满足性问题和命题公式的一种新思路，同时提供了算法复杂度的正式分析。此外，论文还展示了如何将规则进一步扩展到n元蕴含图，以捕捉所有已知的等价性保持预处理程序。

与该论文相关的研究包括基于SAT预处理的其他等价性保持方法，如Huang等人的计算等价性（Computing Equivalences）和Sinz的自动预处理（Automatic Preprocessing）等。