Conflict-driven clause learning: Revision history

27 April 2025

• curprev 20:4720:47, 27 April 2025 William.Sørensen talk contribs m 16,454 bytes +7 Fix strange wording undo

20 February 2025

• curprev 04:3304:33, 20 February 2025 Zontasticality talk contribs 16,447 bytes −378 reformat the formalization section undo Tag: Visual edit: Switched

19 February 2025

• curprev 23:1223:12, 19 February 2025 Zontasticality talk contribs 16,825 bytes +6,348 add sequent calculus notation for CDCL rules undo Tag: Visual edit: Switched

7 December 2024

• curprev 12:1012:10, 7 December 2024 AnomieBOT talk contribs m 10,477 bytes +19 Dating maintenance tags: {{Citation needed}} undo
• curprev 10:1010:10, 7 December 2024 AksharVarma talk contribs m 10,458 bytes +19 →Applications: Request citation for "used effectively in several real world applications" undo

8 August 2024

• curprev 08:0108:01, 8 August 2024 Jochen Burghardt talk contribs 10,439 bytes −63 →References: now in side tab undo

7 August 2024

• curprev 23:4523:45, 7 August 2024 Pppery talk contribs 10,502 bytes +82 Why do I have to do everything manually? undo
• curprev 23:4323:43, 7 August 2024 Pppery talk contribs 10,420 bytes +126 Second attempt undo
• curprev 23:4023:40, 7 August 2024 Pppery talk contribs 10,294 bytes −164 Cleanup cite undo

24 July 2024

• curprev 06:1406:14, 24 July 2024 Pppery talk contribs 10,458 bytes +73 →Algorithm: Tag undo

17 May 2024

• curprev 04:4004:40, 17 May 2024 Golden heart talk contribs 10,385 bytes −13 It's absurd to put the "unsatisfied" here, because if the clause is really "unsatisfied", then we need force the free literal to be true, we must force it to be false in order to keep the clause "unsatisfied", so this description has serious error. undo

20 December 2023

• curprev 18:3318:33, 20 December 2023 InternetArchiveBot talk contribs 10,398 bytes +180 Rescuing 1 sources and tagging 0 as dead.) #IABot (v2.0.9.5 undo

16 December 2023

• curprev 02:1802:18, 16 December 2023 OAbot talk contribs m 10,218 bytes +18 Open access bot: doi updated in citation with #oabot. undo

5 December 2023

• curprev 21:4621:46, 5 December 2023 Siddharthist talk contribs m 10,200 bytes +3 Link to backjumping in the introduction undo Tag: 2017 wikitext editor

29 November 2023

• curprev 19:3819:38, 29 November 2023 AnomieBOT talk contribs m 10,197 bytes +19 Dating maintenance tags: {{Citation needed}} undo
• curprev 19:1819:18, 29 November 2023 Siddharthist talk contribs 10,178 bytes +19 →Related algorithms: Citation needed undo Tag: 2017 wikitext editor

30 August 2023

• curprev 15:4415:44, 30 August 2023 Cetrau talk contribs m 10,159 bytes +13 linked Sakallah's wiki page undo

3 June 2023

• curprev 11:3311:33, 3 June 2023 Paul2520 talk contribs 10,146 bytes +44 Adding short description: "SAT solving algorithm" undo Tag: Shortdesc helper

21 March 2023

• curprev 19:0419:04, 21 March 2023 Jochen Burghardt talk contribs 10,102 bytes +18 →Boolean satisfiability problem: keep proper remark about notation in the pictures, as long as they aren't adapted (in the long run, we should reduce the number of employed notation systems from currently 3 to at most 2) undo
• curprev 18:3118:31, 21 March 2023 Jopagu talk contribs m 10,084 bytes +73 Change negation symbol to the more commonly used notation, to match the later example on this page undo
• curprev 18:2318:23, 21 March 2023 204.144.209.97 talk 10,011 bytes +2 add quotes undo
• curprev 18:2218:22, 21 March 2023 204.144.209.97 talk 10,009 bytes +8 Fixed typo in reference to use the same symbols as in the example undo

28 February 2023

• curprev 19:3119:31, 28 February 2023 168.150.120.65 talk 10,001 bytes +1 →Example: Fixed typo: added ‘s’ to “variables” undo Tags: Mobile edit Mobile web edit

26 November 2022

• curprev 18:3318:33, 26 November 2022 Jochen Burghardt talk contribs 10,000 bytes +38 repeat notation footnote undo
• curprev 17:0217:02, 26 November 2022 Wlodr talk contribs m 9,962 bytes +4 link to implication graph where the notion appears first undo

15 November 2022

• curprev 22:5222:52, 15 November 2022 82.197.244.146 talk 9,958 bytes +54 No edit summary undo

