Talk:DPLL

From Wikipedia, the free encyclopedia

May or may not describe the same algorithm as Davis-Logemann-Loveland algorithm. If so, look to merge the two, while preserving all important information. - McCart42 (talk) 21:56, 22 September 2005 (UTC)

It is (or should be the same). The description at Davis-Logemann-Loveland algorithm has some quirks, but basically describes the DPLL algorithm. A merger is reasonable. But what name? I choose DPLL as the currently most used term ("DPLL method" or "DPLL algorithm" are alternatives). DLL is technically correct, but rarely used. I've never seen the long form Davis-Logemann-Loveland algorithm before. Davis-Putnam method is frequently used, but wrong. I vote for "DPLL" (well, I chose it ;-) or "DPLL algorithm". Other voices? --Stephan Schulz 22:13, 22 September 2005 (UTC)

I agree with the merge. I however disagree with DPLL for the only reason that DPLL also stands for Digital Phase Lock Loop (DPLL) while “Davis-Logemann-Loveland algorithm” is unambigous. I propose for the merge something like User:Paolo_Liberatore/DPLL, which starts (more or less) as the current DPLL article and then has a section on the algorithm that is from Davis-Logemann-Loveland. Comments? Paolo Liberatore (Talk) 11:00, 23 September 2005 (UTC)

I approve of the merged version on your userpage. Feel free to change it at the proper location unless anyone disagrees. - McCart42 (talk) 12:43, 23 September 2005 (UTC)

I like it as well (except for the original problems on the D-L-L page - I'll go over it when I have time). I suggest DPLL method or DPLL algorithm as the final name. It avoids the ambiguity with the Digital Phase Lock Loop, and I think it is a much more likely term to search for than the 3-long-names version. Wikipedia policy is to use the best-known term. At least from my reading that would either be the incorrect "Davis-Putnam algorithm/method" or one of the two I suggested. --Stephan Schulz 22:06, 23 September 2005 (UTC)

Ok. I copied the subpage into DPLL algorithm (including the stub sorting by User:Silverfish). Now Davis-Logemann-Loveland algorithm is a redirect and DPLL a disambiguation page. Paolo Liberatore (Talk) 11:55, 24 September 2005 (UTC)