你对这部分工作满意吗?
Are You Satisfied by This Partial Assignment?
摘要:
SAT和SAT相关问题的许多程序-特别是那些需要满足真值分配的完整枚举的程序-依赖于检测满足输入公式的部分分配的效率。在本文中,我们分析了部分分配可满足性的概念-特别是在处理非CNF和存在量化公式时-提出了关于这个概念的模糊性和微妙性的标志,并调查其实际后果。这可能会推动更有效的分配枚举算法的发展。
英文摘要:
Many procedures for SAT and SAT-related problems -- in particular for those requiring the complete enumeration of satisfying truth assignments -- rely their efficiency on the detection of partial assignments satisfying an input formula. In this paper we analyze the notion of partial-assignment satisfiability -- in particular when dealing with non-CNF and existentially-quantified formulas -- raising a flag about the ambiguities and subtleties of this concept, and investigating their practical consequences. This may drive the development of more effective assignment-enumeration algorithms.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。