<p>Regarding your second and third questions, you want to know if there is a name for a partial assignment that is guaranteed not to be a nogood, and which will generate only satisfying assignments when DPLL is applied to it.  I am not aware of a standard name for this concept, but cannot judge whether "reliable assignment" (as you suggest) is suitable.  However, this sounds like it is closely related to Oliver Kullmann's <em>autarky</em> notion.</p>

<ul>
<li>Hans Kleine Büning and Oliver Kullmann, <em>Minimal Unsatisfiability and Autarkies</em>. Chapter 11 of <em>Handbook of Satisfiability</em>, 2009. (<a href="http://www.cs.swan.ac.uk/~csoliver/Artikel/p01c11_mus.pdf" rel="nofollow">draft</a>)</li>
</ul>

<p>I am not aware of any implementations of related concepts, but you might want to ask a SAT solver expert like the people taking part in the SAT Competition (<a href="http://satcompetition.org/2013/proceedings.shtml" rel="nofollow">2013 edition</a>).</p>

CC BY-SA 3.0
2013-11-11T07:57:59.660Z
In fact is it related to autarky. However, they are derived from and applied to a static clause set. When I wrote the proof for the set of reliable assignments in 2-SAT, I found that the method of "partial distributive expansion" is necessary to establish them. That requires a more rigorous definition of the set of allowed partial assignments. I begin to see, what happened when I extended CNF to a conjunction of DNFs and abstracted variables into 2-literal clauses. It was also very helpful, since I now have a reference for clause variable matrices. Thanks.
wolfmanx
CC BY-SA 3.0
2013-11-10T18:37:35.413Z
2013-11-10T18:37:35.413Z
András Salamon
<p>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 <em>certificate</em> 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.).</p>

<p>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 <em>prime implicants</em>. </p>

<p>There is some confusion about terminology in your answer so I will expand on this issue below.</p>

<p><strong>Assignments and Partial Assignments</strong></p>

<blockquote>
  <p>A partial assignment is a partial function in $\mathit{Var} \to \{\mathsf{true}, \mathsf{false}\}$.</p>
</blockquote>

<p>A partial assignment $\pi$ <em>refines</em> 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$.</p>

<p>A <em>total assignment</em> 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.</p>

<p>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.</p>

<p><strong>Minterms and Cubes</strong></p>

<p>A <em>literal</em> in propositional logic is a Boolean variable or its negation. A <em>cube</em> is a conjunction of literals. A cube is a <em>minterm</em> is a cube in which every variable occurs exactly once.</p>

<p>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.</p>

<p><strong>Prime Implicants and Minimal Assignments</strong></p>

<p>Everything above was stated without needing the notion of a formula which is being solved. Let $F$ be a Boolean formula.</p>

<p>An <em>implicant</em> $C$ of a formula $F$ is a cube that implies $F$. The implicant $C$ is a <em>prime implicant</em> if there is no smaller cube that is an implicant.</p>

<p>The dual notion is of an <em>implicate</em>. An <em>implicate</em> $C$ of a formula $F$ is a clause $C$ that is implied by $F$. A <em>prime implicate</em> is an implicate that with no sub-clause that is an implicate.</p>

<p>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.</p>

<p><strong>Formalizing your question</strong></p>

<p>I think it would help to use more precise terms in formalizing your question. Here are some examples.</p>

<p>Consider a partial assignment $\pi$ and a formula $F$.</p>

<ol>
<li>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$.</li>
<li>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$.</li>
</ol>

<p>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$. </p>

<p>There is no unique partial assignment that represents only satisfying assignments of $F$. There are multiple, maximal ones, corresponding to prime implicants.</p>

<p><strong>References about implicants</strong></p>

<p>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.</p>

<ol>
<li><a href="http://link.springer.com/chapter/10.1007/978-3-540-24730-2_3" rel="nofollow noreferrer">Minimal Assignments for Bounded Model Checking</a>, 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).</li>
<li><a href="http://kenmcmil.com/pubs/CAV02.pdf" rel="nofollow noreferrer">Applying SAT Methods in Unbounded Symbolic Model Checking</a>, McMillan, 2002.</li>
</ol>

<p><strong>About your algorithm</strong></p>

<p>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 <em>unit rule</em>.</p>

<p>Please confirm if this is what you mean by  <em>reliable assignment</em>. </p>

