Davis–Putnam algorithm: Revision history

5 August 2024

• curprev 20:5920:59, 5 August 2024 Macrakis talk contribs 7,255 bytes +60 Adding short description: "Check the validity of a logic formula" undo Tag: Shortdesc helper

8 May 2024

• curprev 06:4406:44, 8 May 2024 MarkH21 talk contribs 7,195 bytes +39 introduce subject first undo

9 February 2024

• curprev 19:1819:18, 9 February 2024 MrOllie talk contribs 7,156 bytes −89 →External links: WP:ELNO undo

25 January 2024

• curprev 17:3417:34, 25 January 2024 Citation bot talk contribs 7,245 bytes −73 Removed proxy/dead URL that duplicated identifier. | Use this bot. Report bugs. | Suggested by Abductive | Category:Automated theorem proving | #UCB_Category 9/39 undo

22 January 2024

• curprev 01:4501:45, 22 January 2024 Eejit43Bot talk contribs m 7,318 bytes −26 [Task 2] Fix improperly capitalized section headers, general fixes, removed stub tag undo Tag: AWB

3 January 2024

• curprev 14:5014:50, 3 January 2024 Choltreppe talk contribs m 7,344 bytes +90 add link to a website where you can run davis-putnam on any boolean expression undo

15 December 2023

• curprev 23:5623:56, 15 December 2023 OAbot talk contribs m 7,254 bytes +19 Open access bot: doi updated in citation with #oabot. undo

16 April 2023

• curprev 20:4820:48, 16 April 2023 67.185.21.25 talk 7,235 bytes −1 →Overview: as requested undo Tags: Mobile edit Mobile web edit

15 April 2023

• curprev 15:1815:18, 15 April 2023 Jochen Burghardt talk contribs 7,236 bytes +14 →Overview: attempt to prevent reader's question 'same polarity as what?'; not sure whether 'whichs' is proper English, please fix if necessary undo
• curprev 08:2608:26, 15 April 2023 Jabberwockk talk contribs m 7,222 bytes +95 added removal of clauses with positive literal l in unit propagation, before only the unit clause was removed undo Tag: Visual edit

12 February 2022

• curprev 12:4112:41, 12 February 2022 EmilJ talk contribs 7,127 bytes +7 →Overview: "For every" is not appropriate, as pure literal elimination may create new pure literals. undo
• curprev 11:2911:29, 12 February 2022 EmilJ talk contribs 7,120 bytes +89 →Overview: The stopping conditions should be moved right before the DP procedure to ensure that there IS a non-pure literal undo
• curprev 11:2411:24, 12 February 2022 EmilJ talk contribs 7,031 bytes +17 →Overview: Unit propagation etc. is supposed to be done before EACH elimination of a literal l by the DP procedure, thus the loop should be moved outwards. In fact, there is no need to make this formally a recursive algorithm. undo
• curprev 11:1611:16, 12 February 2022 EmilJ talk contribs 7,014 bytes +296 →Overview: Resolution is not a function of c and n only, it also depends on the choice of l. Better to spell this out. Unit propagation is also easy to spell out to reduce dependence on unexplained functions. undo
• curprev 11:0411:04, 12 February 2022 EmilJ talk contribs 6,718 bytes +114 →Overview: This is a confusing name, as the procedure as given does not construct a satisfying assignment, it only checks satisfiability. In fact, it's easiest to just spell it out. undo
• curprev 11:0011:00, 12 February 2022 EmilJ talk contribs 6,604 bytes +132 →Overview: Even if not present in the original formula, the resolution step may generate clauses that contain a variable with both polarities. These better be be eliminated. undo
• curprev 10:5410:54, 12 February 2022 EmilJ talk contribs 6,472 bytes −23 →Overview: Wth? Φ is never a set of literals, but a set of clauses. What is meant here is that Φ consists of a single nonempty clause; this is not enough, as it does not catch the case when Φ is empty, and on the other hand, the single clause would be immediately eliminated by pure literal elimination anyway. Thus, it's easiest to just check for Φ being empty. undo
• curprev 10:2810:28, 12 February 2022 EmilJ talk contribs 6,495 bytes +104 →Overview: The algorithm is wrong. You can't remove c and n immediately. You FIRST have to resolve ALL pairs c and n, and THEN you can remove them. This is outside the previous loop, so no c and n are in scope any longer. undo

19 November 2021

• curprev 12:4412:44, 19 November 2021 Frap talk contribs m 6,391 bytes +2 Hyphen undo

27 September 2021

• curprev 02:4202:42, 27 September 2021 Mandarax talk contribs m 6,389 bytes +1 ilustration->illustration - Fix a typo in one click undo

24 June 2021

• curprev 10:2310:23, 24 June 2021 AnomieBOT talk contribs m 6,388 bytes +15 Dating maintenance tags: {{Clarify}} undo
• curprev 10:0210:02, 24 June 2021 Jochen Burghardt talk contribs 6,373 bytes +311 →Overview: rm left-over text; ask for explanation of add/remove (was inclear in the previous version already) etc.; specify i/o relation of alg. undo

23 June 2021

• curprev 23:2023:20, 23 June 2021 KamillaŚ talk contribs 6,062 bytes +1,398 i had to write this algorithm for classes so im making wikipedia correct. maybe not the most understandable already but correct. undo Tag: Visual edit: Switched

