Talk:DPLL algorithm

Subsumption

I've checked the original CACM-1962 paper, and it does not mention subsumption in the DPLL algorithm at all. The three rules are I) the one literal clause rule, now known as "unit propagation", II) affirmative-negative rule, now "pure literal elemination", and III*) Splitting Rule, still known under that name. The authors do mention "systematic elemination of redundancy", but only with respect to the original Davis-Putnam algorithm, not with respect to DPLL. I'll revert todays change (with some extra clarification). If anyone has more information, I'm interested in hearing it. --Stephan Schulz 17:40, 24 October 2005 (UTC)

Ok. I had based my description on not-so-recent papers. In particular, I think that one by Crawford and Auton mentioned the clause subsumption rule (and said it was not useful); the fact that the pure literal rule was decided not useful seems to be a very recent finding--I didn't know it. User:Tizio 18:23, 24 October 2005 (UTC)

The "two watch literal" technique pioneered in Chaff has made unit propagation very cheap. In particular, it makes the speed of unit propagation nearly independent of the number of clauses. Thus the gain of a smaller (by number of clauses) formula is nearly nil, while a comparable breakthrough in searching for pure literals has not yet been found. --Stephan Schulz 18:53, 24 October 2005 (UTC)

Good to know! Thanks for the clarification. User:Tizio 21:39, 24 October 2005 (UTC)

In the DPLL pseudocode, why is the second argument provided, given that it is neither used nor returned? Wouldn't the pseudocode be clearer and shorter without this second argument? If the second argument were to be retained, shouldn't the text describe how the algorithm can be modified to return a satisfying truth assignment if there is one? 58.162.12.107 04:10, 29 October 2006 (UTC)

But it is used, in the recursive calls to the sub-provers. It's not returned, though. I've added a note to this effect.--Stephan Schulz 22:54, 29 October 2006 (UTC)

It is true that is used to call the recursive calls, but it is never used in that function, and it is never passed to a different function. In the current example, we don't care about what is the whole current assignation of variables, we only care about the current assignation, but not even that is necessary to pass because we simplify the formula before calling DPLL again. I also think this should be changed. This argument could be usefull if in the middle of the program we would need to now about the previous assignments that have been done, but not otherwise. —Preceding unsigned comment added by 85.54.228.63 (talk • contribs) 02:53, 6 August 2007

Indeed, since assigned literals are added to the formula, there is no need to carry the assignment to the recursive calls. Tizio 08:50, 6 August 2007 (UTC)

CNF is ambiguous

The article goes

The DPLL algorithm can be summarized in the following pseudocode, where Φ is the CNF formula:

Does CNF mean Conjunctive normal form or Clausal normal form in this context? Also see CNF —Preceding unsigned comment added by 146.133.1.43 (talk) 09:28, 7 November 2007 (UTC)

It does not matter. The two are strictly isomorphic (and fairly obviously so for propositional logic). --Stephan Schulz 10:24, 7 November 2007 (UTC)

Here CNF is Conjunctive Normal Form.

Pseudo code is ambiguous

Seems to me that the 'l' variable is used to represent both unit clause and literal:

  for every unit clause l in Φ
     Φ=unit-propagate(l, Φ);
  for every literal l that occurs pure in Φ
     Φ=pure-literal-assign(l, Φ);
  l := choose-literal(Φ);

Wouldn't it be clearer to have:

  for every unit clause {l} in Φ
     Φ=unit-propagate(l, Φ);
  for every literal l that occurs pure in Φ
     Φ=pure-literal-assign(l, Φ);
  l := choose-literal(Φ);

Very confusing the way it is currently... —Preceding unsigned comment added by 192.94.38.34 (talk) 01:49, 15 November 2007 (UTC)

Instead of killing the author in plenty of painful ways, I'd suggest rewriting the pseudocode so that it doesn't use variables which are single letters, but instead names them with respect to their role in the algorithm. Still I cannot resist suggesting a special warm place in hell should be reserved for those who use minuscule Latin letter "L" to name variables. I could see them fitting nicely together, right next to those who use inconsistent spacing and minus signs in function names in the same time they use infix math operators. Aren't there any standards for how code should be written in Wiki? PS. This algorithm in its current form worth nothing w/o "unit propagation" and "pure literal assign" being defined. 79.176.130.107 (talk) 23:01, 19 October 2013 (UTC)

