2020/02/28 by Roberto Sebastiani, Sebastiani, Roberto
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.2003.04225
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.