<?xml version="1.0" encoding="UTF-8"?>
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom" xmlns:dc="http://purl.org/dc/elements/1.1/">
  <channel>
    <title>Forem: Lahari</title>
    <description>The latest articles on Forem by Lahari (@obanai).</description>
    <link>https://forem.com/obanai</link>
    <image>
      <url>https://media2.dev.to/dynamic/image/width=90,height=90,fit=cover,gravity=auto,format=auto/https:%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Fuser%2Fprofile_image%2F2208474%2Fec0f9153-d21f-443f-bac6-bc827ad96eb7.jpeg</url>
      <title>Forem: Lahari</title>
      <link>https://forem.com/obanai</link>
    </image>
    <atom:link rel="self" type="application/rss+xml" href="https://forem.com/feed/obanai"/>
    <language>en</language>
    <item>
      <title>Hare and Tortoise - To Find Start of Loop in Linked List</title>
      <dc:creator>Lahari</dc:creator>
      <pubDate>Thu, 12 Dec 2024 20:03:05 +0000</pubDate>
      <link>https://forem.com/obanai/hare-and-tortoise-to-find-start-of-loop-in-linked-list-2eei</link>
      <guid>https://forem.com/obanai/hare-and-tortoise-to-find-start-of-loop-in-linked-list-2eei</guid>
      <description>&lt;h2&gt;
  
  
  A &lt;em&gt;tiny&lt;/em&gt; bit of background
&lt;/h2&gt;

&lt;p&gt;"Hare and Tortoise!" - cool name, right? Well, the algorithm is even cooler! Frankly, there were points in my life when I was fuming at this algo, and it was just sitting there, legs crossed on the couch's arm, smoking a cigar, smiling smoothly, and watching me suffer... But! Things changed, and now I am the one on the couch, and it's my pet now (preferably with a leash, no offense to pet lovers! Though it does feel a bit offensive, sorry!)&lt;/p&gt;

&lt;h2&gt;
  
  
  What Is This Algo??
&lt;/h2&gt;

&lt;p&gt;It's composed of one thing- an awesome and brilliant logic. Its aim is to find the starting node of the loop in a linked list, if one exists. &lt;/p&gt;

&lt;h2&gt;
  
  
  The &lt;strong&gt;Brilliant Logic&lt;/strong&gt; Behind The Scenes -
&lt;/h2&gt;

