Answer to your primary question: You have posed a Yes/No question. By definition, a Yes/No answer suffices. There is no requirement to produce any kind of assignment as an answer. If you modify the problem to require a certificate for the Yes/No answer, the answer will depend on what constraints you impose on the certificate and the certification algorithm (should it be linear-time verifiable, etc.).
Answer about terminology: The most common term I know of for what you call ``micromal'' is minimal assignment. I do not have a good sense for how standard this terminology is. If the partial assignments are represented as formulae, you obtain the very standard notion of prime implicants.
There is some confusion about terminology in your answer so I will expand on this issue below.
Assignments and Partial Assignments
A partial assignment is a partial function in $\mathit{Var} \to \{\mathsf{true}, \mathsf{false}\}$.
A partial assignment $\pi$ refines a partial assignment $\theta$ if for every variable $x$ on which $\theta$ is defined, $\pi$ is also defined and $\theta(x) = \pi(x)$. This definition allows $\pi$ to assign values for variables not assigned to by $\theta$.
A total assignment is a partial assignment that is a total function. A partial assignment represents the set of total assignments that refine it (meaning, that extend it). Observe that these definitions make no reference to formulae.
You can define the truth value of a formula under a partial assignment in a fairly standard manner. The only difference to defining the truth value of a formula under an assignment is that a formula may be $\mathsf{true}$, $\mathsf{false}$ or $\mathsf{unknown}$ under a partial assignment.
Minterms and Cubes
A literal in propositional logic is a Boolean variable or its negation. A cube is a conjunction of literals. A cube is a minterm is a cube in which every variable occurs exactly once.
There is a correspondence between minterms and partial assignments. Every partial assignment $\pi$ defined on exactly $k$ variables can be represented by a minterm $\ell_0 \land \cdots \land \ell_{k-1}$, such that $\ell_i = x_i$ if $\pi$ is defined on $x_i$ and sends $x_i$ to $\mathsf{true}$ and $\ell_i = \neg x_i$ if $\pi$ sends $x_i$ to $\mathsf{false}$. Observe that a total assignment $\sigma$ refines a partial assignment $\pi$ exactly if the assignment $\sigma$ satisfies the cube representation of $\pi$. We can similarly move in the other direction and represent cubes as partial assignments.
Prime Implicants and Minimal Assignments
Everything above was stated without needing the notion of a formula which is being solved. Let $F$ be a Boolean formula.
An implicant $C$ of a formula $F$ is a cube that implies $F$. The implicant $C$ is a prime implicant if there is no smaller cube that is an implicant.
The dual notion is of an implicate. An implicate $C$ of a formula $F$ is a clause $C$ that is implied by $F$. A prime implicate is an implicate that with no sub-clause that is an implicate.
The connection to your question is: If a partial assignment $\pi$ represents an implicant for a formula $F$, then every total assignment that refines $\pi$ satisfies $F$. Moreover, if no $\theta$ refined by $\pi$ represents an implicant, then $\pi$ represents a prime implicant. The literature on prime implicants is vast, but you only need to follow work that is based on modern SAT solvers because they will be using partial assignments.
Formalizing your question
I think it would help to use more precise terms in formalizing your question. Here are some examples.
Consider a partial assignment $\pi$ and a formula $F$.
- What is $\pi$ called if every total assignment $\theta$ that refines $\pi$ satisfies $F$? That is, $\pi$ represents a subset of the satisfiying assignments of $F$.
- What is $\pi$ called if every total assignment $\theta$ that satisfies $F$ also refines $\pi$? That is, $\pi$ represents a superset of the satisfying assignments of $F$.
Some comments. There is a unique, maximally defined partial assignment that contains a superset of all satisfying assignments to $F$. You can construct this by taking the conjunction of all literals implied by $F$.
There is no unique partial assignment that represents only satisfying assignments of $F$. There are multiple, maximal ones, corresponding to prime implicants.
References about implicants
These references are within a model checking context as I am more familiar with that context. There are discussions of minimizing assignments and manipulation of implication graphs in both these papers.
- Minimal Assignments for Bounded Model Checking, Ravi and Somenzi, 2004. (I did not find a freely available PDF, but maybe you can mail the authors if you don't have Springer access).
- Applying SAT Methods in Unbounded Symbolic Model Checking, McMillan, 2002.
About your algorithm
There are certain things you are doing in your algorithm which makes me wonder if you are familiar with modern SAT algorithms. You are describing a mix of the original Davis-Putnam and the Davis-Logeman-Loveland algorithm from the 60s. Specifically, Steps 4 and 5 are implemented differently today in what is called the unit rule.
Please confirm if this is what you mean by reliable assignment.
A partial assignment $\pi$ is reliable for a formula $F$ if some
extension of $\pi$ satisfies $F$.
I think that this definition is equivalent to yours but much much shorter. A better term would be feasible. Note that a partial assignment that is not reliable in the sense defined here is called a conflict.
I would suggest looking at the following CS Theory answers. (and all have answers shamelessly from me)
- Starting SAT solver papers
- CNF Rule Hierarchy Discovery
- Good reference about approximate methods for solving logic problems