6 December 2020

• curprev 13:4213:42, 6 December 2020 Monkbot talk contribs m 4,664 bytes −46 Task 18 (cosmetic): eval 4 templates: del empty params (3×); hyphenate params (1×); undo Tag: AWB

20 July 2020

• curprev 19:1219:12, 20 July 2020 Galebazz talk contribs 4,710 bytes −550 Undid revision 968664324 by Johnaearley86 (talk): Identified as test/vandalism using m:WikiLoop DoubleCheck version 4.1.0. See it or provide your opinion at http://doublecheck.wikiloop.org/revision/enwiki/968664324 undo Tag: Undo
• curprev 19:1019:10, 20 July 2020 Johnaearley86 talk contribs 5,260 bytes +550 blupt undo Tags: Visual edit Mobile edit Mobile web edit

13 June 2020

• curprev 20:5420:54, 13 June 2020 OAbot talk contribs m 4,710 bytes +48 Open access bot: hdl added to citation with #oabot. undo

9 June 2020

• curprev 22:2722:27, 9 June 2020 InternetArchiveBot talk contribs 4,662 bytes +137 Bluelink 1 book for verifiability (prndis)) #IABot (v2.0.1) (GreenC bot undo

6 November 2019

• curprev 16:4316:43, 6 November 2019 Jochen Burghardt talk contribs 4,525 bytes −4 →References: undo rest of vandalism edit of 13 January 2014, the first part of which was fixed today undo
• curprev 02:0302:03, 6 November 2019 2607:fea8:3d60:92b:a59d:3069:4edc:6918 talk 4,529 bytes −5 →References undo

3 May 2019

• curprev 13:5613:56, 3 May 2019 Rodw talk contribs m 4,534 bytes +29 Disambiguating links to Martin Davis (link changed to Martin Davis (mathematician)) using DisamAssist. undo

8 April 2019

• curprev 16:4316:43, 8 April 2019 Jochen Burghardt talk contribs 4,505 bytes +14 →Overview: refer to picture, also to make clear for which steps it presents examples undo
• curprev 16:3416:34, 8 April 2019 Jochen Burghardt talk contribs 4,491 bytes +684 →Overview: suggest image undo

18 April 2017

• curprev 19:2019:20, 18 April 2017 Michael Hardy talk contribs 3,807 bytes +2 No edit summary undo

27 December 2016

• curprev 18:1618:16, 27 December 2016 Omnipaedista talk contribs 3,805 bytes −29 rm obsolete tag undo

21 May 2015

• curprev 19:5119:51, 21 May 2015 Jochen Burghardt talk contribs 3,834 bytes −6 fix wrong reference by "it" undo
• curprev 19:4819:48, 21 May 2015 Jochen Burghardt talk contribs 3,840 bytes +130 →top: devote an own paragraph to DPLL, as it is the best algorithm as of today undo
• curprev 19:4519:45, 21 May 2015 Jochen Burghardt talk contribs 3,710 bytes −108 Undid own revision 663446391: DPLL was already mentioned in article undo
• curprev 19:4219:42, 21 May 2015 Jochen Burghardt talk contribs 3,818 bytes +108 →See also undo

17 May 2015

• curprev 17:3417:34, 17 May 2015 Trappist the monk talk contribs m 3,710 bytes 0 →References: replace/remove deprecated cs1|2 parameters; using AWB undo

8 March 2015

• curprev 10:3610:36, 8 March 2015 Yobot talk contribs m 3,710 bytes −1 Removed invisible unicode characters + other fixes using AWB (10850) undo

7 March 2015

• curprev 09:3909:39, 7 March 2015 Magioladitis talk contribs 3,711 bytes −722 Undid revision 649954517 by 210.212.242.166 (talk) this seems to be pasted from another site. it contains characters in PUA. It also broke layout undo

5 March 2015

• curprev 06:3306:33, 5 March 2015 210.212.242.166 talk 4,433 bytes +722 →See also undo

7 May 2014

• curprev 15:3315:33, 7 May 2014 Monkbot talk contribs m 3,711 bytes −9 →References: Task 3: Fix CS1 deprecated coauthor parameter errors undo

29 March 2014

• curprev 00:3600:36, 29 March 2014 Monkbot talk contribs m 3,720 bytes −11 →References: Task 1c: Fix CS1 deprecated date parameter errors undo

27 January 2014

• curprev 10:2110:21, 27 January 2014 Ugog Nizdast talk contribs m 3,731 bytes −46 Reverted 1 edit by Dorybadboy identified as test/vandalism using STiki undo
• curprev 10:1610:16, 27 January 2014 Dorybadboy talk contribs m 3,777 bytes +46 No edit summary undo Tag: gettingstarted edit

12 January 2014

• curprev 23:1223:12, 12 January 2014 Starswager18 talk contribs 3,731 bytes +10 No edit summary undo Tag: gettingstarted edit

4 January 2014

• curprev 23:4023:40, 4 January 2014 Myasuda talk contribs m 3,721 bytes −1 →References: sp undo

24 December 2013

• curprev 21:4721:47, 24 December 2013 DemocraticLuntz talk contribs 3,722 bytes −19 Reverted 1 good faith edit by 197.206.150.100 using STiki undo