Are You Satisfied by This Partial Assignment?
share
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.
READ FULL TEXT