AlphaZeroSAT.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 5,
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3 (ipykernel)",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.9.5"
    },
    "colab": {
      "name": "AlphaZeroSAT.ipynb",
      "provenance": [],
      "machine_shape": "hm",
      "include_colab_link": true
    },
    "accelerator": "GPU"
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/github/dmeoli/NeuroSAT/blob/master/AlphaZeroSAT.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "md4JZ9dNr-cj",
        "outputId": "9520dcbe-c8c5-4433-8465-10113ff835b3"
      },
      "source": [
        "from google.colab import drive\n",
        "\n",
        "drive.mount('/content/gdrive')"
      ],
      "id": "md4JZ9dNr-cj",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Mounted at /content/gdrive\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "PSSjiEf1sjTf",
        "outputId": "22bc2abc-e990-48c2-e7a1-882d7b7afee1"
      },
      "source": [
        "%cd gdrive/My Drive"
      ],
      "id": "PSSjiEf1sjTf",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/gdrive/My Drive\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "wQDmH68WssAm",
        "outputId": "d27774a6-5e16-421b-ecbc-3f4eb7b4b597"
      },
      "source": [
        "import os\n",
        "\n",
        "if not os.path.isdir('neuroSAT'):\n",
        "  !git clone --recurse-submodules https://github.com/dmeoli/neuroSAT\n",
        "  %cd neuroSAT\n",
        "else:\n",
        "  %cd neuroSAT\n",
        "  !git pull"
      ],
      "id": "wQDmH68WssAm",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/gdrive/My Drive/neuro-sat\n",
            "Already up to date.\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "FDLLNcrEt_il",
        "outputId": "fbee06c8-95e0-4468-b78c-80fd26a0882f"
      },
      "source": [
        "!pip install -r requirements.txt"
      ],
      "id": "FDLLNcrEt_il",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Looking in links: https://pytorch-geometric.com/whl/torch-1.9.0+cu102.html\n",
            "Requirement already satisfied: gym in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 1)) (0.17.3)\n",
            "Requirement already satisfied: numpy in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 2)) (1.19.5)\n",
            "Requirement already satisfied: PyYAML in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 3)) (3.13)\n",
            "Requirement already satisfied: scipy in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 4)) (1.4.1)\n",
            "Collecting split-folders\n",
            "  Downloading split_folders-0.4.3-py3-none-any.whl (7.4 kB)\n",
            "Collecting tensorboardX\n",
            "  Downloading tensorboardX-2.4-py2.py3-none-any.whl (124 kB)\n",
            "\u001b[K     |████████████████████████████████| 124 kB 7.2 MB/s \n",
            "\u001b[?25hRequirement already satisfied: tensorflow in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 7)) (2.6.0)\n",
            "Requirement already satisfied: torch==1.9.0 in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 8)) (1.9.0+cu102)\n",
            "Collecting torch-geometric\n",
            "  Downloading torch_geometric-2.0.0.tar.gz (308 kB)\n",
            "\u001b[K     |████████████████████████████████| 308 kB 44.9 MB/s \n",
            "\u001b[?25hRequirement already satisfied: tqdm in /usr/local/lib/python3.7/dist-packages (from -r requirements.txt (line 10)) (4.62.0)\n",
            "Collecting torch-sparse\n",
            "  Downloading https://data.pyg.org/whl/torch-1.9.0%2Bcu102/torch_sparse-0.6.12-cp37-cp37m-linux_x86_64.whl (2.9 MB)\n",
            "\u001b[K     |████████████████████████████████| 2.9 MB 6.7 MB/s \n",
            "\u001b[?25hCollecting torch-scatter\n",
            "  Downloading https://data.pyg.org/whl/torch-1.9.0%2Bcu102/torch_scatter-2.0.8-cp37-cp37m-linux_x86_64.whl (8.0 MB)\n",
            "\u001b[K     |████████████████████████████████| 8.0 MB 20.2 MB/s \n",
            "\u001b[?25hRequirement already satisfied: typing-extensions in /usr/local/lib/python3.7/dist-packages (from torch==1.9.0->-r requirements.txt (line 8)) (3.7.4.3)\n",
            "Requirement already satisfied: pyglet<=1.5.0,>=1.4.0 in /usr/local/lib/python3.7/dist-packages (from gym->-r requirements.txt (line 1)) (1.5.0)\n",
            "Requirement already satisfied: cloudpickle<1.7.0,>=1.2.0 in /usr/local/lib/python3.7/dist-packages (from gym->-r requirements.txt (line 1)) (1.3.0)\n",
            "Requirement already satisfied: future in /usr/local/lib/python3.7/dist-packages (from pyglet<=1.5.0,>=1.4.0->gym->-r requirements.txt (line 1)) (0.16.0)\n",
            "Requirement already satisfied: protobuf>=3.8.0 in /usr/local/lib/python3.7/dist-packages (from tensorboardX->-r requirements.txt (line 6)) (3.17.3)\n",
            "Requirement already satisfied: six>=1.9 in /usr/local/lib/python3.7/dist-packages (from protobuf>=3.8.0->tensorboardX->-r requirements.txt (line 6)) (1.15.0)\n",
            "Requirement already satisfied: grpcio<2.0,>=1.37.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.39.0)\n",
            "Requirement already satisfied: keras-preprocessing~=1.1.2 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.1.2)\n",
            "Requirement already satisfied: termcolor~=1.1.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.1.0)\n",
            "Requirement already satisfied: flatbuffers~=1.12.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.12)\n",
            "Requirement already satisfied: wrapt~=1.12.1 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.12.1)\n",
            "Requirement already satisfied: gast==0.4.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (0.4.0)\n",
            "Requirement already satisfied: tensorboard~=2.6 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (2.6.0)\n",
            "Requirement already satisfied: tensorflow-estimator~=2.6 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (2.6.0)\n",
            "Requirement already satisfied: keras~=2.6 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (2.6.0)\n",
            "Requirement already satisfied: h5py~=3.1.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (3.1.0)\n",
            "Requirement already satisfied: clang~=5.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (5.0)\n",
            "Requirement already satisfied: google-pasta~=0.2 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (0.2.0)\n",
            "Requirement already satisfied: opt-einsum~=3.3.0 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (3.3.0)\n",
            "Requirement already satisfied: absl-py~=0.10 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (0.12.0)\n",
            "Requirement already satisfied: astunparse~=1.6.3 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (1.6.3)\n",
            "Requirement already satisfied: wheel~=0.35 in /usr/local/lib/python3.7/dist-packages (from tensorflow->-r requirements.txt (line 7)) (0.37.0)\n",
            "Requirement already satisfied: cached-property in /usr/local/lib/python3.7/dist-packages (from h5py~=3.1.0->tensorflow->-r requirements.txt (line 7)) (1.5.2)\n",
            "Requirement already satisfied: tensorboard-data-server<0.7.0,>=0.6.0 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (0.6.1)\n",
            "Requirement already satisfied: requests<3,>=2.21.0 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (2.23.0)\n",
            "Requirement already satisfied: google-auth-oauthlib<0.5,>=0.4.1 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (0.4.5)\n",
            "Requirement already satisfied: tensorboard-plugin-wit>=1.6.0 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (1.8.0)\n",
            "Requirement already satisfied: werkzeug>=0.11.15 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (1.0.1)\n",
            "Requirement already satisfied: markdown>=2.6.8 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (3.3.4)\n",
            "Requirement already satisfied: google-auth<2,>=1.6.3 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (1.34.0)\n",
            "Requirement already satisfied: setuptools>=41.0.0 in /usr/local/lib/python3.7/dist-packages (from tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (57.4.0)\n",
            "Requirement already satisfied: rsa<5,>=3.1.4 in /usr/local/lib/python3.7/dist-packages (from google-auth<2,>=1.6.3->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (4.7.2)\n",
            "Requirement already satisfied: cachetools<5.0,>=2.0.0 in /usr/local/lib/python3.7/dist-packages (from google-auth<2,>=1.6.3->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (4.2.2)\n",
            "Requirement already satisfied: pyasn1-modules>=0.2.1 in /usr/local/lib/python3.7/dist-packages (from google-auth<2,>=1.6.3->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (0.2.8)\n",
            "Requirement already satisfied: requests-oauthlib>=0.7.0 in /usr/local/lib/python3.7/dist-packages (from google-auth-oauthlib<0.5,>=0.4.1->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (1.3.0)\n",
            "Requirement already satisfied: importlib-metadata in /usr/local/lib/python3.7/dist-packages (from markdown>=2.6.8->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (4.6.4)\n",
            "Requirement already satisfied: pyasn1<0.5.0,>=0.4.6 in /usr/local/lib/python3.7/dist-packages (from pyasn1-modules>=0.2.1->google-auth<2,>=1.6.3->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (0.4.8)\n",
            "Requirement already satisfied: idna<3,>=2.5 in /usr/local/lib/python3.7/dist-packages (from requests<3,>=2.21.0->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (2.10)\n",
            "Requirement already satisfied: chardet<4,>=3.0.2 in /usr/local/lib/python3.7/dist-packages (from requests<3,>=2.21.0->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (3.0.4)\n",
            "Requirement already satisfied: certifi>=2017.4.17 in /usr/local/lib/python3.7/dist-packages (from requests<3,>=2.21.0->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (2021.5.30)\n",
            "Requirement already satisfied: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in /usr/local/lib/python3.7/dist-packages (from requests<3,>=2.21.0->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (1.24.3)\n",
            "Requirement already satisfied: oauthlib>=3.0.0 in /usr/local/lib/python3.7/dist-packages (from requests-oauthlib>=0.7.0->google-auth-oauthlib<0.5,>=0.4.1->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (3.1.1)\n",
            "Requirement already satisfied: networkx in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (2.6.2)\n",
            "Requirement already satisfied: scikit-learn in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (0.22.2.post1)\n",
            "Requirement already satisfied: pandas in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (1.1.5)\n",
            "Collecting rdflib\n",
            "  Downloading rdflib-6.0.0-py3-none-any.whl (376 kB)\n",
            "\u001b[K     |████████████████████████████████| 376 kB 56.7 MB/s \n",
            "\u001b[?25hRequirement already satisfied: googledrivedownloader in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (0.4)\n",
            "Requirement already satisfied: jinja2 in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (2.11.3)\n",
            "Requirement already satisfied: pyparsing in /usr/local/lib/python3.7/dist-packages (from torch-geometric->-r requirements.txt (line 9)) (2.4.7)\n",
            "Collecting yacs\n",
            "  Downloading yacs-0.1.8-py3-none-any.whl (14 kB)\n",
            "Requirement already satisfied: zipp>=0.5 in /usr/local/lib/python3.7/dist-packages (from importlib-metadata->markdown>=2.6.8->tensorboard~=2.6->tensorflow->-r requirements.txt (line 7)) (3.5.0)\n",
            "Requirement already satisfied: MarkupSafe>=0.23 in /usr/local/lib/python3.7/dist-packages (from jinja2->torch-geometric->-r requirements.txt (line 9)) (2.0.1)\n",
            "Requirement already satisfied: pytz>=2017.2 in /usr/local/lib/python3.7/dist-packages (from pandas->torch-geometric->-r requirements.txt (line 9)) (2018.9)\n",
            "Requirement already satisfied: python-dateutil>=2.7.3 in /usr/local/lib/python3.7/dist-packages (from pandas->torch-geometric->-r requirements.txt (line 9)) (2.8.2)\n",
            "Collecting isodate\n",
            "  Downloading isodate-0.6.0-py2.py3-none-any.whl (45 kB)\n",
            "\u001b[K     |████████████████████████████████| 45 kB 3.9 MB/s \n",
            "\u001b[?25hRequirement already satisfied: joblib>=0.11 in /usr/local/lib/python3.7/dist-packages (from scikit-learn->torch-geometric->-r requirements.txt (line 9)) (1.0.1)\n",
            "Building wheels for collected packages: torch-geometric\n",
            "  Building wheel for torch-geometric (setup.py) ... \u001b[?25l\u001b[?25hdone\n",
            "  Created wheel for torch-geometric: filename=torch_geometric-2.0.0-py3-none-any.whl size=513273 sha256=70e4b8ca32c9726fc3172adf84c627bebc2b4f34b439041b58dcec0cd149c84a\n",
            "  Stored in directory: /root/.cache/pip/wheels/b5/22/3f/10c97635d8d73e012582116b4e449d47fc64b7246cc71085fc\n",
            "Successfully built torch-geometric\n",
            "Installing collected packages: isodate, yacs, rdflib, torch-sparse, torch-scatter, torch-geometric, tensorboardX, split-folders\n",
            "Successfully installed isodate-0.6.0 rdflib-6.0.0 split-folders-0.4.3 tensorboardX-2.4 torch-geometric-2.0.0 torch-scatter-2.0.8 torch-sparse-0.6.12 yacs-0.1.8\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "HMMK1om7bzWs"
      },
      "source": [
        "datasets = {'uniform-random-3-sat': {'train': ['uf50-218', 'uuf50-218',\n",
        "                                               'uf100-430', 'uuf100-430'],\n",
        "                                     'val': ['uf50-218', 'uuf50-218',\n",
        "                                             'uf100-430', 'uuf100-430'],\n",
        "                                     'inner_test': ['uf50-218', 'uuf50-218',\n",
        "                                                    'uf100-430', 'uuf100-430'],\n",
        "                                     'test': ['uf250-1065', 'uuf250-1065']},\n",
        "            'graph-coloring': {'train': ['flat50-115'],\n",
        "                               'val': ['flat50-115'],\n",
        "                               'inner_test': ['flat50-115'],\n",
        "                               'test': ['flat30-60',\n",
        "                                        'flat75-180',\n",
        "                                        'flat100-239',\n",
        "                                        'flat125-301',\n",
        "                                        'flat150-360',\n",
        "                                        'flat175-417',\n",
        "                                        'flat200-479']}}"
      ],
      "id": "HMMK1om7bzWs",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "HaZyEN4cwNZ9",
        "outputId": "cb480c93-dd80-4284-c740-ce9046e1c09f"
      },
      "source": [
        "%cd AlphaZeroSAT"
      ],
      "id": "HaZyEN4cwNZ9",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/gdrive/My Drive/neuro-sat/AlphaZeroSAT\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "L31jaJGxwQ7J"
      },
      "source": [
        "## Build C++"
      ],
      "id": "L31jaJGxwQ7J"
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "fowxddSsejLg",
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "outputId": "7dbde897-f7be-4f18-bbd8-ac89290f64ec"
      },
      "source": [
        "%cd MCTSminisat\n",
        "!apt install libgsl-dev\n",
        "!sudo ln -s --force /usr/local/lib/python3.7/dist-packages/numpy/core/include/numpy /usr/include/numpy  # https://stackoverflow.com/a/44935933/5555994\n",
        "!make distclean && CXXFLAGS=-w make && make python-wrap PYTHON=python3.7\n",
        "!apt install swig\n",
        "!swig -fastdispatch -c++ -python minisat/gym/GymSolver.i\n",
        "%cd .."
      ],
      "id": "fowxddSsejLg",
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "/content/gdrive/My Drive/neuro-sat/AlphaZeroSAT/MCTSminisat\n",
            "Reading package lists... Done\n",
            "Building dependency tree       \n",
            "Reading state information... Done\n",
            "The following additional packages will be installed:\n",
            "  libgsl23 libgslcblas0\n",
            "Suggested packages:\n",
            "  gsl-ref-psdoc | gsl-doc-pdf | gsl-doc-info | gsl-ref-html\n",
            "The following NEW packages will be installed:\n",
            "  libgsl-dev libgsl23 libgslcblas0\n",
            "0 upgraded, 3 newly installed, 0 to remove and 40 not upgraded.\n",
            "Need to get 1,926 kB of archives.\n",
            "After this operation, 9,474 kB of additional disk space will be used.\n",
            "Get:1 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libgslcblas0 amd64 2.4+dfsg-6 [79.7 kB]\n",
            "Get:2 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libgsl23 amd64 2.4+dfsg-6 [823 kB]\n",
            "Get:3 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libgsl-dev amd64 2.4+dfsg-6 [1,023 kB]\n",
            "Fetched 1,926 kB in 11s (183 kB/s)\n",
            "Selecting previously unselected package libgslcblas0:amd64.\n",
            "(Reading database ... 148492 files and directories currently installed.)\n",
            "Preparing to unpack .../libgslcblas0_2.4+dfsg-6_amd64.deb ...\n",
            "Unpacking libgslcblas0:amd64 (2.4+dfsg-6) ...\n",
            "Selecting previously unselected package libgsl23:amd64.\n",
            "Preparing to unpack .../libgsl23_2.4+dfsg-6_amd64.deb ...\n",
            "Unpacking libgsl23:amd64 (2.4+dfsg-6) ...\n",
            "Selecting previously unselected package libgsl-dev.\n",
            "Preparing to unpack .../libgsl-dev_2.4+dfsg-6_amd64.deb ...\n",
            "Unpacking libgsl-dev (2.4+dfsg-6) ...\n",
            "Setting up libgslcblas0:amd64 (2.4+dfsg-6) ...\n",
            "Setting up libgsl23:amd64 (2.4+dfsg-6) ...\n",
            "Setting up libgsl-dev (2.4+dfsg-6) ...\n",
            "Processing triggers for man-db (2.8.3-2ubuntu0.1) ...\n",
            "Processing triggers for libc-bin (2.27-3ubuntu1.2) ...\n",
            "/sbin/ldconfig.real: /usr/local/lib/python3.7/dist-packages/ideep4py/lib/libmkldnn.so.0 is not a symbolic link\n",
            "\n",
            "rm -f   build/release/minisat/core/shadow.o  build/release/minisat/core/Solver.o  build/release/minisat/core/Const.o  build/release/minisat/core/Main.o  build/release/minisat/simp/SimpSolver.o  build/release/minisat/simp/Main.o  build/release/minisat/utils/System.o  build/release/minisat/utils/Options.o  build/release/minisat/gym/GymSolver.o   build/debug/minisat/core/shadow.o  build/debug/minisat/core/Solver.o  build/debug/minisat/core/Const.o  build/debug/minisat/core/Main.o  build/debug/minisat/simp/SimpSolver.o  build/debug/minisat/simp/Main.o  build/debug/minisat/utils/System.o  build/debug/minisat/utils/Options.o  build/debug/minisat/gym/GymSolver.o   build/profile/minisat/core/shadow.o  build/profile/minisat/core/Solver.o  build/profile/minisat/core/Const.o  build/profile/minisat/core/Main.o  build/profile/minisat/simp/SimpSolver.o  build/profile/minisat/simp/Main.o  build/profile/minisat/utils/System.o  build/profile/minisat/utils/Options.o  build/profile/minisat/gym/GymSolver.o   build/dynamic/minisat/core/shadow.o  build/dynamic/minisat/core/Solver.o  build/dynamic/minisat/core/Const.o  build/dynamic/minisat/core/Main.o  build/dynamic/minisat/simp/SimpSolver.o  build/dynamic/minisat/simp/Main.o  build/dynamic/minisat/utils/System.o  build/dynamic/minisat/utils/Options.o  build/dynamic/minisat/gym/GymSolver.o \\\n",
            "            build/release/minisat/core/shadow.d  build/release/minisat/core/Solver.d  build/release/minisat/core/Const.d  build/release/minisat/core/Main.d  build/release/minisat/simp/SimpSolver.d  build/release/minisat/simp/Main.d  build/release/minisat/utils/System.d  build/release/minisat/utils/Options.d  build/release/minisat/gym/GymSolver.d   build/debug/minisat/core/shadow.d  build/debug/minisat/core/Solver.d  build/debug/minisat/core/Const.d  build/debug/minisat/core/Main.d  build/debug/minisat/simp/SimpSolver.d  build/debug/minisat/simp/Main.d  build/debug/minisat/utils/System.d  build/debug/minisat/utils/Options.d  build/debug/minisat/gym/GymSolver.d   build/profile/minisat/core/shadow.d  build/profile/minisat/core/Solver.d  build/profile/minisat/core/Const.d  build/profile/minisat/core/Main.d  build/profile/minisat/simp/SimpSolver.d  build/profile/minisat/simp/Main.d  build/profile/minisat/utils/System.d  build/profile/minisat/utils/Options.d  build/profile/minisat/gym/GymSolver.d   build/dynamic/minisat/core/shadow.d  build/dynamic/minisat/core/Solver.d  build/dynamic/minisat/core/Const.d  build/dynamic/minisat/core/Main.d  build/dynamic/minisat/simp/SimpSolver.d  build/dynamic/minisat/simp/Main.d  build/dynamic/minisat/utils/System.d  build/dynamic/minisat/utils/Options.d  build/dynamic/minisat/gym/GymSolver.d \\\n",
            "   build/release/bin/minisat_core build/release/bin/minisat  build/debug/bin/minisat_core build/debug/bin/minisat  build/profile/bin/minisat_core build/profile/bin/minisat  build/dynamic/bin/minisat_core build/dynamic/bin/minisat \\\n",
            "   build/release/lib/libminisat.a  build/debug/lib/libminisat.a  build/profile/lib/libminisat.a \\\n",
            "  build/dynamic/lib/libminisat.so.2.1.0\\\n",
            "  build/dynamic/lib/libminisat.so.2\\\n",
            "  build/dynamic/lib/libminisat.so\n",
            "rm -f config.mk\n",
            "Compiling: build/release/minisat/simp/Main.o\n",
            "Compiling: build/release/minisat/core/shadow.o\n",
            "Compiling: build/release/minisat/core/Solver.o\n",
            "Compiling: build/release/minisat/core/Const.o\n",
            "Compiling: build/release/minisat/simp/SimpSolver.o\n",
            "Compiling: build/release/minisat/utils/System.o\n",
            "Compiling: build/release/minisat/utils/Options.o\n",
            "Compiling: build/release/minisat/gym/GymSolver.o\n",
            "Linking Static Library: build/release/lib/libminisat.a\n",
            "Linking Binary: build/release/bin/minisat\n",
            "Compiling: build/dynamic/minisat/core/shadow.o\n",
            "Compiling: build/dynamic/minisat/core/Solver.o\n",
            "Compiling: build/dynamic/minisat/core/Const.o\n",
            "Compiling: build/dynamic/minisat/simp/SimpSolver.o\n",
            "Compiling: build/dynamic/minisat/utils/System.o\n",
            "Compiling: build/dynamic/minisat/utils/Options.o\n",
            "Compiling: build/dynamic/minisat/gym/GymSolver.o\n",
            "Linking Shared Library: build/dynamic/lib/libminisat.so.2.1.0\n",
            "g++ -O2 -fPIC -c minisat/gym/GymSolver_wrap.c++ -o minisat/gym/GymSolver_wrap.o -I. -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wall -Wno-parentheses -Wextra -std=c++11 -I/usr/include/python3.7 -I./GSL/include\n",
            "In file included from \u001b[01m\u001b[K./minisat/simp/SimpSolver.h:25:0\u001b[m\u001b[K,\n",
            "                 from \u001b[01m\u001b[Kminisat/gym/GymSolver.h:4\u001b[m\u001b[K,\n",
            "                 from \u001b[01m\u001b[Kminisat/gym/GymSolver_wrap.c++:3121\u001b[m\u001b[K:\n",
            "\u001b[01m\u001b[K./minisat/core/Solver.h:\u001b[m\u001b[K In member function ‘\u001b[01m\u001b[KMinisat::lbool Minisat::Solver::solveLimited(const Minisat::vec<Minisat::Lit>&)\u001b[m\u001b[K’:\n",
            "\u001b[01m\u001b[K./minisat/core/Solver.h:434:56:\u001b[m\u001b[K \u001b[01;35m\u001b[Kwarning: \u001b[m\u001b[Kunused parameter ‘\u001b[01m\u001b[Kassumps\u001b[m\u001b[K’ [\u001b[01;35m\u001b[K-Wunused-parameter\u001b[m\u001b[K]\n",
            " inline lbool    Solver::solveLimited  (const vec<Lit>& \u001b[01;35m\u001b[Kassumps\u001b[m\u001b[K){ return solve_(); }\n",
            "                                                        \u001b[01;35m\u001b[K^~~~~~~\u001b[m\u001b[K\n",
            "g++ -shared -o minisat/gym/_GymSolver.so build/dynamic/minisat/core/shadow.o build/dynamic/minisat/core/Solver.o build/dynamic/minisat/core/Const.o build/dynamic/minisat/simp/SimpSolver.o build/dynamic/minisat/utils/System.o build/dynamic/minisat/utils/Options.o build/dynamic/minisat/gym/GymSolver.o minisat/gym/GymSolver_wrap.o /usr/lib/x86_64-linux-gnu/libz.so -Wall -lz -L./GSL/lib -lgsl -lgslcblas -lm\n",
            "Reading package lists... Done\n",
            "Building dependency tree       \n",
            "Reading state information... Done\n",
            "The following additional packages will be installed:\n",
            "  swig3.0\n",
            "Suggested packages:\n",
            "  swig-doc swig-examples swig3.0-examples swig3.0-doc\n",
            "The following NEW packages will be installed:\n",
            "  swig swig3.0\n",
            "0 upgraded, 2 newly installed, 0 to remove and 40 not upgraded.\n",
            "Need to get 1,100 kB of archives.\n",
            "After this operation, 5,822 kB of additional disk space will be used.\n",
            "Get:1 http://archive.ubuntu.com/ubuntu bionic/universe amd64 swig3.0 amd64 3.0.12-1 [1,094 kB]\n",
            "Get:2 http://archive.ubuntu.com/ubuntu bionic/universe amd64 swig amd64 3.0.12-1 [6,460 B]\n",
            "Fetched 1,100 kB in 7s (154 kB/s)\n",
            "Selecting previously unselected package swig3.0.\n",
            "(Reading database ... 148764 files and directories currently installed.)\n",
            "Preparing to unpack .../swig3.0_3.0.12-1_amd64.deb ...\n",
            "Unpacking swig3.0 (3.0.12-1) ...\n",
            "Selecting previously unselected package swig.\n",
            "Preparing to unpack .../swig_3.0.12-1_amd64.deb ...\n",
            "Unpacking swig (3.0.12-1) ...\n",
            "Setting up swig3.0 (3.0.12-1) ...\n",
            "Setting up swig (3.0.12-1) ...\n",
            "Processing triggers for man-db (2.8.3-2ubuntu0.1) ...\n",
            "/content/gdrive/My Drive/neuro-sat/AlphaZeroSAT\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "3HfQgkPGJw60"
      },
      "source": [
        "## Uniform Random 3-SAT\n",
        "\n",
        "We split *(u)uf50-218* and *(u)uf100-430* into three subsets: 800 training problems, 100 validation, and 100 test problems.\n",
        "\n",
        "For generalization experiments, we use 100 problems from all the other benchmarks.\n",
        "\n",
        "To evaluate the knowledge transfer properties of the trained models across different task families, we use 100 problems from all the *graph coloring* benchmarks."
      ],
      "id": "3HfQgkPGJw60"
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "mVGgy2OJJ1Ga"
      },
      "source": [
        "PROBLEM_TYPE='uniform-random-3-sat'"
      ],
      "id": "mVGgy2OJJ1Ga",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "wdosdrbtJ4eC"
      },
      "source": [
        "!bash train_val_test_split.sh \"$PROBLEM_TYPE\""
      ],
      "id": "wdosdrbtJ4eC",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "UkAeU-OpJ61V"
      },
      "source": [
        "### Train"
      ],
      "id": "UkAeU-OpJ61V"
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "13qNIbGceYHs"
      },
      "source": [
        "for TRAIN_PROBLEM_NAME, TEST_PROBLEM_NAME in zip(datasets[PROBLEM_TYPE]['train'],\n",
        "                                                datasets[PROBLEM_TYPE]['inner_test']):\n",
        "  !python train.py \\\n",
        "    --save_dir runs/\"$PROBLEM_TYPE\"/\"$TRAIN_PROBLEM_NAME\" \\\n",
        "    --best_model -1 \\\n",
        "    --status_file status.pkl \\\n",
        "    --result_file result.pkl \\\n",
        "    --dump_dir parameters \\\n",
        "    --dump_file sl.pkl \\\n",
        "    --train_path ../data/\"$PROBLEM_TYPE\"/\"$TRAIN_PROBLEM_NAME\" \\\n",
        "    --test_path ../data/\"$PROBLEM_TYPE\"/\"$TEST_PROBLEM_NAME\" \\\n",
        "    --max_clause 120 \\\n",
        "    --max_var 20 \\\n",
        "    --sl_buffer_size 1000000 \\\n",
        "    --n_batch 32 \\\n",
        "    --n_stack 1 \\\n",
        "    --n_repeat 100 \\\n",
        "    --n_start 0 \\\n",
        "    --n_train_files 0 \\\n",
        "    --n_test_files 0 \\\n",
        "    --l2_coeff 0.0001 \\\n",
        "    --sl_num_steps 64000 \\\n",
        "    --sl_n_batch 32 \\\n",
        "    --sl_n_checkpoint 32000 \\\n",
        "    --n_cycles 2 \\\n",
        "    --show_only 'No' \\\n",
        "    --which_cycle 0"
      ],
      "id": "13qNIbGceYHs",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "_iwBVB7bujSP"
      },
      "source": [
        "## Graph Coloring\n",
        "\n",
        "Graph coloring benchmarks have only 100 problems each, except for *flat50-115* which contains 1000, so we split it into three subsets: 800 training problems, 100 validation, and 100 test problems.\n",
        "\n",
        "For generalization experiments, we use 100 problems from all the other benchmarks."
      ],
      "id": "_iwBVB7bujSP"
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "z0DheaL7umDK"
      },
      "source": [
        "PROBLEM_TYPE='graph-coloring'"
      ],
      "id": "z0DheaL7umDK",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "!bash train_val_test_split.sh \"$PROBLEM_TYPE\""
      ],
      "metadata": {
        "id": "3LjDtt2rua60"
      },
      "id": "3LjDtt2rua60",
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "ihBmCPQkuttZ"
      },
      "source": [
        "### Train"
      ],
      "id": "ihBmCPQkuttZ"
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "MWTQd1kduwRY"
      },
      "source": [
        "for TRAIN_PROBLEM_NAME, TEST_PROBLEM_NAME in zip(datasets[PROBLEM_TYPE]['train'],\n",
        "                                                datasets[PROBLEM_TYPE]['inner_test']):\n",
        "  !python train.py \\\n",
        "    --save_dir runs/\"$PROBLEM_TYPE\"/\"$TRAIN_PROBLEM_NAME\" \\\n",
        "    --best_model -1 \\\n",
        "    --status_file status.pkl \\\n",
        "    --result_file result.pkl \\\n",
        "    --dump_dir parameters \\\n",
        "    --dump_file sl.pkl \\\n",
        "    --train_path ../data/\"$PROBLEM_TYPE\"/\"$TRAIN_PROBLEM_NAME\" \\\n",
        "    --test_path ../data/\"$PROBLEM_TYPE\"/\"$TEST_PROBLEM_NAME\" \\\n",
        "    --max_clause 120 \\\n",
        "    --max_var 20 \\\n",
        "    --sl_buffer_size 1000000 \\\n",
        "    --n_batch 32 \\\n",
        "    --n_stack 1 \\\n",
        "    --n_repeat 100 \\\n",
        "    --n_start 0 \\\n",
        "    --n_train_files 0 \\\n",
        "    --n_test_files 0 \\\n",
        "    --l2_coeff 0.0001 \\\n",
        "    --sl_num_steps 64000 \\\n",
        "    --sl_n_batch 32 \\\n",
        "    --sl_n_checkpoint 32000 \\\n",
        "    --n_cycles 2 \\\n",
        "    --show_only 'No' \\\n",
        "    --which_cycle 0"
      ],
      "id": "MWTQd1kduwRY",
      "execution_count": null,
      "outputs": []
    }
  ]
}