<blockquote>
  <p>A partial assignment $\pi$ is <em>reliable</em> for a formula $F$ if some
  extension of $\pi$ satisfies $F$.</p>
</blockquote>

<p>I think that this definition is equivalent to yours but much much shorter. A better term would be <em>feasible</em>. Note that a partial assignment that is not reliable in the sense defined here is called a <em>conflict</em>. </p>

<p>I would suggest looking at the following CS Theory answers. (and all have answers shamelessly from me)</p>

<ol>
<li><a href="https://cstheory.stackexchange.com/a/7611/4155">Starting SAT solver papers</a> </li>
<li><a href="https://cstheory.stackexchange.com/questions/16133/cnf-rule-hierarchy-discovery/16134#16134">CNF Rule Hierarchy Discovery</a></li>
<li><a href="https://cstheory.stackexchange.com/questions/18716/good-reference-about-approximate-methods-for-solving-logic-problems/18717#18717">Good reference about approximate methods for solving logic problems</a></li>
</ol>

CC BY-SA 3.0
2013-11-04T08:01:21.457Z
Thank you very much for your answer. It is extremely helpful as it gives me all the necessary words to describe my observations in standard terms and further close the communication gap. "Prime implicant" is exactly what I call a "minimal solution" (I got this from Bronstein 30 years ago and could not find it any more in newer prints). I will rephrase my question accordingly. I would vote up your answer, but unfortunately, I am not yet allowed.
wolfmanx
CC BY-SA 3.0
2013-11-04T08:56:30.063Z
Glad it could help. Hope you find the leads you need.
Vijay D
CC BY-SA 3.0
2013-11-09T18:45:04.493Z
The definition you are giving is my definition of an **unreliable** partial assignment. So, no, your definition does not apply.
wolfmanx
CC BY-SA 3.0
2013-11-10T00:20:42.107Z
What is the definition of unreliable assignment?  The definition I give above is the opposite of a nogood. If some refinement of $r$ (as I have defined) satisfies $F$ then $R(r)$ will be non-empty, hence $r$ is reliable. Also, if you return 'reliable' assignments as I currently understand them, they may not be polynomial time verifiable.
Vijay D
CC BY-SA 3.0
2013-11-10T00:52:09.237Z
I looked into the paper "Efficient CNF Simplification based on Binary Implication Graphs". At a first glance I did not see anything new, but the perspective is rather interesting. I took the example from that paper and prepared a step by step view [http://sw-amt.ws/exp/prime-implicants/README-simplification.html] with my algorithm, to show I handle CNF simplification. You do not have to understand the matrix entirely, but the visual progression may help to understand, that I am doing things differently than regular SAT solvers.
wolfmanx
CC BY-SA 3.0
2013-11-10T13:26:29.733Z
I think I am getting the hang of it. Being lost in the intricacies of my algorithm I had completely forgotten that it is based on the rigorous application of the most simple logic. It seems perfectly easy to express partial distributive expansion in a formalized language: http://www.sw-amt.ws/satoku/doc/doc-partial-distributive-expansion/README.html
wolfmanx
CC BY-SA 3.0
2013-11-10T22:12:42.947Z
And here is the proof of reliability for 2-SAT
http://sw-amt.ws/exp/prime-implicants/README.html#proof-of-reliability-for-2-sat
wolfmanx
CC BY-SA 3.0
2013-11-11T19:25:44.183Z
@wolfmanx, I'm busy with other things and can't spend more time on this right now. But I'm glad you see that a formalization that does not go through an algorithm is possible. Good luck with your SAT adventures. The last 13 items here might interest you: http://www-cs-faculty.stanford.edu/~uno/programs.html
Vijay D
CC BY-SA 3.0
2013-11-11T21:55:27.147Z
Thanks a lot for your help. But I actually went through the algorithm formally :)
wolfmanx
CC BY-SA 3.0
2013-11-04T02:41:51.893Z
2013-11-09T12:28:18.617Z
2017-04-13T12:32:28.080Z
Vijay D
<p>Considering the definition</p>

<blockquote>
  <p>"2-SAT: Given a CNF formula whose clauses have exactly 2 literals,
  does there exist an assignment of $\mathsf{TRUE}$ or $\mathsf{FALSE}$ to the variables
  that will satisfy the formula?"</p>
</blockquote>

<p><strong>Question 1:</strong> Is it necessary to give an assignment, or is it sufficient to prove that an assignment exists? (This question has been answered by Vijay D.)</p>