14 September 2022

• curprev 13:1113:11, 14 September 2022 MHizzani talk contribs m 9,904 bytes +9 →Applications: change reference link for Glucose solver undo

29 May 2022

• curprev 07:4707:47, 29 May 2022 John of Reading talk contribs 9,895 bytes +1,264 Reverted 1 edit by 102.250.1.74 (talk): Unexplained deletion undo Tags: Twinkle Undo

28 May 2022

• curprev 23:5723:57, 28 May 2022 102.250.1.74 talk 8,631 bytes −1,264 No edit summary undo Tags: Reverted references removed Visual edit Mobile edit Mobile web edit

9 March 2022

• curprev 22:4922:49, 9 March 2022 Mathnerd314159 talk contribs 9,895 bytes −1,793 remove DP/DPLL sections. WP:COATRACK undo

2 January 2022

• curprev 14:4714:47, 2 January 2022 Willondon talk contribs m 11,688 bytes −105 →Background: unnecessary statement undo
• curprev 14:1614:16, 2 January 2022 80.214.214.248 talk 11,793 bytes +1 →Completeness: wording undo Tags: Mobile edit Mobile app edit Android app edit

16 October 2021

• curprev 10:4110:41, 16 October 2021 Citation bot talk contribs 11,792 bytes +75 Add: s2cid, title. Changed bare reference to CS1/2. | Use this bot. Report bugs. | Suggested by BrownHairedGirl | Linked from User:BrownHairedGirl/Articles_with_bare_links | #UCB_webform_linked 1354/2198 undo

6 December 2020

• curprev 02:2702:27, 6 December 2020 Monkbot talk contribs m 11,717 bytes −30 Task 18 (cosmetic): eval 8 templates: del empty params (3×); hyphenate params (3×); undo Tag: AWB

24 November 2020

• curprev 10:3810:38, 24 November 2020 176.128.128.82 talk 11,747 bytes +63 Add a new solver with reference undo

23 June 2020

• curprev 23:0523:05, 23 June 2020 OAbot talk contribs m 11,684 bytes +48 Open access bot: hdl added to citation with #oabot. undo

14 May 2020

• curprev 08:3708:37, 14 May 2020 Kku talk contribs m 11,636 bytes +4 link state space search using Find link undo

11 May 2019

• curprev 13:2813:28, 11 May 2019 Texvc2LaTeXBot talk contribs m 11,632 bytes +12 Replacing deprecated latex syntax mw:Extension:Math/Roadmap undo

8 April 2019

• curprev 15:5515:55, 8 April 2019 Jochen Burghardt talk contribs 11,620 bytes −16 →CDCL (conflict-driven clause learning): ditto undo
• curprev 15:5415:54, 8 April 2019 Jochen Burghardt talk contribs 11,636 bytes −12 →DPLL algorithm: rm extra indentation undo
• curprev 15:5315:53, 8 April 2019 Jochen Burghardt talk contribs 11,648 bytes −40 →DPLL algorithm: ditto undo
• curprev 15:5315:53, 8 April 2019 Jochen Burghardt talk contribs 11,688 bytes −71 →DP algorithm: rm "see more details" in presence of ((main)) undo

27 March 2019

• curprev 10:3110:31, 27 March 2019 2a02:2c40:500:a006:f9d0:9965:ba4f:12 talk 11,759 bytes −2 →DPLL algorithm: uses chronological backtracking, without learning undo

10 March 2019

• curprev 02:1102:11, 10 March 2019 Citation bot talk contribs m 11,761 bytes −1 Alter: contribution, title. Add: citeseerx, isbn. Removed URL that duplicated unique identifier. | You can use this bot yourself. Report bugs here. | User-activated. undo

6 November 2018

• curprev 10:2110:21, 6 November 2018 Jochen Burghardt talk contribs 11,762 bytes +7 →Boolean satisfiability problem undo
• curprev 10:2010:20, 6 November 2018 Jochen Burghardt talk contribs 11,755 bytes +102 →Boolean satisfiability problem: explain notation "+" and "(...)(...)" in the pictures undo

5 November 2018

• curprev 15:3015:30, 5 November 2018 46.193.2.51 talk 11,653 bytes +15 →Boolean satisfiability problem: Use the commonly accepted notation for CNF/SAT problems undo

26 September 2018

• curprev 14:4514:45, 26 September 2018 The Anome talk contribs 11,638 bytes 0 casing undo Tag: Visual edit
• curprev 10:3610:36, 26 September 2018 The Anome talk contribs m 11,638 bytes 0 The Anome moved page Conflict-Driven Clause Learning to Conflict-driven clause learning undo
• curprev 10:3610:36, 26 September 2018 The Anome talk contribs 11,638 bytes +10 fmt undo Tag: Visual edit