2
$\begingroup$

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 Vijay D.)

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

Detailed examples are available at Prime Implicants and Reliable Assignments.

The full context is an integrated SAT algorithm for a complete set of solutions. Here is an informal rationale on what I have to cover eventually. Any hints welcome.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – David Richerby Nov 2 '13 at 19:42
  • $\begingroup$ @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). $\endgroup$ – wolfmanx Nov 2 '13 at 22:40
  • $\begingroup$ 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? $\endgroup$ – D.W. Nov 2 '13 at 23:47
  • $\begingroup$ @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 $\endgroup$ – wolfmanx Nov 6 '13 at 9:00
  • $\begingroup$ @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. $\endgroup$ – wolfmanx Nov 6 '13 at 9:11
8
$\begingroup$

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, 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, 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
  2. CNF Rule Hierarchy Discovery
  3. Good reference about approximate methods for solving logic problems
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – wolfmanx Nov 4 '13 at 8:01
  • $\begingroup$ Glad it could help. Hope you find the leads you need. $\endgroup$ – Vijay D Nov 4 '13 at 8:56
  • $\begingroup$ The definition you are giving is my definition of an unreliable partial assignment. So, no, your definition does not apply. $\endgroup$ – wolfmanx Nov 9 '13 at 18:45
  • $\begingroup$ 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. $\endgroup$ – Vijay D Nov 10 '13 at 0:20
  • $\begingroup$ 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 [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. $\endgroup$ – wolfmanx Nov 10 '13 at 0:52
1
$\begingroup$

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)

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – wolfmanx Nov 11 '13 at 7:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.