<p><strong>Question 2:</strong> A reliable assignment is a partial assignment which is guaranteed to deliver only satisfying assignments under DPLL. I.e., DPLL can never resolve an empty clause and therefore never produces an unsatisfying assignment. A reliable assignment is different from an implicant as it does not necessarily satisfy all clauses. However, an implicant is a special case of a reliable assignment.</p>

<p>I would prefer using the correct term for this type of assignment.</p>

<p><strong>Question3:</strong> Reliable assignments appear in my SAT solving algorithm as an entire set with cost O(n^2). A set of implicants can be generated by distributive expansion of the disjunctions defining the reliable assignments with cost O(2^n). Due to the construction, each implicant is necessarily defined by the conjunction of a subset of reliable assignments.</p>

<p>Does such a set of reliable assignments appear in other algorithms?</p>

<hr>

<p><strong>Context</strong></p>

<p>The reliable assignments appear in the context of <a href="http://www.sw-amt.ws/satoku/doc/doc-partial-distributive-expansion/README.html" rel="nofollow">Partial Distributive Expansion</a></p>

<p>Detailed examples are available at <a href="http://sw-amt.ws/exp/prime-implicants/README.html" rel="nofollow">Prime Implicants and Reliable Assignments</a>.</p>

<p>The full context is an integrated SAT algorithm for a complete set of solutions. Here is an <a href="http://www.sw-amt.ws/satoku/doc/doc-rationale/README.html" rel="nofollow">informal rationale</a> on what I have to cover eventually. Any hints welcome.</p>

CC BY-SA 3.0
2013-11-02T19:42:27.327Z
I don't know if this class of partial solutions already has a name but, if it doesn't, I recommend that you choose a name that will help your readers understand their properties. For example, in graph theory, trees have a similar structure to biological trees, so it's easy to remember what they are. To me, "micromal" would mean "resembling a microme", whatever one of those is, and that gives no hint at all to the reader.
David Richerby
CC BY-SA 3.0
2013-11-02T22:40:23.570Z
@david-richerby Thanks for your answer :) I understand what you mean ("mikromal" sounds different in German).

I agree with you and I would name it just "minimal", because that is exactly what it is. It is the minimum amount of information necessary to reliably construct a satisfying assignment. But somebody else already used this absolute term to specify an assignment that satisfies all clauses (but not necessarily all variables).
wolfmanx
CC BY-SA 3.0
2013-11-02T23:47:53.627Z
I'm not sure whether I understand exactly what the question is asking.  It sounds like the question is: "Is this solution strategy acceptable?"  I don't know how to answer that, without a definition of what you mean by acceptable.  Perhaps one approach would be to think about applications of your approach.  Can you identify an application where this enables you to do something that couldn't have been done with prior algorithms, or that you can do much more efficiently than prior algorithms?
D.W.
CC BY-SA 3.0
2013-11-06T09:00:14.910Z
@vijay-d No, I have not misunderstood them.

The prime implicants for the CNF:
  ( ¬a ∨ ¬b ) ∧ ( ¬a ∨  d ) ∧ (  a ∨  b ) ∧ (  a ∨  c ) ∧ ( ¬b ∨  c ) ∧ (  b ∨  d ) ∧ (  c ∨  d )
are given by the DNF:
  ( ¬a ∧  b ∧  c ) ∨ (  a ∧ ¬b ∧  d )
Additional reliable assignments are:
  ( c ), ( d )
