# Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration

arXiv: https://arxiv.org/abs/2503.01536 · HTML: https://mlsanity.com/paper/2503.01536/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 46 references that are in the map.
- First posted on arXiv 3 Mar 2025.

## Builds on (most cited first, 9 of 9)

- [Approximate Counting in SMT and Value Estimation for Probabilistic Programs](https://mlsanity.com/paper/1411.0659/) (2014)
- [Projected Model Counting](https://mlsanity.com/paper/1507.07648/) (2015)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [Optimization Modulo Theories with Linear Rational Costs](https://mlsanity.com/paper/1410.6039/) (2014)
- [Disjoint Partial Enumeration without Blocking Clauses](https://mlsanity.com/paper/2306.00461/) (2023)
- [Are You Satisfied by This Partial Assignment?](https://mlsanity.com/paper/2003.04225/) (2020)
- [Canonical Decision Diagrams Modulo Theories](https://mlsanity.com/paper/2404.16455/) (2024)
- [On Enumerating Short Projected Models](https://mlsanity.com/paper/2110.12924/) (2021)
- [Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses](https://mlsanity.com/paper/2410.18707/) (2024)

## Abstract (arXiv)

Many procedures for SAT-related problems, in particular for those requiring the complete enumeration of satisfying truth assignments, rely their efficiency and effectiveness on the detection of (possibly small) partial assignments satisfying an input formula. Surprisingly, there seems to be no unique universally-agreed definition of formula satisfaction by a partial assignment in the literature. In this paper we analyze in deep the issue of satisfaction by partial assignments, raising a flag about some ambiguities and subtleties of this concept, and investigating their practical consequences. We identify two alternative notions that are implicitly used in the literature, namely verification and entailment, which coincide if applied to CNF formulas but differ and present complementary properties if applied to non-CNF or to existentially-quantified formulas. We show that, although the former is easier to check and as such is implicitly used by most current search procedures, the latter has better theoretical properties, and can improve the efficiency and effectiveness of enumeration procedures.