SMT_Z3_Latin_Square.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "88649f1f",
   "metadata": {},
   "outputs": [],
   "source": [
    "try:\n",
    "  import google.colab\n",
    "  IN_COLAB = True\n",
    "except:\n",
    "  IN_COLAB = False\n",
    "if IN_COLAB:\n",
    "  # @title Mount Google Drive\n",
    "  # @markdown Mount Google Drive onto `/content/gdrive`. You can skip this if running locally.\n",
    "  from google.colab import drive\n",
    "  drive.mount('/content/gdrive', force_remount=True)\n",
    "  # @markdown Then insert the directory to your python path, you might want to change the path accroding to your need.\n",
    "  import sys\n",
    "  sys.path.insert(0, '/content/gdrive/MyDrive/SAT-Problem')\n",
    "  print(sys.path)\n",
    "  # @markdown Change the following path accrodingly.\n",
    "  %cd /content/gdrive/MyDrive/SAT-Problem\n",
    "  # @markdown Install requirement packages.\n",
    "  !pip install -r requirements.txt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "b83406cd",
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "from internal import utils"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "487da15d",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Modify the variables accordingly here! ####\n",
    "problem_file = \"Latin_Square_Problem_HARD.txt\" # file name for problem description\n",
    "data_dir = \"./datasets\"       # folder that contains problem file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "8c09a0b4",
   "metadata": {},
   "outputs": [],
   "source": [
    "# experiment flag for checkpoint category\n",
    "experiment = \"latin_square\"           \n",
    "# checkpoint path that store ouptut result/ configuration backup\n",
    "ckpt_path = os.path.join(os.getcwd(), \"checkpoint\", \"sat\", \"z3\")\n",
    "# full path of specified data file\n",
    "data_path = os.path.join(os.getcwd(), data_dir, problem_file)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "5dc3a180",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0,1,2,0\n",
      "2,0,0,1\n",
      "1,0,0,2\n",
      "0,0,1,0\n"
     ]
    }
   ],
   "source": [
    "# Check input data file exist\n",
    "if not utils.file_exists(data_path):\n",
    "  raise ValueError(f\"Specified input data file do not exist: {data_path}\")\n",
    "# Check out specific input problem file as expected\n",
    "with open(data_path, 'r') as f:\n",
    "    data_file = f.read()\n",
    "print(data_file)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "abc29602",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution of latin_square problem:\r\n",
      "3 1 2 4\r\n",
      "2 3 4 1\r\n",
      "1 4 3 2\r\n",
      "4 2 1 3\r\n",
      "\r\n"
     ]
    }
   ],
   "source": [
    "os.environ['CKPT_DIR']         = ckpt_path\n",
    "os.environ['DATA_FILE']        = data_path                           # full path of specified data file\n",
    "os.environ['SOLVER_TYPE']      = \"z3\"                                # adopt z3-solver for backend problem solving\n",
    "os.environ['PUZZLE_TYPE']      = \"latin_square\"                      # only cnf | sudoku | latin_square are supported\n",
    "os.environ['PROB_TYPE']        = \"sat\"                               # solving technology\n",
    "os.environ['DATA_EXT']         = utils.get_extention(problem_file)   # file extension\n",
    "!python -m eval \\\n",
    "  --gin_bindings=\"Config.puzzle_type    = '${PUZZLE_TYPE}'\" \\\n",
    "  --gin_bindings=\"Config.data_ext       = '${DATA_EXT}'\" \\\n",
    "  --gin_bindings=\"Config.solver_type    = '${SOLVER_TYPE}'\" \\\n",
    "  --gin_bindings=\"Config.data_file      = '${DATA_FILE}'\" \\\n",
    "  --gin_bindings=\"Config.data_ext       = '${DATA_EXT}'\" \\\n",
    "  --gin_bindings=\"Config.checkpoint_dir = '${CKPT_DIR}'\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ade1acfb",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "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.8.10"
  },
  "vscode": {
   "interpreter": {
    "hash": "b0fa6594d8f4cbf19f97940f81e996739fb7646882a419484c72d19e05852a7e"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}