&lt;p&gt;It is common knowledge that "Hare runs faster than Tortoise". Similarly, we have a hare pointer and a tortoise pointer in our algorithm. Since 'tortoise' is too lengthy and we're too lazy, let's go with the conventional names- fast pointer and slow pointer. (Because it's ugly to call them hare and slow pointers.)&lt;/p&gt;

&lt;h3&gt;
  
  
  See how they run- (oh, I &lt;em&gt;love&lt;/em&gt; that movie!)
&lt;/h3&gt;

&lt;p&gt;fast_ptr goes two steps and slow_ptr takes one at a time. If no loop is present, fast_ptr would eventually be null (or at least its next node will be). Else the fast_ptr would eventually catch up with slow_ptr (like Cap does with Sam Wilson). Now let's take a break and reflect on these two. (Sipping milk:)...) Yeah, break time's over, let's warm up:&lt;/p&gt;

&lt;blockquote&gt;
&lt;p&gt;If fast_ptr or its next node becomes NULL: return NULL (coz there's no 'loop' for us to return the starting point of the 'loop')&lt;br&gt;
Else we know there's a loop and that both fast_ptr and slow_ptr are inside the loop, each pointing to (some) same node&lt;/p&gt;
&lt;/blockquote&gt;

&lt;h3&gt;
  
  
  Time for a dash of magic (or some logic)
&lt;/h3&gt;

&lt;p&gt;Say, the length from head until the start_of_loop(S) is 'a' and the extra distance from start_of_loop till meeting_point(M) is 'b'. Let the remaining unnamed length be 'y'. &lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fj92ftujn2n2xbdgu1yw1.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fj92ftujn2n2xbdgu1yw1.png" alt="Visualization" width="800" height="203"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;Now Here's what I call a &lt;em&gt;'good observation'&lt;/em&gt;:
The extra length travelled by fast_ptr is equal to a+b. Because the fact that fast_ptr took 2 steps while slow_ptr took only one means that the distance traveled by fast_ptr is twice that traveled by slow_ptr. &lt;/li&gt;
&lt;li&gt;Distance traveled by slow_ptr = a+b. So, the distance traveled by fast_ptr is 2(a+b). &lt;/li&gt;
&lt;li&gt;Like slow_ptr, fast_ptr also covered a distance of a+b initially. And then it traveled 'an extra distance y and b' (say some 'n' times) to meet the slow_ptr.&lt;/li&gt;
&lt;li&gt;So basically, the extra distance covered by fast_ptr was n(y+b) which is equal to a+b. (2(a+b)-(a+b) = a+b)&lt;/li&gt;
&lt;/ul&gt;

&lt;blockquote&gt;
&lt;p&gt;

&lt;span class="katex-element"&gt;
  &lt;span class="katex"&gt;&lt;span class="katex-mathml"&gt;n(y+b)=a+b=&amp;gt;a=n(y+b)−bn(y+b)=a+b =&amp;gt; a = n(y+b)-b &lt;/span&gt;&lt;span class="katex-html"&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;n&lt;/span&gt;&lt;span class="mopen"&gt;(&lt;/span&gt;&lt;span class="mord mathnormal"&gt;y&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mbin"&gt;+&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;b&lt;/span&gt;&lt;span class="mclose"&gt;)&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mrel"&gt;=&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;a&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mbin"&gt;+&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;b&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mrel"&gt;=&amp;gt;&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;a&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mrel"&gt;=&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;n&lt;/span&gt;&lt;span class="mopen"&gt;(&lt;/span&gt;&lt;span class="mord mathnormal"&gt;y&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mbin"&gt;+&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;b&lt;/span&gt;&lt;span class="mclose"&gt;)&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;span class="mbin"&gt;−&lt;/span&gt;&lt;span class="mspace"&gt;&lt;/span&gt;&lt;/span&gt;&lt;span class="base"&gt;&lt;span class="strut"&gt;&lt;/span&gt;&lt;span class="mord mathnormal"&gt;b&lt;/span&gt;&lt;/span&gt;&lt;/span&gt;&lt;/span&gt;
&lt;/span&gt;
 | This equation suggests that going through the loop n times, while skipping a distance of 'b', is same as traveling a distance of 'a'. &lt;/p&gt;
&lt;/blockquote&gt;

&lt;ul&gt;
&lt;li&gt;The above statement can also be interpreted in another way- if some 'ptr1' is to travel a distance 'a+b' and a 'ptr2' is to travel ny+(n-1)b starting from M, they would point to same node (meeting_point) at the end of the journey. &lt;/li&gt;
&lt;li&gt;But, since both are travelling at same speeds (one step at a time), they would already be pointing to same nodes long before they reach meeting_point. &lt;/li&gt;
&lt;li&gt;To conclude, both the pointers would have pointed to same node since the start_of_loop. So, the first node where "ptr1==ptr2" would be the start node of the loop.&lt;/li&gt;
&lt;li&gt;Therefore, if the hare_ptr starts from the head node again, this time slowing down, and taking one step at a time (because it's tired running all his life), and the slow_ptr resumes from meeting_point and try to go over the loop, both will meet at the start_of_loop.&lt;/li&gt;
&lt;/ul&gt;

&lt;h3&gt;
  
  
  Algorithm in C/C++
&lt;/h3&gt;



&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;Node *startNodeOfLoop(Node *head)
{
    Node *fast = head, *slow = head;
    while(fast &amp;amp;&amp;amp; fast-&amp;gt;next){
        slow = slow-&amp;gt;next;
        fast = fast-&amp;gt;next-&amp;gt;next;
        if(fast==slow) {
            fast = head;
            while(fast!=slow){
                fast = fast-&amp;gt;next;
                slow = slow-&amp;gt;next;
            }
            return fast;
        }
    }
    return NULL;
}
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;h2&gt;
  
  
  Epilogue
&lt;/h2&gt;

&lt;p&gt;Ah, Man! that was exhaustingly lengthy (longer than I intended). Nonetheless, I &lt;em&gt;really&lt;/em&gt; hope you are on the couch with the algorithm's leash in your hand. The Hare &amp;amp; Tortoise algorithm described above is also known as Floyd's Cycle-Finding Algorithm. It's a brilliant and efficient solution to the problem of detecting cycles in a linked list. I believe that it is algorithms like these that remind me where true beauty resides while solving problems the programmer's way. Adios!!&lt;/p&gt;

</description>
      <category>algorithms</category>
      <category>programming</category>
      <category>tutorial</category>
      <category>datastructures</category>
    </item>
    <item>
      <title>Kadane's Algorithm - For Max SubArray Sum</title>
      <dc:creator>Lahari</dc:creator>
      <pubDate>Sun, 08 Dec 2024 17:14:40 +0000</pubDate>
      <link>https://forem.com/obanai/kadanes-algo-for-max-sum-sub-array-4e5p</link>
      <guid>https://forem.com/obanai/kadanes-algo-for-max-sum-sub-array-4e5p</guid>
      <description>&lt;h2&gt;
  
  
  Introduction
&lt;/h2&gt;

&lt;p&gt;&lt;em&gt;SPOILER ALERT: This section is specifically dedicated to bragging about Kadane, not the algorithm. So, feel free to skip this section. (No, I am kidding! I'd actually prefer that you read it...)&lt;/em&gt;&lt;br&gt;
Joseph "Jay" Born Kadane (whose full name I just gathered from Wikipedia) is the scientist who published this algorithm I am going to talk about. I am nothing but in awe for this man. It's been a year since I've known this algorithm, but whenever I think of this algo, I can't help but feel immense respect and look up to him. This algorithm is so simple once you understand it but that wouldn't degrade any of its charisma. Instead, (I do and suppose that) you will feel a sense of accomplishment and the warmth in your chest. That's the effect of brilliant logic that even novices like us can implement—it touches the heart! (In a modest claim, we're not novices; we're outstanding. Or perhaps outstanding novices...) With the "irrelevant" part out of the way, let's delve into the essence.&lt;/p&gt;

&lt;h2&gt;
  
  
  Explanation
&lt;/h2&gt;

&lt;p&gt;&lt;strong&gt;Problem statement:&lt;/strong&gt; You need to find the sum of the subarray having maximum sum among all subarrays of given integer array.&lt;br&gt;
&lt;strong&gt;The Algo:&lt;/strong&gt; &lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;The problem statement mentions "integer array". Which means negative integers included. We obviously don't want to add a negative integer to get maximum sum... but it has a downside -&lt;/li&gt;
&lt;/ul&gt;

&lt;blockquote&gt;
&lt;p&gt;Say the array has elements - 7 1 -4 5&lt;br&gt;
If you're stopping at 7+1 = 8, you have a sub-optimal solution.&lt;br&gt;
Because 7+1-4+5 = 9&lt;/p&gt;
&lt;/blockquote&gt;

&lt;ul&gt;
&lt;li&gt;So instead, we'll stop adding when the &lt;em&gt;sum&lt;/em&gt; becomes -ve. This does not have any downsides. Because whatever sum lies ahead of this point, is better off without this negative sum decreasing its value.&lt;/li&gt;
&lt;li&gt;But we're not sure if a sum that's calculated up until this point will be greater or the sum that's yet to be calculated newly, somewhere beyond this point.&lt;/li&gt;
&lt;li&gt;Therefore, we maintain a maxSum variable that would, at a given instance of time, store the maximum sum calculated since the start, up until then.&lt;/li&gt;
&lt;/ul&gt;

&lt;p&gt;I hope you're not confused. If you are, take a look at this code and read those lines again.&lt;/p&gt;

&lt;h3&gt;
  
  
  Algorithm
&lt;/h3&gt;



&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;maxSum,sum &amp;lt;- (-infinity)
loop {
   sum &amp;lt;- sum + ele
   maxSum &amp;lt;- Maximum(sum, maxSum)
   if (sum &amp;lt; 0) {
      sum = 0
   }
}
return maxSum
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;ul&gt;
&lt;li&gt;
&lt;strong&gt;NOTE:&lt;/strong&gt; In every iteration, maxSum is updated not caring whether the sum is -ve or not. It might strike you as a redundancy. After all, (sum &amp;gt; maxSum) is possible only when sum&amp;gt;0. But think about an array with all -ve integers- because the sum is always -ve, the maxSum never gets updated from (-infinity) to the least negative integer. There are other cases too. So, it's important to try to update maxSum in each iteration.&lt;/li&gt;
&lt;/ul&gt;

&lt;h3&gt;
  
  
  Returning Subarray
&lt;/h3&gt;

&lt;ul&gt;
&lt;li&gt;Where is the fun in returning just the maxSum?? Let's return the subarray that produces the maxSum!!&lt;/li&gt;
&lt;li&gt;Don't feel overwhelmed! All we have to do is figure out the start and the end of the subarray.&lt;/li&gt;
&lt;li&gt;So, while calculating a sum, we obviously need to know where it started. For this, we'll have a 'startIndex' variable. But we don't actually need the endIndex because we're not sure if the current sum is going to be the maxSum. Instead, we'll have 'actualStart', 'actualEnd' variables indicating the start and end indices of the sum which is in maxSum variable. &lt;/li&gt;
&lt;li&gt;Whenever maxSum variable is (actually) updated, current startIndex will be actualStart and current index will be actualEnd.
&lt;/li&gt;
&lt;/ul&gt;

&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;maxSum,sum &amp;lt;- (-infinity)
startIndex, actualStart &amp;lt;- 0
loop {
   sum &amp;lt;- sum + ele
   if (sum &amp;gt; maxSum) {
      maxSum &amp;lt;- sum
      actualStart &amp;lt;- startIndex
      actualEnd &amp;lt;- current_index
   }
   if (sum &amp;lt; 0) {
      sum = 0
      startIndex = current_index
   }
}
return array[actualStart..actualEnd]
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;h2&gt;
  
  
  Conclusion
&lt;/h2&gt;

&lt;p&gt;Kadane's Algorithm is a brilliant example of how simple logic can solve complex problems efficiently. By understanding and implementing this algorithm, you can find the maximum subarray sum in linear time. Give it a try (in your favorite programming language), I am sure you'll ace it!!&lt;/p&gt;

&lt;p&gt;&lt;strong&gt;P.S.:&lt;/strong&gt; Did you know that Kadane's Algorithm is an iterative dynamic programming algorithm? I've never seen a simpler DP algorithm than this!&lt;/p&gt;

</description>
      <category>algorithms</category>
      <category>dp</category>
      <category>programming</category>
      <category>tutorial</category>
    </item>
    <item>
      <title>DPLL: All-Time Hit SAT-Solver</title>
      <dc:creator>Lahari</dc:creator>
      <pubDate>Sat, 07 Dec 2024 11:44:59 +0000</pubDate>
      <link>https://forem.com/obanai/dpll-all-time-hit-sat-solver-4keb</link>
      <guid>https://forem.com/obanai/dpll-all-time-hit-sat-solver-4keb</guid>
      <description>&lt;h2&gt;
  
  
  Enter DPLL! - An Introduction
&lt;/h2&gt;

&lt;p&gt;Ever wondered how computers solve those tricky SAT problems? Meet the DPLL algorithm, a cornerstone in the world of logic puzzles. What does DPLL stand for? Its very creators &lt;strong&gt;D&lt;/strong&gt;avis, &lt;strong&gt;P&lt;/strong&gt;utnam, &lt;strong&gt;L&lt;/strong&gt;ogemann, and &lt;strong&gt;L&lt;/strong&gt;oveland! It's a classic in the field of computer science, simplifying complex problems by systematically exploring possible solutions.&lt;/p&gt;

&lt;h3&gt;
  
  
  What is DPLL??
&lt;/h3&gt;

&lt;p&gt;DPLL algorithm is designed to determine the satisfiability of logical formulas. It is essentially a "Trial and Error" method, but more sophisticated. The algorithm works by systematically exploring possible assignments and simplifying the formula through techniques like unit propagation and pure literal elimination. This process reduces the complexity of the problem, making it easier to find a solution or prove that no solution exists.&lt;/p&gt;

&lt;h3&gt;
  
  
  So, how does it work?
&lt;/h3&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;strong&gt;Unit Propagation:&lt;/strong&gt; Unit literals are assigned TRUE (Because if they are not, the clause and in turn the whole sentence would become FALSE). When a literal (a unit) is assigned, the effects fall upon the clauses containing either the literal or its negated version. There are two points to be noted:&lt;/li&gt;
&lt;/ul&gt;

&lt;p&gt;&lt;strong&gt;1. clause contains literal&lt;/strong&gt;&lt;/p&gt;

&lt;blockquote&gt;
&lt;p&gt;A clause is true if any literal is true, even if the other literals do not yet have truth values&lt;/p&gt;
&lt;/blockquote&gt;

&lt;p&gt;Hence, the clause can be removed from the list of clauses that make the problem (a sentence).&lt;/p&gt;

&lt;blockquote&gt;
&lt;p&gt;For example, the sentence (A ∨ B ∨ C) is true if A is true, regardless of the values of B and C. &lt;/p&gt;
&lt;/blockquote&gt;

&lt;p&gt;&lt;strong&gt;2. clause contains -literal&lt;/strong&gt;&lt;/p&gt;

&lt;blockquote&gt;
&lt;p&gt;A sentence is false if any clause is false, which occurs when each of its literals is false. This can occur long before the model is complete.&lt;/p&gt;
&lt;/blockquote&gt;

&lt;p&gt;So, the literals that become FALSE because of the new assignment can be removed from corresponding clauses.&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;&lt;p&gt;&lt;strong&gt;Pure Literal Elimination:&lt;/strong&gt; Next, it is about literals that only appear in one form (either always positive or always negative) also called "pure literals". These are assigned TRUE (For obvious reasons - &lt;em&gt;A literal that is never negated cannot be the cause of a failure when it is assigned&lt;/em&gt; and only aids in satisfying the clause and the sentence). &lt;/p&gt;&lt;/li&gt;
&lt;li&gt;&lt;p&gt;&lt;strong&gt;Splitting:&lt;/strong&gt; Finally, the remaining subproblems are tackled by choosing a variable and assigning it a value. If the assigned value leads to FAILURE, the alternate value is assigned after backtracking. To improve the algorithm further, a heuristic can be employed to choose the variable.&lt;/p&gt;&lt;/li&gt;
&lt;li&gt;&lt;p&gt;&lt;strong&gt;Success or Failure:&lt;/strong&gt; This is determined by examining the list of clauses. Because of unit propagation done after each assignment, clauses might get removed or shortened. &lt;br&gt;
No clauses in the list would mean that every clause was deemed TRUE and got removed from the list. So, the assignments done so far are returned, indicating success.&lt;br&gt;
An empty clause in the list suggests that every literal belonging to the clause was deemed FALSE and was removed from the clause. This means that the whole sentence is FALSE and FAILURE (None) is returned.&lt;/p&gt;&lt;/li&gt;
&lt;/ul&gt;

&lt;h4&gt;
  
  
  Pseudocode
&lt;/h4&gt;

&lt;blockquote&gt;
&lt;p&gt;Artificial Intelligence - A Modern Approach&lt;br&gt;
 (Third Edition) by Stuart J. Russell and Peter Norvig&lt;br&gt;
&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F6zp3fjdq3cod5euwsvay.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F6zp3fjdq3cod5euwsvay.png" alt="DPLL algorithm from Artificial Intelligence A Modern Approach (Figure 7.17)" width="800" height="561"&gt;&lt;/a&gt;&lt;/p&gt;
&lt;/blockquote&gt;

&lt;h4&gt;
  
  
  Implementation in Python
&lt;/h4&gt;



&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;# Functions
find_pure_literals(clauses) 
unit_propagation(clauses, unit) 
dpll(clauses, assignmemt)
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;





&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;def find_pure_literals(clauses):
    ''' Returns list of pure literals present in the provided list of clauses
    '''
    pure_literals = []
    for clause in clauses:
        for literal in clause:
            if literal not in pure_literals:
                pure_literals.append(literal) # adds all literals
    pure_literals = [x for x in pure_literals if -x not in pure_literals] # retains pure literals and filters out others
    return pure_literals

def unit_propagation(clauses, unit):
    ''' Eliminates the clauses that contain 'unit'
        Shortens the clauses that contain '-unit'
        Returns the list of clauses after the above modifications
    '''
    new_clauses = []
    for clause in clauses:
        if unit in clause:
            continue # removing true clauses (clauses with 'unit')
        new_clause = [x for x in clause if x != -unit] # shortening clauses with '-unit'
        new_clauses.append(new_clause)
    return new_clauses

def dpll(clauses, assignment):
    '''
    Returns the current assignment if no more clauses in the list
    None if empty clauses found (FAILED TO SATISFY)
    Assign pure literal TRUE, if any
    Assign unit literal TRUE, if any
    Choose a variable, assign FALSE, proceed for other literals: 
        If the result is FAILURE, remove the assignment 
        (BACKTRACK), assign TRUE and return the result (success 
        or failure, whatever!)
        Else return the result

    Note: The assigned pure literals, chosen variables are also propagated just like unit literals
    '''
    if not clauses:
        return assignment

    if any([len(clause)==0 for clause in clauses]):
        return None

    for clause in clauses:
        if len(clause)==1: # unit literal
            unit = clause.pop()
            clauses = unit_propagation(clauses, unit)
            assignment.append(unit)
            return dpll(clauses, assignment)

    pure_literals = find_pure_literals(clauses)
    if pure_literals:
        for unit in pure_literals:
            clauses = unit_propagation(clauses, unit)
            assignment.append(unit)
        return dpll(clauses, assignment)

    variable = clauses[0].pop() # chosen var - first literal in the first clause found in the list of clauses
    result = dpll(unit_propagation(clauses, -variable), assignment + [-variable]) # modify clauses, assignments and pass as params
    if result:
        return result
    return dpll(unit_propagation(clauses, variable), assignment + [variable])

&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;





&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;# main
cnf1 = [{1, -3, 4}, {-1, 2, 3}, {-2, -3, 4}, {1, -2, 3}, {-1, 2, -4}, {1, 2, -3}, {-1, -2, 3}, {1, -3, -4}, {-1, 3, 4}, {2, -3, 4}]
cnf2 = [{1, -2, 3}, {-1, 2, -3}, {1, 2, 3}, {-1, -2, -3}, {1, -3, 4}, {-1, 3, -4}, {2, -3, 4}, {-2, 3, -4}, {1, -2, 4}, {-1, 2, -4}]
cnf3 = [{-1, -2}, {-1, -3}, {-2, -3}, {1, 2}, {1, 3}, {2, 3}]
cnf_list = [cnf1, cnf2, cnf3]
for i,cnf in enumerate(cnf_list):
    result = dpll(cnf, [])
    if result:
      print(f"CNF {i+1} is satisfiable with the following assignment: \n{result}")
    else:
      print(f"CNF {i+1} is unsatisfiable\n[]")
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;h3&gt;
  
  
  Advantages (And also Limitations:)
&lt;/h3&gt;

&lt;p&gt;I don't intend to make this post any longer, so here's a brief overview regarding the pros and cons -&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;DPLL is highly efficient for many practical SAT problems (mainly due to its use of awesome techniques like unit propagation and pure literal elimination)&lt;/li&gt;
&lt;li&gt;Also, it is complete (it WILL find a solution, if one exists)&lt;/li&gt;
&lt;li&gt;&lt;p&gt;This algorithm forms the basis for many modern SAT solvers, which are used in various applications such as automated theorem proving, hardware verification, and artificial intelligence. (I just cited that from Wikipedia, but whatever; I know it's true)&lt;/p&gt;&lt;/li&gt;
&lt;li&gt;&lt;p&gt;In the worst case, the DPLL algorithm has an exponential time complexity. &lt;/p&gt;&lt;/li&gt;
&lt;li&gt;&lt;p&gt;It can consume a significant amount of memory, especially for large instances.&lt;/p&gt;&lt;/li&gt;
&lt;li&gt;&lt;p&gt;The performance can be heavily dependent on the heuristics used for variable selection and decision making. Poor heuristics can lead to inefficient searches and longer solution times.&lt;/p&gt;&lt;/li&gt;
&lt;/ul&gt;

&lt;h3&gt;
  
  
  Applications? (My, My...)
&lt;/h3&gt;

&lt;p&gt;By this time, you already know that this algorithm is designed for solving SAT problems. Therefore, it follows that any problem which can be modeled as SAT problem is indeed solvable using DPLL!&lt;/p&gt;

&lt;h3&gt;
  
  
  Conclusion
&lt;/h3&gt;

&lt;p&gt;You've been exposed to DPLL Algorithm to solve satisfiability problems. That's what the conclusion is! So, grab a coffee, roll up those sleeves, and go Plus Ultra on DPLL. NOW!&lt;/p&gt;

&lt;h3&gt;
  
  
  References
&lt;/h3&gt;

&lt;ul&gt;
&lt;li&gt;This post is meant to be an (assignment-level) introduction on DPLL. So, if you're really into it (like wanting to explore heuristics for choosing variable), become a search ninja on &lt;a href="https://www.google.com/" rel="noopener noreferrer"&gt;Google&lt;/a&gt; (Sure, you did your research, but hey, there's always more to discover!)&lt;/li&gt;
&lt;li&gt;Also, I'd recommend going through &lt;a href="https://github.com/yanshengjia/ml-road/blob/master/resources/Artificial%20Intelligence%20-%20A%20Modern%20Approach%20(3rd%20Edition).pdf" rel="noopener noreferrer"&gt;the textbook&lt;/a&gt; yourself once.&lt;/li&gt;
&lt;li&gt;I found these &lt;a href="https://www.cse.iitd.ac.in/~mausam/courses/col333/autumn2023/lectures/07-logic.pdf" rel="noopener noreferrer"&gt;slides&lt;/a&gt; really helpful and definitely recommend.&lt;/li&gt;
&lt;/ul&gt;

</description>
      <category>dpll</category>
      <category>algorithms</category>
      <category>ai</category>
      <category>tutorial</category>
    </item>
  </channel>
</rss>
