SGER: Path Dissolution in Propositional Logic

确定命题逻辑中的公式是否可满足的问题在计算机科学中有着悠久的历史。它在复杂性理论中很重要，并且在机器人、光学字符识别、数据库系统、计算机体系结构、电路设计和验证等领域有着无数的应用，仅举几例。大部分机械定理证明社区的传统观点是，自动演绎的有趣应用需要一阶逻辑而不是命题逻辑。随着命题逻辑最近的成功，这种观点已经开始改变。命题逻辑当然是棘手的（除非NP = P）。用知识表示和数据库系统解决这个问题的一种方法是知识编译预处理潜在的命题理论。这个想法是在离线阶段做尽可能多的计算。然后在线阶段的查询可以快速处理。Horn子句、有序二元决策图、素蕴涵/蕴涵集和可分解否定范式（DNNF）都被提出作为这种编译的目标。路径分解是一种推理机制，自然地与NNF中的公式一起工作。它是强完全的，因为任何链接激活序列最终都会终止，产生一个称为完全溶解剂的无链接公式。剩下的路径是原始公式的模型。全分解式已被有效地用于计算公式的素蕴涵式和蕴涵式.可分解否定范式于1998年首次提出，目前正在研究其在知识表示和数据库系统中的应用。DNNF中的公式是一个完全溶剂，DNNF的许多优点似乎都存在于完全溶剂中，而且似乎公式的完全溶剂比公式的DNNF表示更有效。本研究的主要目的是探讨DNNF与全溶剂的关系。

ABSTRACT0229339Erik Rosenthal U of New HavenThe problem SAT determining whether a formula in propositional logic is satisfiable hasa long history in computer science. It is important in complexity theory and has myriad applicationsin fields such as robotics, optical character recognition, database systems, computerarchitecture, circuit design, and verification, to name but a few.The traditional view of much of the mechanical theorem proving community has been thatinteresting applications of automated deduction require first-order rather than propositionallogic. That view has begun to change in light of recent successes with propositional logic.Propositional logic is of course intractiable (unless NP = P). One approach to this problemwith knowledge representaion and database systems is knowledge compilation preprocessingthe underlying propositional theory. The idea is to do as much computation as possible in anoffline phase. Then queries in the online phase can be handled quickly. Horn clauses, orderedbinary decision diagrams, sets of prime implicates/implicants, and decomposable negationnormal form (DNNF) have all been proposed as targets of such compilation.Path dissolution is an inference mechanism that works naturally with formulas in NNF. Itis strongly complete in the sense that any sequence of link activations will eventually terminate,producing a linkless formula called the full dissolvent. The paths that remain are models of theoriginal formula. Full dissolvents have been used effectively for computing the prime implicantsand implicates of a formula.Decomposable negation normal form was first introduced in 1998 and is currently beingstudied for application to knowledge representation and database systems. A formula in DNNFis a full dissolvent, and it appears that many of the advantages of DNNF exist with full dissolvents.It also appears that a full dissolvent of a formula can be obtained more effciently thana DNNF representation of the formula. The main thrust of this project will be to examine therelationship of DNNF and full dissolvents.