Purity elimination eliminated

I'm a bit concerned about the complete elimination of the text on purity. As far as I know, most modern solvers indeed omit it (MiniSAT does not seem to implement it, and Chaff and Berkmin certainly don't. See [1]). --Stephan Schulz (talk) 21:17, 24 June 2011 (UTC)

Of course, nowadays solvers do not use this algorithm, they use the CDCL algorithm. See the CDCL algorithm's page. — Preceding unsigned comment added by 163.5.55.13 (talk) 14:15, 22 December 2015 (UTC)

2 watched literals

A possible addition to the article could be that modern SAT solver use "2 watched literals" to efficiently implement DPLL. — Preceding unsigned comment added by RainCT (talk • contribs) 11:44, 22 January 2012 (UTC)

The 2 watched literals is a structure used with the CDCL algorithm. — Preceding unsigned comment added by 163.5.55.13 (talk) 14:24, 22 December 2015 (UTC)

Problem in the example

I think there is a problem in the example. After assigning a to 0, b should be assigned to 0 due to the pure literal rule and not to a decision. — Preceding unsigned comment added by Ludowsky (talk • contribs) 14:37, 22 December 2015 (UTC)

Purity explained

If a propositional variable occurs with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses do not constrain the search anymore and can be deleted.

I know very little about this subject, and this statement initially puzzled me, until my brain recalled that these formulas are all in CNF, and this is probably the reason why purity makes these variables so amenable to hustling out the back door. — MaxEnt 18:11, 16 April 2018 (UTC)

Expository significance

If you look at the CDCL page, the lead (at present) basically says "we're not good at explaining things top down here" with a veiled hint to come visit this page instead. Plan B is to drape a bib over your chest and enter into the "begin at the beginning narrative" of the core CDCL exposition.

Sometimes old is good pedagogically.

Perhaps this page should strive for unusual clarity, despite being yesterday's news, after all. — MaxEnt 18:16, 16 April 2018 (UTC)

Pure literal elimination

@Jochen Burghardt:Hi again, No the title is "Pure literal elimination", so here "literal" is deleted not clause.

Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.

I think the correct word is literal. Thanks,Hooman Mallahzadeh (talk) 13:58, 2 May 2021 (UTC)

Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm.

Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! Hooman Mallahzadeh (talk) 14:16, 2 May 2021 (UTC)

@Jochen Burghardt: Yes you are right, here

In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.

So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. Hooman Mallahzadeh (talk) 14:28, 2 May 2021 (UTC)

@Jochen Burghardt: I correct the sentence, to remove this ambiguity. Please inspect it. Thanks, Hooman Mallahzadeh (talk) 14:36, 2 May 2021 (UTC)

Now that I've typed it in, I'll show my reply anyway:

For example, in the CNF (w ∨ x ∨ ¬z) ∧ (x ∨ ¬y ∨ z) ∧ (¬w ∨ ¬y ∨ z) ∧ (¬w ∨ ¬x ∨ z) the variable y occurse only negated, it is hence pure. By assigning FALSE to y, all clauses containing ¬y can be satisfied. The remaining problem is just to satisfy the clauses that don't contain ¬y, that is, those remaining after deleting all clauses containing ¬y. In the example: (w ∨ x ∨ ¬z) ∧ (¬w ∨ ¬x ∨ z). Deleting only the literal ¬y everywhere would leave an unneccessarily complicated problem.

Assigning an appropriate truth value to a pure literal preserves satisfiability. In the example, if the original CNF can be satisfied, then the reduced one can be satisfied, too, since it is a subproblem. Vice versa, if the reduced CNF is satisfied by an assignment, then extending it by y:=FALSE will yield a satsifying assignment for the original CNF. So, we don't need both branches.

I guess the name "pure literal elimination" is motivated by the fact that a pure literal is needed to apply the rule. Maybe, it should merely be read as "elimination (of clauses) based on pure literals", rather than as "elimination of pure literals (and nothing else)". The literal if eliminated by eliminating the clause it is contained in. - Jochen Burghardt (talk) 14:39, 2 May 2021 (UTC)

1958 & NSA

Would it be worthwhile to update the page w/ information in the originating 1958 NSA report?

Link to paper and exposition - [2] — Preceding unsigned comment added by 2601:14D:4400:570:EC40:8323:DAA4:F6F9 (talk) 13:34, 6 October 2022 (UTC)