RL_in_SATLike_tuning_with_formula_invariant_model.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "private_outputs": true,
      "provenance": [],
      "collapsed_sections": [
        "o2Y7-lmq_kUq",
        "ZWGyXG1JWplr"
      ],
      "machine_shape": "hm",
      "authorship_tag": "ABX9TyPsPWJDEzCUjp1Ouzv0+oHW",
      "include_colab_link": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/github/ShaswataJash/Satlike/blob/main/RL_in_SATLike_tuning_with_formula_invariant_model.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "TFPg7TcNBx1B"
      },
      "source": [
        "# Download Weighted MaxSAT formulas"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "AbOTlCOfYVIm"
      },
      "source": [
        "!pip install gdown==3.6.4"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Tg2yNNTvY6hz"
      },
      "source": [
        "#downloading from my personal Google drive\n",
        "import gdown\n",
        "gdown.download('https://drive.google.com/uc?id=1MO34-v5jO2FlgDjyTjIpuMznOTkWYLY0', 'mse17-incomplete-weighted-benchmarks.zip', quiet=False) #418MB\n",
        "gdown.download('https://drive.google.com/uc?id=1kBVV3VFQXFPyVnu4jmtQRJz6SH5PBuFC', 'ms18_incomplete_wt.zip', quiet=False) #780MB\n"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "9xK2fjTrZS9W"
      },
      "source": [
        "import shutil\n",
        "import time\n",
        "\n",
        "#unpacking of this zip file may take more than 30 seconds\n",
        "start_time_of_unpacking = time.time()\n",
        "shutil.unpack_archive('mse17-incomplete-weighted-benchmarks.zip', '.')\n",
        "print(\"total time taken for unpacking = %s in seconds\" % (time.time() - start_time_of_unpacking))\n",
        "\n",
        "start_time_of_unpacking = time.time()\n",
        "shutil.unpack_archive('ms18_incomplete_wt.zip', '.')\n",
        "print(\"total time taken for unpacking = %s in seconds\" % (time.time() - start_time_of_unpacking))"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "3GgUQ0I4cLGs"
      },
      "source": [
        "import glob\n",
        "import pprint\n",
        "formula_files17 = glob.glob('/content/mse17-incomplete-weighted-benchmarks' + '/**/*.wcnf.gz', recursive=True)\n",
        "#pprint.pprint(formula_files17)\n",
        "print(\"total formula17 file count=%s\" % (len(formula_files17)))\n",
        "formula_files18 = glob.glob('/content/maxsat_instances/ms_evals/MS18/mse18-incomplete-weighted-benchmarks' + '/**/*.wcnf.gz', recursive=True)\n",
        "#pprint.pprint(formula_files18)\n",
        "print(\"total formula18 file count=%s\" % (len(formula_files18)))"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "o2Y7-lmq_kUq"
      },
      "source": [
        "# G++ version upgrade to G++8"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "vWTeoCxCvW-L"
      },
      "source": [
        "!sudo apt update\n",
        "!sudo apt-get install gcc-8 g++-8"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Txgmo1hL0W9s"
      },
      "source": [
        "!sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-8 80 --slave /usr/bin/g++ g++ /usr/bin/g++-8 \n",
        "!sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 70 --slave /usr/bin/g++ g++ /usr/bin/g++-7 "
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "KmcWdLwK1NUn"
      },
      "source": [
        "!sudo update-alternatives --install /usr/bin/x86_64-linux-gnu-gcc x86_64-linux-gnu-gcc /usr/bin/gcc-8 80 --slave /usr/bin/x86_64-linux-gnu-g++ x86_64-linux-gnu-g++ /usr/bin/g++-8\n",
        "!sudo update-alternatives --install /usr/bin/x86_64-linux-gnu-gcc x86_64-linux-gnu-gcc /usr/bin/gcc-7 70 --slave /usr/bin/x86_64-linux-gnu-g++ x86_64-linux-gnu-g++ /usr/bin/g++-7"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "ZBVs5vNC0vpr"
      },
      "source": [
        "!gcc --version\n",
        "!x86_64-linux-gnu-gcc --version"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "VyQ1k4gO_ulo"
      },
      "source": [
        "# Satlike Git code download"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "H7MwhXZziUnm"
      },
      "source": [
        "!rm -Rf Satlike\n",
        "!git clone https://github.com/ShaswataJash/Satlike.git\n",
        "%cd /content/Satlike/"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "ZWGyXG1JWplr"
      },
      "source": [
        "# Compiling Satlike executable with santize protection to find out memory corruption issues"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "2uPcFz4qI1Hh"
      },
      "source": [
        "#ensure libtcmalloc.so.4 is not preloaded. If that happens asan will not able to instrument malloc and free\n",
        "!echo $LD_PRELOAD\n",
        "%env LD_PRELOAD=\n",
        "!echo $LD_PRELOAD"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "SAYpIW39bwXG"
      },
      "source": [
        "!g++ -O2 -Wall -g -fstack-protector-strong -D_FORTIFY_SOURCE=2 pms.cpp -o pms.out -fsanitize=address -fsanitize=pointer-compare -fsanitize=pointer-subtract -fsanitize=undefined"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "wE370T1h_0aV"
      },
      "source": [
        "!ldd pms.out #verify that libasan is in order before any tcmalloc lib "
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "yN7o9BbLR1Uw"
      },
      "source": [
        "#refer: https://github.com/google/sanitizers/wiki/AddressSanitizerFlags#run-time-flags\n",
        "#refer: https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html\n",
        "%env ASAN_OPTIONS=verbosity=2:detect_invalid_pointer_pairs=2"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "wIaCMJAEDIj6"
      },
      "source": [
        "import os\n",
        "import re\n",
        "import gzip\n",
        "import shutil\n",
        "\n",
        "def decompress_formula(selected_formula_file):\n",
        "    work_dir = '/tmp'\n",
        "    filename = os.path.split(selected_formula_file)[-1]\n",
        "    filename = re.sub(r\"\\.gz$\", \"\", filename, flags=re.IGNORECASE)\n",
        "    decompressed_filename = os.path.join(work_dir, filename)\n",
        "    print(\"selected_formula_file = %s\" % (decompressed_filename))\n",
        "    with gzip.open(selected_formula_file, 'rb') as f_in: \n",
        "        with open(decompressed_filename, 'wb') as f_out:\n",
        "            shutil.copyfileobj(f_in, f_out)\n",
        "\n",
        "    return decompressed_filename\n"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "hwHLceYQFh82"
      },
      "source": [
        "#testing single instance of formula execution\n",
        "import random\n",
        "random_selected_formula_file = random.choice(formula_files)\n",
        "decompress_formula(random_selected_formula_file)\n",
        "!sudo ./pms.out \"/tmp/lisbon-wedding-lisbon-wedding-4-19.wcnf\" #using sudo because asan lib will able to instrument printf only in priviledged mode"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "LBvJDVspNi_W"
      },
      "source": [
        "#testing all instances of formula execuation\n",
        "import subprocess\n",
        "for f in formula_files:\n",
        "    decomp_f = decompress_formula(f)\n",
        "    print(subprocess.run(\"sudo ./pms.out %s\" % (decomp_f), shell=True, check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE))"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "vmtmwiidDj_t"
      },
      "source": [
        "# SWIG installation for python interface of C++ Satlike"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "tHGRJAJnn3_M"
      },
      "source": [
        "!wget http://prdownloads.sourceforge.net/swig/swig-4.0.2.tar.gz"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "jTAgbpVqxU98"
      },
      "source": [
        "!gunzip swig-4.0.2.tar.gz\n",
        "!tar -xvf swig-4.0.2.tar"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "axnr3a2l1lmn"
      },
      "source": [
        "%cd swig-4.0.2/\n",
        "!./configure\n",
        "!make\n",
        "!make install"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "BDOVypRl665X"
      },
      "source": [
        "%cd /content/Satlike/\n",
        "!swig -c++ -python satlikew.i\n",
        "!cat satlikew.i"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "f_VRCQ6eD8dO"
      },
      "source": [
        "%%writefile satlikew.cpp\n",
        "\n",
        "#include \"basis_pms.h\"\n",
        "#include \"pms.h\""
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "8NbJrGBL3173"
      },
      "source": [
        "%%writefile setup.py\n",
        "\n",
        "#!/usr/bin/env python\n",
        "\n",
        "\"\"\"\n",
        "setup.py file for satlikew\n",
        "\"\"\"\n",
        "\n",
        "from distutils.core import setup, Extension\n",
        "\n",
        "#https://stackoverflow.com/questions/1676384/how-to-pass-flag-to-gcc-in-python-setup-py-script\n",
        "satlikew_module = Extension('_satlikew',\n",
        "                           sources=['satlikew_wrap.cxx', 'satlikew.cpp'],\n",
        "                           #extra_compile_args=['-fsanitize=address -fsanitize=pointer-compare -fsanitize=pointer-subtract -fsanitize=leak -fsanitize=undefined']\n",
        "                           #extra_link_args=['-fsanitize=address -fsanitize=pointer-compare -fsanitize=pointer-subtract -fsanitize=leak -fsanitize=undefined']\n",
        "                           )\n",
        "\n",
        "setup (name = 'satlikew',\n",
        "       version = '0.1',\n",
        "       author      = \"Shaswata Jash\",\n",
        "       description = \"\"\"To interact with SatLike3.0 algorithm from python\"\"\",\n",
        "       ext_modules = [satlikew_module],\n",
        "       py_modules = [\"satlikew\"],\n",
        "       )"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Iq1075DU7z0v"
      },
      "source": [
        "#refer http://www.swig.org/Doc4.0/Python.html#Python_nn20\n",
        "!python setup.py build_ext --inplace"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "BFSKo7mzE-hG"
      },
      "source": [
        "!ls -l /content/Satlike/_satlikew.cpython-36m-x86_64-linux-gnu.so"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "aYOFgFM8Y39z"
      },
      "source": [
        "!ldd /content/Satlike/_satlikew.cpython-36m-x86_64-linux-gnu.so"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "eJXydw-UFd1s"
      },
      "source": [
        "import os\n",
        "import satlikew\n",
        "import time\n",
        "import shutil\n",
        "import re\n",
        "import gzip\n",
        "\n",
        "satlike = satlikew.Satlike()\n",
        "try:\n",
        "    gzipped_file_name = '/content/mse17-incomplete-weighted-benchmarks/correlation-clustering-Rounded_CorrelationClustering_Vowel_BINARY_N760_D0.200.wcnf.gz'\n",
        "    work_dir = '/tmp'\n",
        "    filename = os.path.split(gzipped_file_name)[-1]\n",
        "    filename = re.sub(r\"\\.gz$\", \"\", filename, flags=re.IGNORECASE)\n",
        "    decompressed_filename = os.path.join(work_dir, filename)\n",
        "\n",
        "    print(\"decompressed_filename = %s\" % (decompressed_filename))\n",
        "    #refer: https://stackoverflow.com/questions/55040442/how-to-register-gz-format-in-shutil-register-archive-format-to-use-same-format\n",
        "    with gzip.open(gzipped_file_name, 'rb') as f_in: \n",
        "        with open(decompressed_filename, 'wb') as f_out:\n",
        "            shutil.copyfileobj(f_in, f_out)\n",
        "\n",
        "    satlike.build_instance(decompressed_filename);\n",
        "    satlike.algo_init(1, todebug=False) #no-randomization (i.e. fixed seed value of one)\n",
        "    last_soft_unsat_weight = satlike.get_total_soft_weight()+1\n",
        "    start_time = time.time()\n",
        "    break_from_outer_loop = False\n",
        "    while break_from_outer_loop == False:\n",
        "        satlike.init_with_decimation_stepwise();\n",
        "        current_step = 1\n",
        "        while current_step < satlike.get_max_flips():\n",
        "            current_step += 1\n",
        "            satlike.local_search_stepwise(15, 1e-07, 300, 500, current_step, False)\n",
        "            if (satlike.get_hard_unsat_nb() == 0) and (satlike.get_opt_unsat_weight() < last_soft_unsat_weight):\n",
        "                print(\"opt_unsat_weight = %s time-taken in sec=%s\" % (satlike.get_opt_unsat_weight(), time.time() - start_time))\n",
        "                last_soft_unsat_weight = satlike.get_opt_unsat_weight()\n",
        "\n",
        "            if last_soft_unsat_weight == 0:\n",
        "                break_from_outer_loop = True\n",
        "                break\n",
        "            \n",
        "            if time.time() - start_time > 60:\n",
        "                break_from_outer_loop = True\n",
        "                break\n",
        "\n",
        "finally:\n",
        "    satlike.free_memory()\n"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "BZUbwVzvhHTV"
      },
      "source": [
        "# RAY(RLLib) CLUSTER SETUP"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "vlYoaCdvHkMt"
      },
      "source": [
        "!whoami\n",
        "!pwd\n",
        "!python -V\n",
        "!pip install ray[rllib]"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "HPjTMRQ7of1C"
      },
      "source": [
        "!pip install psutil #will be used by ray to print log_sys_usage\n",
        "!pip install gputil"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "3U0tiG6cv3DA"
      },
      "source": [
        "!ray stop\n",
        "!rm -Rf /tmp/ray\n",
        "!rm -Rf ~/ray_results\n",
        "!rm -Rf /tmp/decompressed_formula\n",
        "!mkdir /tmp/decompressed_formula\n",
        "#!ray start --help\n",
        "#Without explicit information about binding dashboard-host to 127.0.0.1, dashboard can't be connected in google-colab\n",
        "!ray start --head --port=6379 --object-manager-port=8076 --include-dashboard True --dashboard-host 127.0.0.1 --dashboard-port 8265 &"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "5i4USMy-Dyz_"
      },
      "source": [
        "from google.colab.output import eval_js\n",
        "print(eval_js(\"google.colab.kernel.proxyPort(8265)\"))"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "xyitxogWNFzM"
      },
      "source": [
        "%load_ext tensorboard\n",
        "%tensorboard --logdir ~/ray_results"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "n18Vg0cldc8h"
      },
      "source": [
        "## Reinforcement Learning - MaxSAT problem Environment"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "izh9FyfcdiUQ"
      },
      "source": [
        "import numpy as np\n",
        "import gym\n",
        "from gym import spaces\n",
        "from ray.tune.registry import register_env\n",
        "\n",
        "import satlikew\n",
        "import time\n",
        "import shutil\n",
        "import os\n",
        "import re\n",
        "import gzip\n",
        "import sys\n",
        "\n",
        "import random\n",
        "\n",
        "NUMBER_OF_ENV_PER_WORKER = 8\n",
        "\n",
        "# {x - (-1)} / {1 - (-1)} = {X - X_min} / {X_max - X_min}\n",
        "# X = 1/2 * (x + 1) * (X_max - X_min) + X_min\n",
        "def upscale(x, X_min, X_max):\n",
        "    assert x >= -1\n",
        "    assert x <= 1\n",
        "    assert X_min < X_max\n",
        "    return 0.5 * (x + 1) * (X_max - X_min) + X_min\n",
        "\n",
        "\n",
        "# {x - (-1)} / {1 - (-1)} = {X - X_min} / {X_max - X_min}\n",
        "# x =  ({X - X_min} / {X_max - X_min}) * 2 - 1 \n",
        "def downscale(X, X_min, X_max):\n",
        "    assert X >= X_min, \"X=%s >= X_min=%s\" % (X, X_min)\n",
        "    assert X <= X_max, \"X=%s <= X_max=%s\" % (X, X_max)\n",
        "    assert X_min < X_max, \"X_min=%s < X_max=%s\" % (X_min, X_max)\n",
        "    return ((X - X_min) / (X_max - X_min)) * 2 - 1\n",
        "\n",
        "class SATLikeHyperParamTuneEnvFormulaInvariant(gym.Env):\n",
        "\n",
        "    def __init__(self, env_config):\n",
        "        self.mode = env_config[\"mode\"]\n",
        "        self.verbose = env_config[\"verbose\"]\n",
        "        self.worker_index = env_config.worker_index\n",
        "        self.vector_index = env_config.vector_index\n",
        "        self.decompressed_filename = None\n",
        "        self.list_of_formula_files = env_config[\"list_of_formula_files\"]\n",
        "        assert len(self.list_of_formula_files) > 0\n",
        "        self.episode_time_in_sec = env_config[\"episode_time_in_sec\"]\n",
        "        assert self.episode_time_in_sec != None and self.episode_time_in_sec > 0\n",
        "        self.h_inc_eta_max = env_config[\"h_inc_eta_max\"]\n",
        "        assert self.h_inc_eta_max != None and self.h_inc_eta_max >= 1\n",
        "        self.formula_choice_random = env_config[\"formula_choice_random\"]\n",
        "        assert self.formula_choice_random != None and type(self.formula_choice_random)==bool\n",
        "        self.horizon_steps = env_config[\"episode_horizon\"]\n",
        "\n",
        "        self.sat_like = None\n",
        "        self.current_tries = -1\n",
        "        self.current_step = -1\n",
        "        self.algorithm_state = 0\n",
        "        self.last_soft_unsat_weight = -1\n",
        "        self.start_time = -1\n",
        "\n",
        "        self.number_of_rl_timestep = 0\n",
        "        self.total_reward = 0\n",
        "\n",
        "        #1st dimension for t, 2nd dimension for sp, 3rd dimension for h_inc, 4th dimension for eta\n",
        "        self.action_space = spaces.Box(low=-1.0, high=1.0, shape=(4,), dtype=np.float32) #for normalization, values should be in between [-1,1]\n",
        "\n",
        "        #(a) suppose one of the feature can be fraction of hard-clauses unsatisfied with respect to the total number of hard-clauses present in the formula for the current assignment of SATLike iteration. We should emphasize here on ‘fraction’ as this will essentially convert this feature as formula-invariant as it will normalize the value with respect to total of number of hard-clauses present in the formula.\n",
        "        #(b) Similarly, another formula-invariant feature can be ‘fraction’ of sum of satisfied soft-clause weights with respect to total sum of all soft-clause weights\n",
        "                \n",
        "        #for normalization, values should be in between [-1,1]\n",
        "        self.observation_space = spaces.Box(low=-1.0, high=1.0, shape=(2,), dtype=np.float32)\n",
        "\n",
        "    def __getObservationAndReward(self, r, sp, h_inc, eta):\n",
        "        assert self.algorithm_state == 1 or self.algorithm_state == 2\n",
        "\n",
        "        if self.verbose > 2: print(\"[W:%s, E:%s] r=%s sp=%s h_inc=%s eta=%s\" % (self.worker_index, self.vector_index, r, sp, h_inc, eta))\n",
        "\n",
        "        if self.algorithm_state == 1:\n",
        "            self.current_tries += 1\n",
        "            self.current_step = 0\n",
        "            self.sat_like.init_with_decimation_stepwise()\n",
        "            self.algorithm_state = 2\n",
        "        \n",
        "        if self.current_step < self.sat_like.get_max_flips():\n",
        "            self.current_step += 1\n",
        "            self.sat_like.local_search_stepwise(r, sp, h_inc, eta, self.current_step, False)\n",
        "                        \n",
        "            if (self.sat_like.get_hard_unsat_nb() == 0) and (self.sat_like.get_opt_unsat_weight() < self.last_soft_unsat_weight):\n",
        "                if self.verbose > 1: print(\"[W:%s, E:%s] rl-step=%s try=%s step=%s opt_unsat_weight = %s time-taken in sec=%s\" \n",
        "                                           % (self.worker_index, self.vector_index, self.number_of_rl_timestep, self.current_tries, self.current_step, \n",
        "                                              self.sat_like.get_opt_unsat_weight(), time.time() - self.start_time))\n",
        "                self.last_soft_unsat_weight = self.sat_like.get_opt_unsat_weight()\n",
        "            else:\n",
        "                if self.verbose > 2: print(\"[W:%s, E:%s] rl-step=%s try=%s step=%s hard_unsat_nb=%s soft_unsat_weight = %s\" \n",
        "                                           % (self.worker_index, self.vector_index, self.number_of_rl_timestep, self.current_tries, self.current_step, \n",
        "                                              self.sat_like.get_hard_unsat_nb(), self.sat_like.get_soft_unsat_weight()))\n",
        "\n",
        "            if 0 == self.last_soft_unsat_weight:\n",
        "                self.algorithm_state = 1\n",
        "\n",
        "        else:\n",
        "            self.algorithm_state = 1\n",
        "\n",
        "        assert self.sat_like.get_hard_unsat_nb() >= 0\n",
        "        obs1 = 0 if self.sat_like.get_hard_unsat_nb() == 0 else (self.sat_like.get_hard_unsat_nb() / self.sat_like.get_num_hclauses())\n",
        "\n",
        "        assert self.sat_like.get_soft_unsat_weight() >= 0 and (self.sat_like.get_total_soft_weight() >= self.sat_like.get_soft_unsat_weight()),  \\\n",
        "               \"%s total_soft_weight=%s soft_unsat_weight=%s\" % (self.decompressed_filename, self.sat_like.get_total_soft_weight() , self.sat_like.get_soft_unsat_weight())\n",
        "        obs2 = (self.sat_like.get_total_soft_weight() - self.sat_like.get_soft_unsat_weight()) / self.sat_like.get_total_soft_weight()\n",
        "\n",
        "        downscaled_obs1 = downscale(obs1, 0, 1.0) #rescale between [-1,1]\n",
        "        downscaled_obs2 = downscale(obs2, 0, 1.0) #rescale between [-1,1]\n",
        "        obs_arr = np.array([downscaled_obs1, downscaled_obs2])\n",
        "        assert obs_arr.shape == self.observation_space.shape\n",
        "        assert np.max(obs_arr) <= 1.0\n",
        "        assert np.min(obs_arr) >= -1.0\n",
        "\n",
        "        if self.sat_like.get_hard_unsat_nb() > 0:\n",
        "            reward = -(obs1 + 2)\n",
        "            assert -3 <= reward and reward <= -2\n",
        "        else:\n",
        "            #best positive reward can be +2 (positive reward has two parts - (a)unsat weight reduction (b)how fast reduction can be acheived)\n",
        "            reward =  obs2 +  (self.horizon_steps - self.number_of_rl_timestep)/self.horizon_steps #reward according to best solution in self.EPISODE_TIME_IN_SEC sec\n",
        "            assert 0 < reward and reward <= 2\n",
        "        return obs_arr, reward\n",
        "\n",
        "    def close(self):\n",
        "        if self.sat_like != None:\n",
        "            if self.verbose > 0 :\n",
        "                best_cost_desc = self.last_soft_unsat_weight if (self.last_soft_unsat_weight < self.sat_like.get_total_soft_weight()+1) else 'UNDETERMINED'\n",
        "                print(\"[W:%s, E:%s] rl_step_count = %s avg_reward=%s best_cost=%s \" % (self.worker_index, self.vector_index, self.number_of_rl_timestep, \n",
        "                      self.total_reward/self.number_of_rl_timestep, best_cost_desc))\n",
        "            \n",
        "            self.sat_like.free_memory()\n",
        "            self.sat_like = None\n",
        "            os.remove(self.decompressed_filename)\n",
        "            self.decompressed_filename = None\n",
        "        \n",
        "    def reset(self):\n",
        "\n",
        "        self.close()\n",
        "\n",
        "        self.number_of_rl_timestep = 0\n",
        "        self.total_reward = 0\n",
        "        random_selected_formula_file = random.choice(self.list_of_formula_files) if self.formula_choice_random \\\n",
        "                                           else self.list_of_formula_files[self.worker_index*NUMBER_OF_ENV_PER_WORKER + self.vector_index] \n",
        "        \n",
        "        work_dir = '/tmp/decompressed_formula'\n",
        "        filename = os.path.split(random_selected_formula_file)[-1]\n",
        "        filename = re.sub(r\"\\.gz$\", \"\", filename, flags=re.IGNORECASE)\n",
        "        woker_env_separated_filename = 'f_%s_%s_%s_%s' % (time.time(), self.worker_index,self.vector_index,filename)\n",
        "        self.decompressed_filename = os.path.join(work_dir, woker_env_separated_filename)\n",
        "\n",
        "        if self.verbose > 0: print(\"[W:%s, E:%s] selected_formula_file = %s\" % (self.worker_index, self.vector_index, self.decompressed_filename))\n",
        "        with gzip.open(random_selected_formula_file, 'rb') as f_in: \n",
        "            with open(self.decompressed_filename, 'wb') as f_out:\n",
        "                shutil.copyfileobj(f_in, f_out)\n",
        "\n",
        "        self.sat_like = satlikew.Satlike()\n",
        "        self.sat_like.build_instance(self.decompressed_filename)\n",
        "        self.sat_like.algo_init(1, todebug=False) #no-randomization (i.e. fixed seed value of one)\n",
        "        if self.verbose > 0: print(\"[W:%s, E:%s] formula summary: var_count=%s hard_clause_count=%s soft_clause_count=%s max_soft_weight=%s total_soft_clause_weight=%s\" \n",
        "              % (self.worker_index, self.vector_index, self.sat_like.get_num_vars(), self.sat_like.get_num_hclauses(), \n",
        "                 self.sat_like.get_num_sclauses(), self.sat_like.get_top_clause_weight(), self.sat_like.get_total_soft_weight()))\n",
        "        \n",
        "        assert self.sat_like.get_num_vars() > 0\n",
        "        assert self.sat_like.get_num_hclauses() >= 0 #in some formula, there can be only soft clauses\n",
        "        assert self.sat_like.get_num_sclauses() > 0\n",
        "        assert self.sat_like.get_total_soft_weight() > 0\n",
        "        assert self.sat_like.get_top_clause_weight() > 0\n",
        "        \n",
        "        self.current_tries = 0\n",
        "        self.current_step = -1\n",
        "        self.algorithm_state = 1\n",
        "        self.last_soft_unsat_weight = self.sat_like.get_total_soft_weight()+1\n",
        "        self.start_time = time.time()\n",
        "\n",
        "        obs, reward =  self.__getObservationAndReward(self.sat_like.get_hd_count_threshold(), self.sat_like.get_smooth_probability(),\n",
        "                                                      self.sat_like.get_h_inc(), self.sat_like.get_softclause_weight_threshold())\n",
        "        return obs\n",
        "\n",
        "    def step(self, action):\n",
        "        assert action.shape == self.action_space.shape, str(action)\n",
        "        assert np.max(action) <= 1.0, str(action)\n",
        "        assert np.min(action) >= -1.0,  str(action)\n",
        "        scaled_t = int(upscale(action[0], 1, self.sat_like.get_num_vars()))\n",
        "        scaled_sp = upscale(action[1], 0, 1)\n",
        "        #to_swt_to_num_sc_ratio = max(2, self.sat_like.get_top_clause_weight()/self.sat_like.get_num_sclauses()) #note: min of h_inc = 1, thus max can be 2 or higher\n",
        "        scaled_h_inc = int(upscale(action[2], 1, self.h_inc_eta_max)) #TODO: what should be the upper-bound\n",
        "        scaled_eta = int(upscale(action[3], 1, self.h_inc_eta_max)) #TODO: what should be the upper-bound\n",
        "\n",
        "        self.number_of_rl_timestep += 1\n",
        "        \n",
        "        obs , reward = self.__getObservationAndReward(scaled_t,scaled_sp,scaled_h_inc,scaled_eta)\n",
        "        self.total_reward += reward\n",
        "        done = True if (self.last_soft_unsat_weight == 0) or ((time.time() - self.start_time) > self.episode_time_in_sec) else False\n",
        "        info = {}\n",
        "        return obs, reward, done, info\n",
        "\n",
        "register_env(\"satlike_env\", lambda env_config: SATLikeHyperParamTuneEnvFormulaInvariant(env_config))"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "VP5y32kxi0zT"
      },
      "source": [
        "## PPO general configuration setup"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "2tvjgayyiLQz"
      },
      "source": [
        "import ray\n",
        "from ray import tune\n",
        "import ray.rllib.agents.ppo as ppo\n",
        "from ray.tune.logger import pretty_print\n",
        "import pprint\n",
        "import copy\n",
        "import random\n",
        "\n",
        "config = copy.deepcopy(ppo.DEFAULT_CONFIG)\n",
        "import tensorflow as tf\n",
        "device_name = tf.test.gpu_device_name()\n",
        "print('Found GPU at: {}'.format(device_name))\n",
        "gpu_count = 0\n",
        "if device_name == '/device:GPU:0':\n",
        "    gpu_count = 1\n",
        "config[\"num_gpus\"] = gpu_count \n",
        "config[\"num_cpus_for_driver\"] = 0.25\n",
        "config[\"num_cpus_per_worker\"] = 0.5\n",
        "#harcoding to 4, so that for each RL experiment constant 2 CPU worth worker-resource exhausted (config[\"num_cpus_per_worker\"] = 0.5). \n",
        "#This ensures multiple tune-trails can run in parallel according to total cpu availiable in the cluster\n",
        "config[\"num_workers\"] = 4  \n",
        "config[\"num_envs_per_worker\"] = NUMBER_OF_ENV_PER_WORKER\n",
        "config[\"rollout_fragment_length\"] = 64\n",
        "config[\"train_batch_size\"] = config[\"num_workers\"] * config[\"num_envs_per_worker\"] * config[\"rollout_fragment_length\"]\n",
        "config[\"sgd_minibatch_size\"] = min(config[\"sgd_minibatch_size\"],config[\"train_batch_size\"])\n",
        "config[\"horizon\"] = config[\"rollout_fragment_length\"] * 2000 #so that it is always proper multiple of config[\"rollout_fragment_length\"]\n",
        "config[\"preprocessor_pref\"] = None\n",
        "#config[\"framework\"] = 'torch'\n",
        "config[\"clip_rewards\"] = False #as we don't want reward to be cliped in between Tuple[value1, value2]: Clip at value1 and value2.\n",
        "config[\"vf_clip_param\"] = abs(-3 * config[\"horizon\"]) #dividing with max possible value of reward\n",
        "config[\"clip_actions\"] = True #without that we are getting action beyond -1 and 1\n",
        "config[\"lr\"] = 0.000001\n",
        "config[\"ignore_worker_failures\"] = True\n",
        "\n",
        "training_env_config = {\n",
        "    \"mode\": 'training',\n",
        "    \"episode_horizon\": config[\"horizon\"],\n",
        "    \"episode_time_in_sec\": 300, \n",
        "    \"h_inc_eta_max\": 10000, #POTENTIAL HYPER_PARAM TUNE CANDIDATE\n",
        "    \"list_of_formula_files\": formula_files17,\n",
        "    \"formula_choice_random\": True,\n",
        "    \"verbose\": 0\n",
        "}\n",
        "\n",
        "eval_env_config = {\n",
        "    \"mode\": 'eval', \n",
        "    \"episode_horizon\": config[\"horizon\"],\n",
        "    \"episode_time_in_sec\": 3600, #intentionally keeping it high so that validation episodes are predominently terminated using horizon condition (it will improve predictibility)\n",
        "    \"h_inc_eta_max\": training_env_config[\"h_inc_eta_max\"], \n",
        "    \"list_of_formula_files\": random.sample(formula_files18, 2 * NUMBER_OF_ENV_PER_WORKER),\n",
        "    \"formula_choice_random\": False,\n",
        "    \"verbose\": 1\n",
        "}\n",
        "config[\"env_config\"] = training_env_config\n",
        "\n",
        "'''\n",
        "config[\"evaluation_interval\"] = 15 #after every 15 training iteration\n",
        "#config['evaluation_num_workers'] =2\n",
        "config['evaluation_num_episodes'] = max(1,config['evaluation_num_workers']) * config[\"num_envs_per_worker\"]\n",
        "config['evaluation_config']['env_config'] = eval_env_config\n",
        "assert config['evaluation_num_episodes'] <= len(eval_env_config['list_of_formula_files'])\n",
        "'''\n",
        "pprint.pprint(config)\n"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "jXn8JPDtLi2Q"
      },
      "source": [
        "!ln -sf /opt/bin/nvidia-smi /usr/bin/nvidia-smi\n",
        "!nvidia-smi"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "2I7iK41-h0aU"
      },
      "source": [
        "## Tune experiment"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "IEbKaRPWiEyF"
      },
      "source": [
        "from ray.tune.schedulers import ASHAScheduler\n",
        "from ray.tune import CLIReporter, JupyterNotebookReporter\n",
        "from ray.tune.trial import Trial\n",
        "import time\n",
        "import shutil\n",
        "import os\n",
        "import math\n",
        "import copy \n",
        "\n",
        "ray.shutdown()\n",
        "ray.init(address='auto', ignore_reinit_error=True)\n",
        "print('''This cluster consists of {} nodes in total {} CPU resources in total '''.format(len(ray.nodes()), ray.cluster_resources()['CPU']))\n",
        "\n",
        "MAX_NUMBER_OF_EXPERIMENT = 50\n",
        "MAX_TRAINING_ITERATION_PER_TRIAL = 50\n",
        "CHOSEN_METRIC = 'episode_reward_mean'\n",
        "\n",
        "def tune_ppo_in_satlike(search_config):\n",
        "    start_time_of_training = time.time()\n",
        "    print('Started at %s for %s' % (start_time_of_training , search_config))\n",
        "    local_config = copy.deepcopy(config)\n",
        "    local_config[\"num_sgd_iter\"] = int(search_config[\"num_sgd_iter\"])\n",
        "    local_config[\"clip_param\"] = search_config[\"clip_param\"]\n",
        "    local_config[\"kl_coeff\"] = search_config[\"kl_coeff\"]\n",
        "    local_config[\"kl_target\"] = search_config[\"kl_target\"]\n",
        "    local_config[\"rollout_fragment_length\"] = search_config[\"rollout_fragment_length\"]\n",
        "    local_config[\"train_batch_size\"] = local_config[\"num_workers\"] * local_config[\"num_envs_per_worker\"] * local_config[\"rollout_fragment_length\"]\n",
        "    local_config[\"sgd_minibatch_size\"] = min(search_config[\"sgd_minibatch_size\"],local_config[\"train_batch_size\"])\n",
        "    local_config[\"gamma\"] = search_config[\"gamma\"]\n",
        "    local_config[\"lambda\"] = search_config[\"lambda\"]\n",
        "    local_config[\"vf_loss_coeff\"] = search_config[\"vf_loss_coeff\"]\n",
        "    local_config[\"entropy_coeff\"] = search_config[\"entropy_coeff\"]\n",
        "    #local_config[\"lr\"] = search_config[\"lr\"]\n",
        "    local_config[\"model\"][\"use_lstm\"] = search_config[\"use_lstm\"]\n",
        "    local_config[\"model\"][\"lstm_use_prev_action_reward\"] = search_config[\"lstm_use_prev_action_reward\"]\n",
        "    local_config[\"model\"][\"max_seq_len\"] = int(search_config[\"max_seq_len\"])\n",
        "    local_config[\"exploration_config\"][\"type\"] = search_config[\"exploration_strategy\"]\n",
        "    local_config[\"vf_share_layers\"] = search_config[\"vf_share_layers\"]\n",
        "    trainer = ppo.PPOTrainer(config=local_config, env=SATLikeHyperParamTuneEnvFormulaInvariant)\n",
        "    effective_iteration = 0\n",
        "    while effective_iteration < MAX_TRAINING_ITERATION_PER_TRIAL:\n",
        "        # Perform one iteration of training the policy with PPO\n",
        "        result = trainer.train()\n",
        "        #print(pretty_print(result))\n",
        "        if result['episodes_total'] > 0 and math.isnan(result[CHOSEN_METRIC]) == False:\n",
        "            tune.report(episode_reward_mean=result[CHOSEN_METRIC])\n",
        "            effective_iteration += 1\n",
        "    print('Ending at %s episode=%s mean-reward=%s' % (time.time(), result['episodes_total'], result[CHOSEN_METRIC]))\n",
        "    trainer.cleanup()\n",
        "    trainer = None\n",
        "    local_config = None\n",
        "\n",
        "class TimeStopper(Stopper):\n",
        "    def __init__(self, d):\n",
        "        self._start = time.time()\n",
        "        self._deadline = d\n",
        "\n",
        "    def __call__(self, trial_id, score):\n",
        "        return False\n",
        "\n",
        "    def stop_all(self):\n",
        "        return time.time() - self._start > self._deadline\n",
        "\n",
        "class TrialTerminationReporter(CLIReporter):\n",
        "    def __init__(self):\n",
        "        super(TrialTerminationReporter, self).__init__()\n",
        "        self.num_terminated = 0\n",
        "\n",
        "    def should_report(self, trials, done=False):\n",
        "        \"\"\"Reports only on trial termination events.\"\"\"\n",
        "        old_num_terminated = self.num_terminated\n",
        "        self.num_terminated = len([t for t in trials if t.status == Trial.TERMINATED])\n",
        "        return self.num_terminated > old_num_terminated\n",
        "\n",
        "analysis = tune.run(\n",
        "    tune_ppo_in_satlike,\n",
        "    name=\"PPO-IN-SatLike\",\n",
        "    resources_per_trial={\n",
        "        \"cpu\": 0.5,\n",
        "        \"extra_cpu\": 3.5, #refer: {config[\"num_cpus_per_worker\"] = 0.25 * config[\"num_workers\"] = 8} + {config[\"num_cpus_per_driver\"] = 0.25} \n",
        "    },\n",
        "    metric = CHOSEN_METRIC,\n",
        "    mode = 'max',\n",
        "    num_samples=MAX_NUMBER_OF_EXPERIMENT, #conduct MAX_NUMBER_OF_EXPERIMENT random experiment under ASHA (early stopping)\n",
        "    scheduler=ASHAScheduler(),\n",
        "    config={\n",
        "       #refer: https://medium.com/aureliantactics/ppo-hyperparameters-and-ranges-6fc2d29bccbe\n",
        "       \"rollout_fragment_length\": tune.choice([32, 64, 128, 256]),\n",
        "       \"sgd_minibatch_size\": tune.choice([64, 128, 256, 512, 1024]),\n",
        "       \"num_sgd_iter\": tune.uniform(3,30),\n",
        "       \"clip_param\" : tune.choice([0.1, 0.2, 0.3]),\n",
        "       \"kl_coeff\" : tune.uniform(0.3,1),\n",
        "       \"kl_target\" : tune.uniform(0.003,0.03),\n",
        "       \"gamma\": tune.uniform(0.8,0.9997),\n",
        "       \"lambda\": tune.uniform(0.9,1),\n",
        "       \"vf_loss_coeff\": tune.uniform(0.5, 1),\n",
        "       \"entropy_coeff\": tune.uniform(0, 0.01),\n",
        "       #\"lr\" : tune.uniform(0.003,5e-6),\n",
        "       \"use_lstm\": tune.choice([True,False]),\n",
        "       \"lstm_use_prev_action_reward\": tune.choice([True,False]),\n",
        "       \"max_seq_len\": tune.uniform(2,30),\n",
        "       #Only (Multi)Discrete action spaces supported for 'Curiosity' so far! \n",
        "       #EpsilonGreedy also shown issue related shape missmatch - need to investigate further \n",
        "       #For ParameterNoise, postprocess_trajectory() throws NotImplementedError\n",
        "       \"exploration_strategy\": tune.choice(['GaussianNoise', 'OrnsteinUhlenbeckNoise', 'StochasticSampling']),\n",
        "       \"vf_share_layers\": tune.choice([True,False])\n",
        "    },\n",
        "    checkpoint_at_end=True,\n",
        "    fail_fast=True,\n",
        "    progress_reporter = TrialTerminationReporter()\n",
        ")\n",
        "print(\"Best config: \", analysis.get_best_config(metric=CHOSEN_METRIC))\n",
        "ray.shutdown()"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "Hix0stDDhriT"
      },
      "source": [
        "## Single Reinforcement-learning (RL) experiment"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "fOqWrCwMQklS"
      },
      "source": [
        "from google.colab import drive\n",
        "drive.mount('/gdrive')"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "ssOwDSm7vgGE"
      },
      "source": [
        "import time\n",
        "import shutil\n",
        "import os\n",
        "import math\n",
        "\n",
        "ray.shutdown()\n",
        "ray.init(address='auto', ignore_reinit_error=True)\n",
        "print('''This cluster consists of {} nodes in total {} CPU resources in total '''.format(len(ray.nodes()), ray.cluster_resources()['CPU']))\n",
        "\n",
        "tuned_config = copy.deepcopy(config)\n",
        "tuned_config[\"num_sgd_iter\"] = 26\n",
        "tuned_config[\"clip_param\"] = 0.1\n",
        "tuned_config[\"kl_coeff\"] = 0.523515\n",
        "tuned_config[\"kl_target\"] = 0.0280057\n",
        "tuned_config[\"rollout_fragment_length\"] = 32\n",
        "tuned_config[\"train_batch_size\"] = tuned_config[\"num_workers\"] * tuned_config[\"num_envs_per_worker\"] * tuned_config[\"rollout_fragment_length\"]\n",
        "tuned_config[\"sgd_minibatch_size\"] = min(128,tuned_config[\"train_batch_size\"])\n",
        "tuned_config[\"gamma\"] = 0.9749\n",
        "tuned_config[\"lambda\"] = 0.922487\n",
        "tuned_config[\"vf_loss_coeff\"] = 0.550416\n",
        "tuned_config[\"entropy_coeff\"] = 0.00990254\n",
        "tuned_config[\"model\"][\"use_lstm\"] = True\n",
        "tuned_config[\"model\"][\"lstm_use_prev_action_reward\"] = False\n",
        "tuned_config[\"model\"][\"max_seq_len\"] = 27\n",
        "tuned_config[\"exploration_config\"][\"type\"] = 'OrnsteinUhlenbeckNoise'\n",
        "tuned_config[\"vf_share_layers\"] = True\n",
        "\n",
        "trainer = ppo.PPOTrainer(config=config, env=\"satlike_env\")\n",
        "#trainer.restore('/gdrive/My Drive/Colab Notebooks/capstone_proj1/best_checkpointed/best_checkpointed')#mean reward=-228.34249603086218\n",
        "\n",
        "class EvalEnvDictWrap(dict):\n",
        "    def __init__(self, env_conf, w_i, v_i):\n",
        "        for k,v in env_conf.items():\n",
        "            super().__setitem__(k, v)\n",
        "        self.worker_index = w_i\n",
        "        self.vector_index = v_i\n",
        "\n",
        "def compare_with_original_algo(formula_file, max_iteration):\n",
        "    satlike = satlikew.Satlike()\n",
        "    satlike.build_instance(formula_file)\n",
        "    satlike.algo_init(1, todebug=False) #no-randomization (i.e. fixed seed value of one)\n",
        "\n",
        "    last_soft_unsat_weight = satlike.get_total_soft_weight()+1\n",
        "    start_time = time.time()\n",
        "    break_from_outer_loop = False\n",
        "    iteration_count = 0\n",
        "    while break_from_outer_loop == False:\n",
        "        satlike.init_with_decimation_stepwise();\n",
        "        current_step = 1\n",
        "        while current_step < satlike.get_max_flips():\n",
        "            current_step += 1\n",
        "            satlike.local_search_stepwise(satlike.get_hd_count_threshold(), \n",
        "                                          satlike.get_smooth_probability(), \n",
        "                                          satlike.get_h_inc(), \n",
        "                                          satlike.get_softclause_weight_threshold(), \n",
        "                                          current_step, False)\n",
        "            if (satlike.get_hard_unsat_nb() == 0) and (satlike.get_opt_unsat_weight() < last_soft_unsat_weight):\n",
        "                print(\"opt_unsat_weight = %s time-taken in sec=%s\" % (satlike.get_opt_unsat_weight(), time.time() - start_time))\n",
        "                last_soft_unsat_weight = satlike.get_opt_unsat_weight()\n",
        "\n",
        "            if last_soft_unsat_weight == 0:\n",
        "                break_from_outer_loop = True\n",
        "                break\n",
        "            \n",
        "            iteration_count += 1\n",
        "            if iteration_count >= max_iteration:\n",
        "                break_from_outer_loop = True\n",
        "                break \n",
        "\n",
        "    satlike.free_memory()\n",
        "    return last_soft_unsat_weight\n",
        "\n",
        "def validate_on_unseen_data(my_trainer, max_iteration=30000, verbose=0):\n",
        "    try:\n",
        "        pol = my_trainer.get_policy()\n",
        "    except AttributeError:\n",
        "        pol = my_trainer.policy\n",
        "    \n",
        "    eval_episode_sat_soft_clause = 0\n",
        "    comparative_result_from_original_algo = 0\n",
        "    for i in range(len(eval_env_config[\"list_of_formula_files\"])):\n",
        "        eval_env = SATLikeHyperParamTuneEnvFormulaInvariant(\n",
        "                EvalEnvDictWrap(eval_env_config,i//NUMBER_OF_ENV_PER_WORKER,i%NUMBER_OF_ENV_PER_WORKER))\n",
        "\n",
        "        obs = eval_env.reset()\n",
        "        action_in = None\n",
        "        reward_in = None\n",
        "        state_in = pol.model.get_initial_state()\n",
        "        for _ in range(max_iteration):\n",
        "\n",
        "            #refer: https://github.com/ray-project/ray/blob/master/rllib/utils/test_utils.py (refer: check_compute_single_action())\n",
        "            action, state, _ = pol.compute_single_action(\n",
        "                    obs,\n",
        "                    state_in,\n",
        "                    prev_action=action_in,\n",
        "                    prev_reward=reward_in,\n",
        "                    clip_actions=tuned_config[\"clip_actions\"],\n",
        "                    explore=False)\n",
        "            action_in = action\n",
        "            state_in = state\n",
        "            obs, reward, done, info = eval_env.step(action)\n",
        "            reward_in = reward\n",
        "        \n",
        "        unsat_soft_clause = eval_env.last_soft_unsat_weight if (eval_env.last_soft_unsat_weight < eval_env.sat_like.get_total_soft_weight()+1) else -1\n",
        "        if unsat_soft_clause >= 0:\n",
        "            eval_episode_sat_soft_clause += (eval_env.sat_like.get_total_soft_weight() - unsat_soft_clause)\n",
        "        \n",
        "        last_soft_unsat_weight = compare_with_original_algo(eval_env.decompressed_filename,max_iteration)\n",
        "        unsat_soft_clause = last_soft_unsat_weight if (last_soft_unsat_weight < eval_env.sat_like.get_total_soft_weight()+1) else -1\n",
        "        if unsat_soft_clause >= 0:\n",
        "            comparative_result_from_original_algo += (eval_env.sat_like.get_total_soft_weight() - unsat_soft_clause)\n",
        "\n",
        "        eval_env.close()\n",
        "\n",
        "    if verbose > 0: print(\"******** eval_episode_sat_soft_clause = %s comparative_result_from_original_algo=%s ******\" \n",
        "                          % (eval_episode_sat_soft_clause, comparative_result_from_original_algo))\n",
        "    return eval_episode_sat_soft_clause, comparative_result_from_original_algo\n",
        "\n",
        "best_episode_reward_mean = None\n",
        "start_time_of_training = time.time()\n",
        "while time.time() - start_time_of_training < (120 * 60): #120 minutes \n",
        "    # Perform one iteration of training the policy with PPO\n",
        "    result = trainer.train()\n",
        "    validate_on_unseen_data(trainer, verbose=1)\n",
        "    #print(pretty_print(result))\n",
        "    \n",
        "    '''\n",
        "    if best_episode_reward_mean == None:\n",
        "        if result['episodes_total'] > 0 and math.isnan(result['episode_reward_mean']) == False:\n",
        "            best_episode_reward_mean = result['episode_reward_mean']\n",
        "            print(\"Initially: \", best_episode_reward_mean)\n",
        "            validate_on_unseen_data(trainer, verbose=1)\n",
        "    else: \n",
        "        if result['episode_reward_mean'] > best_episode_reward_mean:\n",
        "            best_episode_reward_mean = result['episode_reward_mean']\n",
        "            checkpoint = trainer.save()\n",
        "            print(best_episode_reward_mean, checkpoint)\n",
        "            validate_on_unseen_data(trainer, verbose=1)\n",
        "    '''\n",
        "            \n",
        "trainer.cleanup()\n",
        "ray.shutdown()"
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "jStkkl4FLUNV"
      },
      "source": [
        "!cp -Rf ~/ray_results '/gdrive/My Drive/Colab Notebooks/capstone_proj1/' "
      ],
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "ltqIMfT1x5qQ"
      },
      "source": [
        "!ray stop -v"
      ],
      "execution_count": null,
      "outputs": []
    }
  ]
}