sat_solver.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "name": "SAT Solver",
      "provenance": [],
      "collapsed_sections": [],
      "toc_visible": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "s-tmFiSo7xYI",
        "colab_type": "text"
      },
      "source": [
        "# SAT Solver \n",
        "## Assignment for CS508\n",
        "Name: Apurva N Saraogi\n",
        "\n",
        "Roll Number: 160101013\n",
        "\n",
        "### Task: \n",
        "- To design a SAT solver\n",
        "- Run benchmarks on it to show solver's performance"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "sqvBB3niG20s",
        "colab_type": "text"
      },
      "source": [
        "In this implementation a CDCL based SAT solver is prepared. On the first look DPLL based SAT solver looks promising as it mostly does intutive part like purification and unit propgation, it works good for random test cases, but for industrial purposes CDCL is used mainly due to these three reasons.\n",
        "- The variable is chosen randomly\n",
        "- Chronologically all branches are checked out\n",
        "- No learning from the current partial assignment, throws it all away.\n",
        "\n",
        "In the implementation we take care of these three things as follows, firstly for variable selection we use the below heuristics:\n",
        "- **Random**: The way it is already done.\n",
        "- **Ordered**: The first variable that is unassigned in the order 1,2,3... is chosen.\n",
        "- **Dynamic Largest Individual Sum (DLIS)**: The literal that occurs more frequently. By doing this we will be able to resolve maximum number of clauses at once.\n",
        "- **Largest Variable Sum (LVS)**: The variable that occurs more frequently is chosen. The count is computed once in the beginning and it is static, unlike DLIS does it everytime.\n",
        "- **Jeroslow–Wang (JW)**: Similar to DLIS but more weight is given to a literal in shorter clause compared to a longer clause weight is given by 2^-length.\n",
        "\n",
        "The second and this problems are handled as they are handled commonly in CDCL solvers by doing backjumps and adding clauses whenever conflict is reached. The algorithm is explained in detail in later sections."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "KAODLq-yv6jw",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Importing the libraries required\n",
        "import os\n",
        "import time\n",
        "import random\n",
        "import tabulate\n",
        "from orderedset import OrderedSet\n",
        "import operator\n",
        "import timeout_decorator\n",
        "from IPython.display import HTML, display, clear_output"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "aCaUscZybxdv",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Strategies available\n",
        "strategies = [\"RAN\",\"ORD\",\"LVS\",\"JW\",\"DLIS\"]\n",
        "\n",
        "# Weight to be used in branching strategies\n",
        "weight = 2\n",
        "\n",
        "# Precomputing weights for quicker access\n",
        "pow_weight = [2**(-x) for x in range(0,501)]\n",
        "\n",
        "# Timeout a testcase\n",
        "test_case_timeout = 20\n",
        "\n",
        "implications = 0\n",
        "branches = 0\n",
        "strategy = \"RANDOM\""
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "Dsx117AM4RtR",
        "colab_type": "text"
      },
      "source": [
        "Preprocessing of formula is done to reduce the size of the formula, we call this as regularizing a clause, in this we do three major things:\n",
        "- if p and not(p) are in the same clause, we remove the clause\n",
        "- duplicate literals from a clause are removed\n",
        "- it is then sorted and returned (Helps in searching, will be shown in next sections.)\n",
        "\n",
        "Removal of duplicate clause is done once a clause is regularized by putting them in a set."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "auMd-V_letyp",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Forumula Compression\n",
        "\n",
        "def regularizeClause(clause):\n",
        "  '''\n",
        "  Args:\n",
        "      clause ([int]): \n",
        "  Returns:\n",
        "      [int]: Regualarized clause\n",
        "  '''\n",
        "  # removes duplicate literals \n",
        "  unique_clause = { x: 1 for x in clause}\n",
        "  for x in unique_clause:\n",
        "    # checking if for p: not p exists\n",
        "    if -x in unique_clause.keys():\n",
        "      return frozenset([])\n",
        "  # sorting and returning list\n",
        "  return frozenset(clause)\n",
        "\n",
        "def compressCNF(clauses):\n",
        "  '''\n",
        "  Args:\n",
        "      clauses ([[int]]): \n",
        "  Returns:\n",
        "      [[int]]: Compressed Forumla\n",
        "  '''\n",
        "  # set of clauses and final list to be returned\n",
        "  set_of_clauses = set()\n",
        "  for clause in clauses:\n",
        "    # regularized clause\n",
        "    r_clause = regularizeClause(clause)\n",
        "    # If empty clause ignore it\n",
        "    if len(r_clause)==0:\n",
        "      continue\n",
        "    # if clause not already added then add it\n",
        "    set_of_clauses.add(r_clause)\n",
        "  return set_of_clauses"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "cig6YQmje79V",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Function for reading file\n",
        "\n",
        "def readFile(input_file):\n",
        "  '''\n",
        "  Args:\n",
        "      input_file (str): Location of the input file\n",
        "  Returns:\n",
        "      int: Number of Variables\n",
        "      [int]: clauses\n",
        "  '''\n",
        "  num_of_variables = 0\n",
        "  clauses = []\n",
        "  # Over here opening file, then parsing it and creating input\n",
        "  with open(input_file) as f:\n",
        "    for line in f: \n",
        "      if line[0]=='c' or line[0]=='p' or line[0]=='%' or line[0]=='0':\n",
        "        if line[0]=='p':\n",
        "          num_of_variables = int(line.split()[2])\n",
        "        continue\n",
        "      else:\n",
        "        clause = [int(tok) for tok in line.split()[:-1] if abs(int(tok))>=1 and abs(int(tok))<=num_of_variables]\n",
        "        if(len(clause)>0):\n",
        "          clauses.append(clause)\n",
        "  \n",
        "  return num_of_variables,clauses"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "G3NjfejGe0Ko",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Utility Functions\n",
        "\n",
        "def literal_value(literal):\n",
        "  '''\n",
        "  Returns the variable of the literal\n",
        "  Args:\n",
        "      literal (int):\n",
        "  Returns:\n",
        "      int: Variable\n",
        "  '''  \n",
        "  return abs(literal)\n",
        "\n",
        "def literal_sign(literal):\n",
        "  '''\n",
        "  Returns the type of literal.\n",
        "  Args:\n",
        "      literal (int):\n",
        "  Returns:\n",
        "      bool: Postive Literal -> 1 else 0\n",
        "  '''\n",
        "  if literal>0:\n",
        "    return 1\n",
        "  else:\n",
        "    return 0\n",
        "\n",
        "def evaluate_literal(literal):\n",
        "  '''\n",
        "  Args:\n",
        "      literal int:\n",
        "  Returns: \n",
        "      int: 1 if True 0 if False -1 if unassigned\n",
        "  ''' \n",
        "  if assignment[literal_value(literal)] == -1:\n",
        "    return -1\n",
        "  elif assignment[literal_value(literal)] == literal_sign(literal):\n",
        "    return 1\n",
        "  else:\n",
        "    return 0 \n",
        "\n",
        "\n",
        "def evaluate_clause(clause):\n",
        "  '''\n",
        "  Args:\n",
        "      clause{int}\n",
        "  Returns: \n",
        "      int: 1 if satisfied, 0 if unsatisfied, -x if x unassigned variables\n",
        "  ''' \n",
        "  undecided = 0\n",
        "  for literal in clause:\n",
        "    if evaluate_literal(literal) == 1:\n",
        "      return 1\n",
        "    elif evaluate_literal(literal) == -1:\n",
        "      undecided += 1\n",
        "  if undecided > 0:\n",
        "    return -undecided\n",
        "  else:\n",
        "    return 0\n",
        "\n",
        "def get_first_literal(clause):\n",
        "  '''\n",
        "  Args:\n",
        "      clause{int}\n",
        "  Returns: \n",
        "      int: First unassigned variable in the clause\n",
        "  ''' \n",
        "  for literal in clause:\n",
        "    # As unassigned literal is found return\n",
        "    if evaluate_literal(literal) == -1:\n",
        "      return literal\n",
        "  return None\n",
        "\n",
        "def assignment_over():\n",
        "  '''\n",
        "  Returns:\n",
        "      bool: Depicts if are all variables assigned\n",
        "  ''' \n",
        "  return min(assignment[1:])!=-1"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Gc2N9yl8j7Y8",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def initialize_solver():\n",
        "  # Initializing solver.\n",
        "  global current_level, branch_variable, propogation_history, branch_record, learnings, assignment,graph, LVS_count\n",
        "  current_level = 0 # Stores the current level at which solver is\n",
        "  branch_variable = set() # The variables on which branch is created\n",
        "  branch_record = {} # Tracks level wise record of branch variable\n",
        "  propogation_history = {} # Tracks all the implications done at each level\n",
        "  learnings = set() # Set of all the learned clauses\n",
        "  assignment = [-1]*(num_of_variables+1) # Assignment 1:True,0:False,-1:Empty\n",
        "  LVS_count = [] # Only used when strategy is LVS\n",
        "  graph = { variable: Node(variable) for variable in range(1,num_of_variables+1)}\n",
        "  # Creating nodes for the implication graph."
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "rhMzlENdVHvs",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Basic struct for the Node for making of implication graph\n",
        "class Node:\n",
        "  def __init__(self,variable):\n",
        "    self.variable = variable\n",
        "    self.value = -1\n",
        "    self.level = -1\n",
        "    self.parents = []\n",
        "    self.children = []\n",
        "    self.clause = None"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "IyqxwMPUH4d3",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# Branching Strategy as decsribed earlier\n",
        "\n",
        "def DLIS():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: Literal with maximum occurences.\n",
        "  ''' \n",
        "  # Calculate count of each variable\n",
        "  count = { y:0 for x in range(1,num_of_variables+1) if assignment[x]==-1 for y in [x,-x]}\n",
        "  for clause in clauses:\n",
        "    if evaluate_clause(clause) < 0:\n",
        "      for literal in clause:\n",
        "        if assignment[literal_value(literal)] == -1: \n",
        "          count[literal] += 1.0\n",
        "  # Choose the one which has maximum count \n",
        "  return max(count.items(), key = operator.itemgetter(1))[0]\n",
        "\n",
        "def LVS():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: Variable with maximum occurences in the initial formula.\n",
        "  ''' \n",
        "\n",
        "  global LVS_count\n",
        "  # Check if precomputed for the current problem\n",
        "  if len(LVS_count)==0:\n",
        "    # If not precompute it\n",
        "    LVS_count = { x:0 for x in range(1,num_of_variables+1) }\n",
        "    for clause in clauses:\n",
        "      for literal in clause:\n",
        "        LVS_count[literal_value(literal)]+=1\n",
        "  # Find maximum variable such that variable is unassigned.\n",
        "  max_var = 0\n",
        "  max_value = -1\n",
        "\n",
        "  for var in range(1,num_of_variables+1):\n",
        "    if assignment[var]==-1 and LVS_count[var]>max_value:\n",
        "      max_value = LVS_count[var]\n",
        "      max_var = var\n",
        "\n",
        "  return max_var*random.choice([1,-1])\n",
        "\n",
        "def JW():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: Literal with maximum weight.\n",
        "  ''' \n",
        "  # Similar to the above function, instead of adding one adding weight according\n",
        "  # to length of clause\n",
        "  count = { y:0 for x in range(1,num_of_variables+1) if assignment[x]==-1 for y in [x,-x]}\n",
        "  for clause in clauses:\n",
        "    if evaluate_clause(clause) < 0:\n",
        "      for literal in clause:\n",
        "        if assignment[literal_value(literal)] == -1: \n",
        "          count[literal] += pow_weight[min(500,len(clause))]\n",
        "  return max(count.items(), key = operator.itemgetter(1))[0]\n",
        "\n",
        "\n",
        "def ORD():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: First unassigned variable in order 1,2,3...\n",
        "  ''' \n",
        "  # Select first unassigned variable followed by random sign.\n",
        "  for x in range(1,num_of_variables+1):\n",
        "    if assignment[x] == -1:\n",
        "      return x*random.choice([1,-1])\n",
        "\n",
        "\n",
        "def RAN():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: Randomly pulls out an unassigned literal.\n",
        "  ''' \n",
        "  # Randomly select unassigned variable followed by its sign.\n",
        "  return random.choice([1,-1])*random.choice([x for x in range(1,num_of_variables+1) if assignment[x]==-1])\n",
        "\n",
        "def select_variable():\n",
        "  '''\n",
        "  Returns:\n",
        "      int: The selected literal according to the global variable strategy.\n",
        "  ''' \n",
        "  if strategy == \"ORD\":\n",
        "    return ORD()\n",
        "  elif strategy == \"LVS\":\n",
        "    return LVS()\n",
        "  elif strategy == \"RAN\":\n",
        "    return RAN()\n",
        "  elif strategy == \"DLIS\":\n",
        "    return DLIS()\n",
        "  elif strategy == \"JW\":\n",
        "    return JW()"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "QLf2tlvOYiz0",
        "colab_type": "text"
      },
      "source": [
        "### CDCL Algorithm\n",
        "```\n",
        "1. function CDCL\n",
        "2.     while (true) do\n",
        "3.         while (BCP() = “conflict”) do\n",
        "4.             backtrack-level := Analyze-Conflict();\n",
        "5.             if backtrack-level < 0 then return “Unsatisfiable”;\n",
        "6.             BackTrack(backtrack-level);\n",
        "7.         if ¬Decide() then return “Satisfiable”;\n",
        "```\n",
        "\n",
        "Ref: Daniel Kroening,Ofer Strichman: Decision Procedure"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "5uCG17OAesX8",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def CDCL():\n",
        "  '''\n",
        "  The main driver function of the CDCL algorithm\n",
        "  '''\n",
        "  global current_level, branch_variable, propogation_history, branch_record, learnings, branches\n",
        "  # While all variables are not assigned\n",
        "  while not assignment_over():\n",
        "    # First do unit propogation\n",
        "    conflict = unit_propogation()\n",
        "    if conflict is None:\n",
        "      # If there is no conflict then we need to see if all variables are not\n",
        "      # assigned if not we will branch by selecting a variable\n",
        "      if assignment_over():\n",
        "        break\n",
        "      # Branching is happening\n",
        "      branches = branches + 1\n",
        "      # Select a variable to assign\n",
        "      literal = select_variable()\n",
        "      # As we are branching we will have to increase the level\n",
        "      current_level += 1\n",
        "      # Assign True to literal\n",
        "      assignment[literal_value(literal)] = literal_sign(literal)\n",
        "      # Now  as this is a branching point we need to store where we are\n",
        "      # Branching off, will help later in conflict analyze\n",
        "      branch_variable.add(literal_value(literal))\n",
        "      branch_record[current_level] = literal_value(literal)\n",
        "      # Also we will keep a record of all the unit propositions\n",
        "      propogation_history[current_level] = OrderedSet()\n",
        "      # Update the implication graph, by adding this node\n",
        "      update_graph(literal_value(literal))\n",
        "    else:\n",
        "      # As a conflict has arised we call analyze conflict\n",
        "      # From this we get learning (a clause learned) and a level to jump back to\n",
        "      backtrack_level, learning = analyze_conflict(conflict)\n",
        "      # If level is negative forumla is unsat\n",
        "      if backtrack_level < 0:\n",
        "        return False\n",
        "      # Add clause to the global list\n",
        "      learnings.add(learning)\n",
        "      # backtrack and change current level\n",
        "      backtrack(backtrack_level)\n",
        "      current_level = backtrack_level\n",
        "  return True"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "60GTyIDmXthj",
        "colab_type": "text"
      },
      "source": [
        "\n",
        "### Analyze Conflict Algorithm\n",
        "```\n",
        "1. if current-decision-level = 0 then return -1;\n",
        "2. cl := current-conf licting-clause;\n",
        "3. while (¬Stop-criterion-met(cl)) do\n",
        "4.     lit := Last-assigned-literal(cl);\n",
        "5.     var := Variable-of-literal(lit);\n",
        "6.     ante := Antecedent(lit);\n",
        "7.     cl := Resolve(cl, ante, var);\n",
        "8. add-clause-to-database(cl);\n",
        "9. return clause-asserting-level(cl)\n",
        "```\n",
        "Ref: Daniel Kroening,Ofer Strichman: Decision Procedure\n"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "esRhyBa7chF2",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def analyze_conflict(conflict_clause):\n",
        "  '''\n",
        "  Args:\n",
        "      clause ({int}): \n",
        "  Returns:\n",
        "      int: Level we should jump back to\n",
        "      {int}: Learned Clause\n",
        "  '''\n",
        "  # If conflict is at level 0 no solution is possible\n",
        "  if current_level == 0:\n",
        "    return -1,None\n",
        "\n",
        "  # In current level the order in which variables were assigned\n",
        "  assignment_order = [branch_record[current_level]] + list(propogation_history[current_level])\n",
        "\n",
        "  currrent_conflicting_clause = conflict_clause\n",
        "\n",
        "  # While we don't reach the first UIP we don't stop, and it will always\n",
        "  # terminate as it is guranteed that first UIP will exist.\n",
        "  while not stop_criterion_met(currrent_conflicting_clause):\n",
        "    # Choose the most recent variable assignment done\n",
        "    literal = choose_literal(currrent_conflicting_clause,assignment_order)\n",
        "    # Find ante, the clause to which this literal belongs to\n",
        "    ante = antecedent(literal_value(literal))\n",
        "    # Resolution is done on ante and currently conflicting clause and update it\n",
        "    currrent_conflicting_clause = resolve(currrent_conflicting_clause,ante,literal_value(literal))\n",
        "  \n",
        "  # Return Backtrack Level and Learned Clause from the conflicting clause\n",
        "  return get_learnings_and_level(currrent_conflicting_clause)\n",
        "\n",
        "\n",
        "def stop_criterion_met(clause):\n",
        "  '''\n",
        "  UIP will be the point where at a single level only one assignment is present. \n",
        "  Args:\n",
        "      clause ({int}): \n",
        "  Returns:\n",
        "      bool: If UIP is found return True\n",
        "  '''\n",
        "  current_level_literal = set()\n",
        "  for literal in clause:\n",
        "    if graph[literal_value(literal)].level == current_level:\n",
        "      current_level_literal.add(literal)\n",
        "  \n",
        "  if len(current_level_literal) == 1:\n",
        "  # We are at the UIP as only literal is at current level\n",
        "    return True\n",
        "  else:\n",
        "    return False\n",
        "\n",
        "def choose_literal(clause,assignment_order):\n",
        "  '''\n",
        "  Args:\n",
        "      clause ({int}):\n",
        "      assignment_order ([int]): \n",
        "  Returns:\n",
        "      int: Chosen Literal\n",
        "  '''\n",
        "  # For literal in assignment order\n",
        "  for literal in assignment_order[::-1]:\n",
        "    if literal in clause or -literal in clause:\n",
        "      return literal\n",
        "\n",
        "\n",
        "def get_learnings_and_level(clause):\n",
        "  '''\n",
        "  Args:\n",
        "      clause ({int}): \n",
        "  Returns:\n",
        "      int: Backtrack Level\n",
        "      {int}: Clause\n",
        "  '''\n",
        "  literals = set()\n",
        "  backtrack_level = -1  \n",
        "  # Backtrack Level will be the maximum level found of the given clause that are\n",
        "  # not of current level, if none return current level - 1 \n",
        "  for literal in clause:\n",
        "    literals.add(literal)\n",
        "    if graph[literal_value(literal)].level != current_level:\n",
        "      backtrack_level = max(graph[literal_value(literal)].level,backtrack_level)\n",
        "\n",
        "  if backtrack_level == -1:\n",
        "    backtrack_level = current_level-1\n",
        "  return backtrack_level,frozenset(literals)\n",
        "\n",
        "def antecedent(variable):\n",
        "  '''\n",
        "  Return clause of the variable that is the ante\n",
        "  Args:\n",
        "      varaible (int): \n",
        "  Returns:\n",
        "      {int}: Ante\n",
        "  '''\n",
        "  return graph[variable].clause\n",
        "\n",
        "def resolve(clause,ante,literal):\n",
        "  '''\n",
        "  Args:\n",
        "      clause ([int]):\n",
        "      ante ([int]):\n",
        "      literal (int):             \n",
        "  Returns:\n",
        "      {int}: Clause\n",
        "  '''\n",
        "  # We are doing resolution in this step.\n",
        "  # (x+y')(y+z) => (x+z)\n",
        "  return (clause.union(ante)).difference([literal,-literal])"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "7GFhBidthenQ",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def unit_propogation():\n",
        "  '''\n",
        "  Returns:\n",
        "      {int}: conflict clause\n",
        "  '''  \n",
        "  global assignment,propogation_history, implications\n",
        "  # Keep doing until unit clauses are present\n",
        "  while True:\n",
        "    # Create a OrderedSet for all the unit clauses encountered.\n",
        "    # OrderedSet preserves insertion order and does quicker query \n",
        "    propogation = OrderedSet()\n",
        "    for clause in [x for x in clauses.union(learnings)]:\n",
        "      # Evaluate a clause, if satisfied continue, if unsatisfied report conflict\n",
        "      # clause else add it to the propogation list\n",
        "      result = evaluate_clause(clause)\n",
        "      if result == 1:\n",
        "        continue\n",
        "      elif result == 0:\n",
        "        return clause\n",
        "      elif result == -1:\n",
        "        propogation.add((get_first_literal(clause),clause))\n",
        "    # If no unit clause is encountered return None\n",
        "    if len(propogation) == 0:\n",
        "      return None\n",
        "    # Assign the variable and update the implication graph, add the assignment\n",
        "    # to history of current level\n",
        "    for literal,clause in propogation:\n",
        "      # As this assignment is implied\n",
        "      implications = implications + 1\n",
        "      assignment[literal_value(literal)] = literal_sign(literal)\n",
        "      update_graph(literal_value(literal),clause=clause)\n",
        "      if current_level != 0:\n",
        "        propogation_history[current_level].add(literal)\n",
        "\n",
        "\n",
        "def backtrack(backtrack_level):\n",
        "  '''\n",
        "  Args:\n",
        "      backtrack_level (int):\n",
        "  '''\n",
        "  global graph,assignment,propogation_history,branch_record,branch_variable\n",
        "  # Iterate over all the nodes of the graph\n",
        "  for variable, node in graph.items():\n",
        "    # Node has level greater than backtrack level delete it, else keep it but \n",
        "    # delete children which have a level greater.\n",
        "    if node.level <= backtrack_level:\n",
        "      pruned_children = []\n",
        "      for child in node.children:\n",
        "        if child.level <= backtrack_level:\n",
        "          pruned_children.append(child)\n",
        "      node.children = pruned_children\n",
        "    else:\n",
        "      del node\n",
        "      graph[variable] = Node(variable)\n",
        "      assignment[variable] = -1\n",
        "\n",
        "  # Remove bad literals from the list of branch variables\n",
        "  branch_variable = {variable for variable in range(1,num_of_variables+1) if (assignment[variable] != -1 and len(graph[variable].parents) == 0)}\n",
        "\n",
        "  # Remove the histories of larger levels.\n",
        "  levels = list(branch_record.keys())\n",
        "  for level in levels:\n",
        "    if level > backtrack_level:\n",
        "      del branch_record[level]\n",
        "      del propogation_history[level]\n",
        "\n",
        "\n",
        "def update_graph(variable, clause=None):\n",
        "  '''\n",
        "  Args:\n",
        "      variable (int):\n",
        "      clause ([int]):\n",
        "  '''\n",
        "  # Update the assignment and level of variable\n",
        "  global graph\n",
        "  graph[variable].level = current_level\n",
        "  graph[variable].value = assignment[variable]\n",
        "\n",
        "  # If over here by branching then there will be no clause, as it is selected by\n",
        "  # us but in case of propogation, there will be clause due to which it is here.\n",
        "\n",
        "  if clause is not None:\n",
        "    # Update parents of the clause. As it was a unit clause all others will have\n",
        "    # already being satisfied hence they will be parent to current node.\n",
        "    for l_literal in clause:\n",
        "      literal = literal_value(l_literal)\n",
        "      if variable != literal:\n",
        "        graph[literal].children.append(graph[variable])\n",
        "        graph[variable].parents.append(graph[literal])\n",
        "    graph[variable].clause = clause"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "GHJcUw_KffBg",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "@timeout_decorator.timeout(test_case_timeout)\n",
        "def solve():\n",
        "  '''\n",
        "  Returns:\n",
        "      [int]: Results\n",
        "  ''' \n",
        "  initialize_solver()\n",
        "  if CDCL():\n",
        "    return True,\"s SATISFIABLE\\n\" + \" \".join([\"v\"]+[ str(-x) if assignment[x] == 0 else str(x) for x in range(1,num_of_variables+1)] + [\"0\"])\n",
        "  else:\n",
        "    return False,\"s UNSATISFIABLE\"\n",
        "\n",
        "def terminal_solve(input_file,strategy=\"DLIS\"):\n",
        "  global num_of_variables,clauses\n",
        "  num_of_variables,clauses = readFile(input_file)\n",
        "  num_of_clauses = len(clauses)\n",
        "  clauses = compressCNF(clauses)\n",
        "  initialize_solver()\n",
        "  x = time.time()\n",
        "  output = CDCL()\n",
        "  y = time.time()\n",
        "  static = \"c File: \" + input_file + \"\\nc Clauses: \" + str(num_of_clauses) + \", Variables: \" + str(num_of_variables)+\"\\n\" + \"c Time: \" + str(y-x)+\"\\nc Branches: \" + str(branches) + \" Implications: \" + str(implications) + \"\\nc ================================= \\n\"\n",
        "  if output:\n",
        "    print(static +\"s SATISFIABLE\\n\" + \" \".join([\"v\"]+[ str(-x) if assignment[x] == 0 else str(x) for x in range(1,num_of_variables+1)] + [\"0\"]))\n",
        "  else:\n",
        "    print(static + \"s UNSATISFIABLE\")\n",
        "\n",
        "result = []\n",
        "\n",
        "def benchmark_solve(input_file):\n",
        "  # Read The File, regularize and compress the clauses.\n",
        "  global num_of_variables,clauses\n",
        "  x = time.time()\n",
        "  num_of_variables,clauses = readFile(input_file)\n",
        "  num_of_clauses = len(clauses)\n",
        "  clauses = compressCNF(clauses)\n",
        "  y = time.time()\n",
        "  global result\n",
        "  result = [input_file,num_of_variables,num_of_clauses,\"?\",y-x]\n",
        "  global strategy\n",
        "  for st in strategies:\n",
        "    strategy = st\n",
        "    print(strategy)\n",
        "    try:\n",
        "      x = time.time()\n",
        "      result[3],solution = solve()\n",
        "      y = time.time()\n",
        "      result += [y-x,branches,implications]\n",
        "      with open(\"solutions/\"+input_file.split(\"/\")[-1]+\"-\"+strategy+\".cnf\",\"w\") as f:\n",
        "        f.write(solution+\"\\nc File:\"+input_file+\"\\nc Branches:\"+str(branches)+\" Implications:\"+str(implications)+\" Time:\"+str(y-x))\n",
        "    except timeout_decorator.timeout_decorator.TimeoutError:\n",
        "      result += [str(test_case_timeout)+\"++\",branches,implications]\n",
        "  # Return Result Array.\n",
        "  return result\n"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "RtFEjQWTIQPM",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def pretty_print_table(table):\n",
        "  # Built for displaying tables on Jupyter\n",
        "  Header = \"<table><tr><th>Strategy</th><th colspan='4'></th>\" + \" \".join([\"<th colspan='3'>\"+strategy+\"</th>\" for strategy in strategies])+\"</tr>\"\n",
        "  Header += \"<tr><th>File</th><th>Variables</th><th>Clauses</th><th>SAT</th><th>Read Time</th>\" + \" \".join([\"<th>Time</th><th>Branches</th><th>Implications</th>\" for strategy in strategies])+ \"</tr>\"\n",
        "  style='<style>table{border:1px solid gray;}th{border:1px solid lightgray}td{border:1px solid lightgray}</style>'\n",
        "  display(HTML(style+Header + \" \".join(tabulate.tabulate(table, tablefmt='html').split()[1:])))"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "_bEDg3jhQjIf",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "results = []"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "964VO_-mfgmY",
        "colab_type": "code",
        "outputId": "2847a8cc-5de9-4190-f445-34af463e129a",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 450
        }
      },
      "source": [
        "FOLDER_NAME = \"test_cases\"\n",
        "strategies = [\"RAN\",\"ORD\",\"LVS\",\"JW\",\"DLIS\"]\n",
        "# For all the files in folder add the result of each file to results array\n",
        "for file in os.listdir(FOLDER_NAME):\n",
        "    results.append(benchmark_solve(FOLDER_NAME+\"/\"+file))\n",
        "    clear_output(wait=True)\n",
        "    pretty_print_table(results)"
      ],
      "execution_count": 214,
      "outputs": [
        {
          "output_type": "display_data",
          "data": {
            "text/html": [
              "<style>table{border:1px solid gray;}th{border:1px solid lightgray}td{border:1px solid lightgray}</style><table><tr><th>Strategy</th><th colspan='4'></th><th colspan='3'>RAN</th> <th colspan='3'>ORD</th> <th colspan='3'>LVS</th> <th colspan='3'>JW</th> <th colspan='3'>DLIS</th></tr><tr><th>File</th><th>Variables</th><th>Clauses</th><th>SAT</th><th>Read Time</th><th>Time</th><th>Branches</th><th>Implications</th> <th>Time</th><th>Branches</th><th>Implications</th> <th>Time</th><th>Branches</th><th>Implications</th> <th>Time</th><th>Branches</th><th>Implications</th> <th>Time</th><th>Branches</th><th>Implications</th></tr><tbody> <tr><td>test_cases/19x19queens.cnf</td><td style=\"text-align: right;\"> 361</td><td style=\"text-align: right;\">10735</td><td>True </td><td style=\"text-align: right;\">0.0375969 </td><td>0.7245011329650879 </td><td style=\"text-align: right;\"> 22</td><td style=\"text-align: right;\"> 408</td><td>13.811938762664795 </td><td style=\"text-align: right;\"> 210</td><td style=\"text-align: right;\"> 3863</td><td>20++ </td><td style=\"text-align: right;\">271</td><td style=\"text-align: right;\"> 5765</td><td>20++ </td><td style=\"text-align: right;\"> 473</td><td style=\"text-align: right;\"> 1964</td><td>20++ </td><td style=\"text-align: right;\"> 464</td><td style=\"text-align: right;\"> 1722</td></tr> <tr><td>test_cases/flat30-13.cnf </td><td style=\"text-align: right;\"> 90</td><td style=\"text-align: right;\"> 300</td><td>True </td><td style=\"text-align: right;\">0.00499797 </td><td>0.07964015007019043 </td><td style=\"text-align: right;\"> 15</td><td style=\"text-align: right;\"> 174</td><td>0.05555391311645508 </td><td style=\"text-align: right;\"> 14</td><td style=\"text-align: right;\"> 164</td><td>0.026264667510986328 </td><td style=\"text-align: right;\"> 11</td><td style=\"text-align: right;\"> 79</td><td>0.042482614517211914 </td><td style=\"text-align: right;\"> 24</td><td style=\"text-align: right;\"> 98</td><td>0.03744649887084961 </td><td style=\"text-align: right;\"> 24</td><td style=\"text-align: right;\"> 98</td></tr> <tr><td>test_cases/flat50-102.cnf </td><td style=\"text-align: right;\"> 150</td><td style=\"text-align: right;\"> 545</td><td>True </td><td style=\"text-align: right;\">0.00365877 </td><td>0.0988621711730957 </td><td style=\"text-align: right;\"> 18</td><td style=\"text-align: right;\"> 461</td><td>0.1361086368560791 </td><td style=\"text-align: right;\"> 54</td><td style=\"text-align: right;\"> 494</td><td>0.07672238349914551 </td><td style=\"text-align: right;\"> 18</td><td style=\"text-align: right;\"> 463</td><td>0.07051301002502441 </td><td style=\"text-align: right;\"> 23</td><td style=\"text-align: right;\"> 196</td><td>0.07769441604614258 </td><td style=\"text-align: right;\"> 23</td><td style=\"text-align: right;\"> 196</td></tr> <tr><td>test_cases/uf20-01000.cnf </td><td style=\"text-align: right;\"> 20</td><td style=\"text-align: right;\"> 91</td><td>True </td><td style=\"text-align: right;\">0.00158358 </td><td>0.03455471992492676 </td><td style=\"text-align: right;\"> 26</td><td style=\"text-align: right;\"> 218</td><td>0.023804187774658203 </td><td style=\"text-align: right;\"> 10</td><td style=\"text-align: right;\"> 124</td><td>0.010464191436767578 </td><td style=\"text-align: right;\"> 6</td><td style=\"text-align: right;\"> 55</td><td>0.013496637344360352 </td><td style=\"text-align: right;\"> 4</td><td style=\"text-align: right;\"> 29</td><td>0.008116960525512695 </td><td style=\"text-align: right;\"> 4</td><td style=\"text-align: right;\"> 29</td></tr> <tr><td>test_cases/uf50-0101.cnf </td><td style=\"text-align: right;\"> 50</td><td style=\"text-align: right;\"> 218</td><td>True </td><td style=\"text-align: right;\">0.00287247 </td><td>0.580223798751831 </td><td style=\"text-align: right;\"> 182</td><td style=\"text-align: right;\"> 2515</td><td>0.11874794960021973 </td><td style=\"text-align: right;\"> 49</td><td style=\"text-align: right;\"> 769</td><td>0.027406692504882812 </td><td style=\"text-align: right;\"> 17</td><td style=\"text-align: right;\"> 170</td><td>0.045702457427978516 </td><td style=\"text-align: right;\"> 24</td><td style=\"text-align: right;\"> 228</td><td>0.05267167091369629 </td><td style=\"text-align: right;\"> 24</td><td style=\"text-align: right;\"> 228</td></tr> <tr><td>test_cases/unsat.cnf </td><td style=\"text-align: right;\"> 2</td><td style=\"text-align: right;\"> 4</td><td>False</td><td style=\"text-align: right;\">0.00106788 </td><td>0.0002651214599609375</td><td style=\"text-align: right;\"> 1</td><td style=\"text-align: right;\"> 5</td><td>0.0002639293670654297</td><td style=\"text-align: right;\"> 1</td><td style=\"text-align: right;\"> 5</td><td>0.0003077983856201172</td><td style=\"text-align: right;\"> 1</td><td style=\"text-align: right;\"> 5</td><td>0.0002994537353515625</td><td style=\"text-align: right;\"> 1</td><td style=\"text-align: right;\"> 5</td><td>0.00031113624572753906</td><td style=\"text-align: right;\"> 1</td><td style=\"text-align: right;\"> 5</td></tr> <tr><td>test_cases/unsat1.cnf </td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 8</td><td>False</td><td style=\"text-align: right;\">0.000771999</td><td>0.0007119178771972656</td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 11</td><td>0.0006284713745117188</td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 11</td><td>0.000370025634765625 </td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 11</td><td>0.0009434223175048828</td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 11</td><td>0.0005941390991210938 </td><td style=\"text-align: right;\"> 3</td><td style=\"text-align: right;\"> 11</td></tr> <tr><td>test_cases/uuf50-0100.cnf </td><td style=\"text-align: right;\"> 50</td><td style=\"text-align: right;\"> 218</td><td>False</td><td style=\"text-align: right;\">0.00169492 </td><td>0.9695279598236084 </td><td style=\"text-align: right;\"> 242</td><td style=\"text-align: right;\"> 3920</td><td>0.2140347957611084 </td><td style=\"text-align: right;\"> 73</td><td style=\"text-align: right;\"> 1003</td><td>0.08237147331237793 </td><td style=\"text-align: right;\"> 26</td><td style=\"text-align: right;\"> 496</td><td>0.15317153930664062 </td><td style=\"text-align: right;\"> 47</td><td style=\"text-align: right;\"> 738</td><td>0.17574501037597656 </td><td style=\"text-align: right;\"> 47</td><td style=\"text-align: right;\"> 738</td></tr> <tr><td>test_cases/bmc-2.cnf </td><td style=\"text-align: right;\">2810</td><td style=\"text-align: right;\">11683</td><td>True </td><td style=\"text-align: right;\">0.0687082 </td><td>19.129653215408325 </td><td style=\"text-align: right;\"> 160</td><td style=\"text-align: right;\"> 4943</td><td>65.78856468200684 </td><td style=\"text-align: right;\"> 632</td><td style=\"text-align: right;\"> 12267</td><td>49.41663098335266 </td><td style=\"text-align: right;\">333</td><td style=\"text-align: right;\">14387</td><td>32.43623399734497 </td><td style=\"text-align: right;\"> 246</td><td style=\"text-align: right;\"> 7237</td><td>29.926966428756714 </td><td style=\"text-align: right;\"> 220</td><td style=\"text-align: right;\"> 7939</td></tr> <tr><td>test_cases/uf100-016.cnf </td><td style=\"text-align: right;\"> 100</td><td style=\"text-align: right;\"> 430</td><td>True </td><td style=\"text-align: right;\">0.00383091 </td><td>20++ </td><td style=\"text-align: right;\">1263</td><td style=\"text-align: right;\"> 26013</td><td>16.33281707763672 </td><td style=\"text-align: right;\">1248</td><td style=\"text-align: right;\"> 30633</td><td>1.648735761642456 </td><td style=\"text-align: right;\">202</td><td style=\"text-align: right;\"> 5578</td><td>3.3911619186401367 </td><td style=\"text-align: right;\"> 372</td><td style=\"text-align: right;\"> 7052</td><td>3.6570186614990234 </td><td style=\"text-align: right;\"> 372</td><td style=\"text-align: right;\"> 7052</td></tr> <tr><td>test_cases/uf125-04.cnf </td><td style=\"text-align: right;\"> 125</td><td style=\"text-align: right;\"> 538</td><td>True </td><td style=\"text-align: right;\">0.00412393 </td><td>13.79047155380249 </td><td style=\"text-align: right;\"> 952</td><td style=\"text-align: right;\"> 20115</td><td>20++ </td><td style=\"text-align: right;\">1118</td><td style=\"text-align: right;\"> 31940</td><td>20++ </td><td style=\"text-align: right;\">985</td><td style=\"text-align: right;\">30505</td><td>20++ </td><td style=\"text-align: right;\"> 997</td><td style=\"text-align: right;\"> 24494</td><td>20++ </td><td style=\"text-align: right;\">1131</td><td style=\"text-align: right;\"> 28430</td></tr> <tr><td>test_cases/uf150-02.cnf </td><td style=\"text-align: right;\"> 150</td><td style=\"text-align: right;\"> 645</td><td>True </td><td style=\"text-align: right;\">0.00486898 </td><td>20++ </td><td style=\"text-align: right;\">1040</td><td style=\"text-align: right;\"> 24398</td><td>20++ </td><td style=\"text-align: right;\"> 764</td><td style=\"text-align: right;\"> 22486</td><td>17.072136163711548 </td><td style=\"text-align: right;\">710</td><td style=\"text-align: right;\">25354</td><td>20++ </td><td style=\"text-align: right;\"> 924</td><td style=\"text-align: right;\"> 24552</td><td>20++ </td><td style=\"text-align: right;\"> 958</td><td style=\"text-align: right;\"> 25294</td></tr> <tr><td>test_cases/uf75-02.cnf </td><td style=\"text-align: right;\"> 75</td><td style=\"text-align: right;\"> 325</td><td>True </td><td style=\"text-align: right;\">0.00294042 </td><td>0.04744672775268555 </td><td style=\"text-align: right;\"> 22</td><td style=\"text-align: right;\"> 161</td><td>1.6036314964294434 </td><td style=\"text-align: right;\"> 254</td><td style=\"text-align: right;\"> 5623</td><td>1.289762258529663 </td><td style=\"text-align: right;\">175</td><td style=\"text-align: right;\"> 3687</td><td>0.09412932395935059 </td><td style=\"text-align: right;\"> 25</td><td style=\"text-align: right;\"> 115</td><td>0.14099764823913574 </td><td style=\"text-align: right;\"> 25</td><td style=\"text-align: right;\"> 115</td></tr> <tr><td>test_cases/uuf75-04.cnf </td><td style=\"text-align: right;\"> 75</td><td style=\"text-align: right;\"> 325</td><td>False</td><td style=\"text-align: right;\">0.00568295 </td><td>14.430735349655151 </td><td style=\"text-align: right;\">1303</td><td style=\"text-align: right;\"> 22320</td><td>2.0134904384613037 </td><td style=\"text-align: right;\"> 314</td><td style=\"text-align: right;\"> 6849</td><td>1.1951148509979248 </td><td style=\"text-align: right;\">179</td><td style=\"text-align: right;\"> 4213</td><td>1.4544122219085693 </td><td style=\"text-align: right;\"> 243</td><td style=\"text-align: right;\"> 4574</td><td>1.3848938941955566 </td><td style=\"text-align: right;\"> 243</td><td style=\"text-align: right;\"> 4574</td></tr> <tr><td>test_cases/uf100-0167.cnf </td><td style=\"text-align: right;\"> 100</td><td style=\"text-align: right;\"> 430</td><td>True </td><td style=\"text-align: right;\">0.0128238 </td><td>13.863039255142212 </td><td style=\"text-align: right;\">1133</td><td style=\"text-align: right;\"> 25042</td><td>50.43213486671448 </td><td style=\"text-align: right;\">2159</td><td style=\"text-align: right;\"> 65072</td><td>0.2616395950317383 </td><td style=\"text-align: right;\"> 45</td><td style=\"text-align: right;\"> 898</td><td>0.18059206008911133 </td><td style=\"text-align: right;\"> 52</td><td style=\"text-align: right;\"> 419</td><td>0.1850593090057373 </td><td style=\"text-align: right;\"> 52</td><td style=\"text-align: right;\"> 419</td></tr> <tr><td>test_cases/bmc-7.cnf </td><td style=\"text-align: right;\">8710</td><td style=\"text-align: right;\">39774</td><td>True </td><td style=\"text-align: right;\">0.312685 </td><td>300++ </td><td style=\"text-align: right;\">7519</td><td style=\"text-align: right;\">202699</td><td>300++ </td><td style=\"text-align: right;\">7946</td><td style=\"text-align: right;\">134561</td><td>280.04323983192444 </td><td style=\"text-align: right;\">651</td><td style=\"text-align: right;\">29087</td><td>300++ </td><td style=\"text-align: right;\">6987</td><td style=\"text-align: right;\">159982</td><td>300++ </td><td style=\"text-align: right;\">6427</td><td style=\"text-align: right;\">126504</td></tr> </tbody> </table>"
            ],
            "text/plain": [
              "<IPython.core.display.HTML object>"
            ]
          },
          "metadata": {
            "tags": []
          }
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "pgMtABtF_2Ab",
        "colab_type": "code",
        "outputId": "2d7b9188-a833-43f7-a041-f44f1ee3410b",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 165
        }
      },
      "source": [
        "strategy = \"RAN\"\n",
        "terminal_solve(\"test_cases/flat30-13.cnf\")"
      ],
      "execution_count": 215,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "c File: test_cases/flat30-13.cnf\n",
            "c Clauses: 300, Variables: 90\n",
            "c Time: 0.02236008644104004\n",
            "c Branches: 37 Implications: 472\n",
            "c ================================= \n",
            "s SATISFIABLE\n",
            "v -1 -2 3 4 -5 -6 -7 -8 9 -10 11 -12 -13 14 -15 -16 -17 18 -19 20 -21 22 -23 -24 -25 -26 27 -28 -29 30 -31 32 -33 34 -35 -36 -37 -38 39 40 -41 -42 -43 -44 45 46 -47 -48 -49 -50 51 52 -53 -54 55 -56 -57 -58 59 -60 -61 -62 63 -64 65 -66 -67 68 -69 -70 71 -72 -73 74 -75 -76 -77 78 79 -80 -81 -82 83 -84 -85 86 -87 88 -89 -90 0\n"
          ],
          "name": "stdout"
        }
      ]
    }
  ]
}