See [Prime Implicants and Reliable Assignments](http://sw-amt.ws/exp/prime-implicants/README.html)
wolfmanx
CC BY-SA 3.0
2013-11-06T09:11:06.280Z
@vijay-d What I mean is: prime implicants are sufficient to establish satisfiability, but they are not necessary. Reliable assignments are generally also sufficient, but not necessary. Minimal reliable assignments are both sufficient and necessary. In other words, if prime implicants are required, the algorithm has worst case O(2^n), if reliable assignments are "good enough", the algorithm has worst case O(n^2). That is a huge difference.
wolfmanx
CC BY-SA 3.0
2013-11-06T09:12:30.040Z
@vijay-d That you think that I have misunderstood prime implicants illustrates my problem: I can obviously not communicate effectively, if I keep inventing my own expressions or if I do not use the conventional terms correctly. Which makes it hard to find anybody willing to listen.
wolfmanx
CC BY-SA 3.0
2013-11-06T10:21:06.630Z
@wolfmanx, the hardest but most valuable skill in research is learning to speak a language someone outside your head understands without pulling all your hair out. If it helps, we've all been there. I understand what you want and when I next have time, I'll try to find out what people in the field call it.
Vijay D
CC BY-SA 3.0
2013-11-06T11:40:17.597Z
@vijay-d This is the perfect description of my frustration :) Very much appreciated!
wolfmanx
CC BY-SA 3.0
2013-11-07T03:41:04.997Z
@wolfmanx, it looks like you originally had at least three questions. I modified your title so you don't have to change it again. Please see the suggestions in my answer and use them to formulate a precise question. I also made a suggestion for formatting your question so that the questions are short and separate from the background description. I find it easier to read questions split up in this way.
Vijay D
CC BY-SA 3.0
2013-11-08T03:49:38.367Z
@vijay-d Thanks for your patience. If you are not a teacher, you should really become one. Being inept to ask questions efficiently made me wonder, whether I should even try to formalize my research. I did gain some wonderful insights and they keep coming, but informally looking at the [bare necessities](http://www.sw-amt.ws/satoku/doc/doc-rationale/README.html) makes me feel real small :)
wolfmanx
CC BY-SA 3.0
2013-11-08T08:31:15.327Z
@wolfmanx, thanks. You have not defined reliable assignments. In your example, c is necessary but not sufficient because (a∧b∧c∧d) extends c but does not satisfy the formula. Same for d.
Vijay D
CC BY-SA 3.0
2013-11-08T17:43:47.950Z
In my thesis I used the term "prop" for partial assignments that satisfy every clause.  I do not know a standard name for partial assignments that are not necessarily props, yet can be used as a basis for an algorithm extending (and presumably also pruning) them to become complete assignments.  A partial assignment that _cannot_ be extended to a complete assignment is called a _nogood_; this term was introduced by Stallman (yes, RMS) and Sussman in 1976.
András Salamon
CC BY-SA 3.0
2013-11-08T17:59:51.797Z
@vijay-d I'm pretty sure I have :). I remember doing this verification manually for a couple of months, always hoping that it would, please, succeed, before I realized that the partial assignments had this property because they never failed. I have then tried to invalidate them for a while, just for fun. I have started to formalize reliable assignments now and added an example [http://sw-amt.ws/exp/prime-implicants/README.html#why-a-b-c-d-is-not-a-valid-reliable-refinement-of-c](why (a, b, c, d) is not a valid reliable refinement of (c)).
wolfmanx
CC BY-SA 3.0
2013-11-08T18:25:50.010Z
@AndrásSalamon Are you sure, that we are talking about the same thing? My reliable assignments do not necessarily satisfy every clause. They are sort of lazy and leave some clauses unsatisfied. However, the unsatisfied clauses can easily be satisfied by the mentioned function. I like the term _nogood_, do you have a reference?
wolfmanx
CC BY-SA 3.0
2013-11-08T18:50:20.150Z
http://dx.doi.org/10.1016/0004-3702(77)90029-7 is the journal version of the 1976 techrep that introduced _nogood_ (which is a standard term in constraint programming, with the more specific definition that I mentioned); it is the first hit on Google Scholar for "stallman sussman".
András Salamon
CC BY-SA 3.0
2013-11-08T18:52:56.583Z
Also, please re-read what I wrote in my comment.
András Salamon
CC BY-SA 3.0
2013-11-08T21:35:32.300Z
@AndrásSalamon Thanks. You're right, you said so. My classification was reliable/unreliable/totally unreliable. reliable/unreliable/_nogood_ is better. Especially if it is standard already.
wolfmanx
CC BY-SA 3.0
2013-11-09T15:47:23.637Z
@VijayD: are you sure conflict is the right term?  I thought conflict meant a partial assignment that does not satisfy the original clauses together with the speculative assignments so far; conflict clauses represent nogoods but not all nogoods are of this form.  In particular, any partial assignment is a nogood in an unsatisfiable formula, whereas the conflicts depend on the algorithm.  A pointer to a specific paper would be welcome.
András Salamon
CC BY-SA 3.0
2013-11-09T16:07:44.100Z
@VijayD: For instance, the Sakallah/Marques-Silva survey from 2011 says "GRASP introduced a novel procedure for clause learning from conflicts, i.e., from partial assignments that cause the formula to evaluate to 0... A conﬂict is captured as a partial variable assignment, namely the assignment that causes the CNF formula to evaluate to 0.   Negating this assignment yields the desired missing constraint in the form of a conﬂict-induced clause."
András Salamon
CC BY-SA 3.0
2013-11-09T18:08:11.773Z
@AndrásSalamon, yes you are right. A conflict is a partial assignment that causes at least one clause to evaluate to false. A conflict clause blocks a conflict. I see that a nogood is a different notion.
Vijay D
<cc.complexity-theory><lo.logic><sat>
Questions about special types of partial assignments
wolfmanx
# Questions about special types of partial assignments

(Asked by: username_0 on 2013-11-02)

Considering the definition

> "2-SAT: Given a CNF formula whose clauses have exactly 2 literals,
> does there exist an assignment of $\mathsf{TRUE}$ or $\mathsf{FALSE}$ to the variables
> that will satisfy the formula?"

**Question 1:** Is it necessary to give an assignment, or is it sufficient to prove that an assignment exists? (This question has been answered by username_3.)

**Question 2:** A reliable assignment is a partial assignment which is guaranteed to deliver only satisfying assignments under DPLL. I.e., DPLL can never resolve an empty clause and therefore never produces an unsatisfying assignment. A reliable assignment is different from an implicant as it does not necessarily satisfy all clauses. However, an implicant is a special case of a reliable assignment.

I would prefer using the correct term for this type of assignment.

**Question3:** Reliable assignments appear in my SAT solving algorithm as an entire set with cost O(n^2). A set of implicants can be generated by distributive expansion of the disjunctions defining the reliable assignments with cost O(2^n). Due to the construction, each implicant is necessarily defined by the conjunction of a subset of reliable assignments.

Does such a set of reliable assignments appear in other algorithms?

---

**Context**

The reliable assignments appear in the context of [Partial Distributive Expansion](http://www.sw-amt.ws/satoku/doc/doc-partial-distributive-expansion/README.html)

Detailed examples are available at [Prime Implicants and Reliable Assignments](http://sw-amt.ws/exp/prime-implicants/README.html).

The full context is an integrated SAT algorithm for a complete set of solutions. Here is an [informal rationale](http://www.sw-amt.ws/satoku/doc/doc-rationale/README.html) on what I have to cover eventually. Any hints welcome.

**Tags:** cc.complexity-theory, lo.logic, sat

> **Comments:**
> **username_1**: I don't know if this class of partial solutions already has a name but, if it doesn't, I recommend that you choose a name that will help your readers understand their properties. For example, in graph theory, trees have a similar structure to biological trees, so it's easy to remember what they are. To me, "micromal" would mean "resembling a microme", whatever one of those is, and that gives no hint at all to the reader.  
> **username_0**: @david-richerby Thanks for your answer :) I understand what you mean ("mikromal" sounds different in German).  I agree with you and I would name it just "minimal", because that is exactly what it is. It is the minimum amount of information necessary to reliably construct a satisfying assignment. But somebody else already used this absolute term to specify an assignment that satisfies all clauses (but not necessarily all variables).  
> **username_2**: I'm not sure whether I understand exactly what the question is asking.  It sounds like the question is: "Is this solution strategy acceptable?"  I don't know how to answer that, without a definition of what you mean by acceptable.  Perhaps one approach would be to think about applications of your approach.  Can you identify an application where this enables you to do something that couldn't have been done with prior algorithms, or that you can do much more efficiently than prior algorithms?  
> **username_0**: @vijay-d No, I have not misunderstood them.  The prime implicants for the CNF:   ( ¬a ∨ ¬b ) ∧ ( ¬a ∨  d ) ∧ (  a ∨  b ) ∧ (  a ∨  c ) ∧ ( ¬b ∨  c ) ∧ (  b ∨  d ) ∧ (  c ∨  d ) are given by the DNF:   ( ¬a ∧  b ∧  c ) ∨ (  a ∧ ¬b ∧  d ) Additional reliable assignments are:   ( c ), ( d ) See [Prime Implicants and Reliable Assignments](http://sw-amt.ws/exp/prime-implicants/README.html)  
> **username_0**: @vijay-d What I mean is: prime implicants are sufficient to establish satisfiability, but they are not necessary. Reliable assignments are generally also sufficient, but not necessary. Minimal reliable assignments are both sufficient and necessary. In other words, if prime implicants are required, the algorithm has worst case O(2^n), if reliable assignments are "good enough", the algorithm has worst case O(n^2). That is a huge difference.  
> **username_0**: @vijay-d That you think that I have misunderstood prime implicants illustrates my problem: I can obviously not communicate effectively, if I keep inventing my own expressions or if I do not use the conventional terms correctly. Which makes it hard to find anybody willing to listen.  
> **username_3**: @username_0, the hardest but most valuable skill in research is learning to speak a language someone outside your head understands without pulling all your hair out. If it helps, we've all been there. I understand what you want and when I next have time, I'll try to find out what people in the field call it.  
> **username_0**: @vijay-d This is the perfect description of my frustration :) Very much appreciated!  
> **username_3**: @username_0, it looks like you originally had at least three questions. I modified your title so you don't have to change it again. Please see the suggestions in my answer and use them to formulate a precise question. I also made a suggestion for formatting your question so that the questions are short and separate from the background description. I find it easier to read questions split up in this way.  
> **username_0**: @vijay-d Thanks for your patience. If you are not a teacher, you should really become one. Being inept to ask questions efficiently made me wonder, whether I should even try to formalize my research. I did gain some wonderful insights and they keep coming, but informally looking at the [bare necessities](http://www.sw-amt.ws/satoku/doc/doc-rationale/README.html) makes me feel real small :)  
> **username_3**: @username_0, thanks. You have not defined reliable assignments. In your example, c is necessary but not sufficient because (a∧b∧c∧d) extends c but does not satisfy the formula. Same for d.  
> **username_4**: In my thesis I used the term "prop" for partial assignments that satisfy every clause.  I do not know a standard name for partial assignments that are not necessarily props, yet can be used as a basis for an algorithm extending (and presumably also pruning) them to become complete assignments.  A partial assignment that _cannot_ be extended to a complete assignment is called a _nogood_; this term was introduced by Stallman (yes, RMS) and Sussman in 1976.  
> **username_0**: @vijay-d I'm pretty sure I have :). I remember doing this verification manually for a couple of months, always hoping that it would, please, succeed, before I realized that the partial assignments had this property because they never failed. I have then tried to invalidate them for a while, just for fun. I have started to formalize reliable assignments now and added an example [http://sw-amt.ws/exp/prime-implicants/README.html#why-a-b-c-d-is-not-a-valid-reliable-refinement-of-c](why (a, b, c, d) is not a valid reliable refinement of (c)).  
> **username_0**: @AndrásSalamon Are you sure, that we are talking about the same thing? My reliable assignments do not necessarily satisfy every clause. They are sort of lazy and leave some clauses unsatisfied. However, the unsatisfied clauses can easily be satisfied by the mentioned function. I like the term _nogood_, do you have a reference?  
> **username_4**: http://dx.doi.org/10.1016/0004-3702(77)90029-7 is the journal version of the 1976 techrep that introduced _nogood_ (which is a standard term in constraint programming, with the more specific definition that I mentioned); it is the first hit on Google Scholar for "stallman sussman".  
> **username_4**: Also, please re-read what I wrote in my comment.  
> **username_0**: @AndrásSalamon Thanks. You're right, you said so. My classification was reliable/unreliable/totally unreliable. reliable/unreliable/_nogood_ is better. Especially if it is standard already.  
> **username_4**: @VijayD: are you sure conflict is the right term?  I thought conflict meant a partial assignment that does not satisfy the original clauses together with the speculative assignments so far; conflict clauses represent nogoods but not all nogoods are of this form.  In particular, any partial assignment is a nogood in an unsatisfiable formula, whereas the conflicts depend on the algorithm.  A pointer to a specific paper would be welcome.  
> **username_4**: @VijayD: For instance, the Sakallah/Marques-Silva survey from 2011 says "GRASP introduced a novel procedure for clause learning from conflicts, i.e., from partial assignments that cause the formula to evaluate to 0... A conﬂict is captured as a partial variable assignment, namely the assignment that causes the CNF formula to evaluate to 0.   Negating this assignment yields the desired missing constraint in the form of a conﬂict-induced clause."  
> **username_3**: @AndrásSalamon, yes you are right. A conflict is a partial assignment that causes at least one clause to evaluate to false. A conflict clause blocks a conflict. I see that a nogood is a different notion.  

---

## 2 answers

### Answer by username_3 on 2013-11-04. Score: 8 | Accepted answer

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$.

1. 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$.
2. 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.

1. [Minimal Assignments for Bounded Model Checking](http://link.springer.com/chapter/10.1007/978-3-540-24730-2_3), 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).
2. [Applying SAT Methods in Unbounded Symbolic Model Checking](http://kenmcmil.com/pubs/CAV02.pdf), 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)

1. [Starting SAT solver papers](https://cstheory.stackexchange.com/a/7611/4155)
2. [CNF Rule Hierarchy Discovery](https://cstheory.stackexchange.com/questions/16133/cnf-rule-hierarchy-discovery/16134#16134)
3. [Good reference about approximate methods for solving logic problems](https://cstheory.stackexchange.com/questions/18716/good-reference-about-approximate-methods-for-solving-logic-problems/18717#18717)

> **Comments:**
> **username_0**: Thank you very much for your answer. It is extremely helpful as it gives me all the necessary words to describe my observations in standard terms and further close the communication gap. "Prime implicant" is exactly what I call a "minimal solution" (I got this from Bronstein 30 years ago and could not find it any more in newer prints). I will rephrase my question accordingly. I would vote up your answer, but unfortunately, I am not yet allowed.  
> **username_3**: Glad it could help. Hope you find the leads you need.  
> **username_0**: The definition you are giving is my definition of an **unreliable** partial assignment. So, no, your definition does not apply.  
> **username_3**: What is the definition of unreliable assignment?  The definition I give above is the opposite of a nogood. If some refinement of $r$ (as I have defined) satisfies $F$ then $R(r)$ will be non-empty, hence $r$ is reliable. Also, if you return 'reliable' assignments as I currently understand them, they may not be polynomial time verifiable.  
> **username_0**: I looked into the paper "Efficient CNF Simplification based on Binary Implication Graphs". At a first glance I did not see anything new, but the perspective is rather interesting. I took the example from that paper and prepared a step by step view [http://sw-amt.ws/exp/prime-implicants/README-simplification.html] with my algorithm, to show I handle CNF simplification. You do not have to understand the matrix entirely, but the visual progression may help to understand, that I am doing things differently than regular SAT solvers.  
> **username_0**: I think I am getting the hang of it. Being lost in the intricacies of my algorithm I had completely forgotten that it is based on the rigorous application of the most simple logic. It seems perfectly easy to express partial distributive expansion in a formalized language: http://www.sw-amt.ws/satoku/doc/doc-partial-distributive-expansion/README.html  
> **username_0**: And here is the proof of reliability for 2-SAT http://sw-amt.ws/exp/prime-implicants/README.html#proof-of-reliability-for-2-sat  
> **username_3**: @username_0, I'm busy with other things and can't spend more time on this right now. But I'm glad you see that a formalization that does not go through an algorithm is possible. Good luck with your SAT adventures. The last 13 items here might interest you: http://www-cs-faculty.stanford.edu/~uno/programs.html  
> **username_0**: Thanks a lot for your help. But I actually went through the algorithm formally :)  

---

### Answer by username_4 on 2013-11-10. Score: 1

Regarding your second and third questions, you want to know if there is a name for a partial assignment that is guaranteed not to be a nogood, and which will generate only satisfying assignments when DPLL is applied to it. I am not aware of a standard name for this concept, but cannot judge whether "reliable assignment" (as you suggest) is suitable. However, this sounds like it is closely related to Oliver Kullmann's *autarky* notion.

* Hans Kleine Büning and Oliver Kullmann, *Minimal Unsatisfiability and Autarkies*. Chapter 11 of *Handbook of Satisfiability*, 2009. ([draft](http://www.cs.swan.ac.uk/~csoliver/Artikel/p01c11_mus.pdf))

I am not aware of any implementations of related concepts, but you might want to ask a SAT solver expert like the people taking part in the SAT Competition ([2013 edition](http://satcompetition.org/2013/proceedings.shtml)).

> **Comments:**
> **username_0**: In fact is it related to autarky. However, they are derived from and applied to a static clause set. When I wrote the proof for the set of reliable assignments in 2-SAT, I found that the method of "partial distributive expansion" is necessary to establish them. That requires a more rigorous definition of the set of allowed partial assignments. I begin to see, what happened when I extended CNF to a conjunction of DNFs and abstracted variables into 2-literal clauses. It was also very helpful, since I now have a reference for clause variable matrices. Thanks.  

---

