Are You Satisfied by This Partial Assignment?

TL;DR

This paper examines the concept of partial-assignment satisfiability in complex formulas, highlighting ambiguities and their implications for improving enumeration algorithms in SAT-related problems.

Contribution

It provides a detailed analysis of partial-assignment satisfiability, especially for non-CNF and quantified formulas, addressing ambiguities and practical impacts.

Findings

Identifies ambiguities in partial-assignment satisfiability

Analyzes implications for non-CNF and quantified formulas

Suggests directions for developing better enumeration algorithms

Abstract

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.