Are You Satisfied by This Partial Assignment?
This work addresses foundational issues in SAT solving that could lead to more effective algorithms for researchers and practitioners in computational logic.
The paper analyzes the ambiguities and subtleties of partial-assignment satisfiability for SAT and SAT-related problems, particularly for non-CNF and existentially-quantified formulas, to potentially improve the efficiency of complete enumeration algorithms.
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.