SMT_Z3_Sudoku.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "2cccb11a",
   "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": "9317f647",
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "from internal import utils"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "04b4d2ca",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Modify the variables accordingly here! ####\n",
    "problem_file = \"puzzle.txt\" # file name for problem description\n",
    "data_dir = \"./datasets\"      # folder that contains problem file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "bbadee4e",
   "metadata": {},
   "outputs": [],
   "source": [
    "# experiment flag for checkpoint category\n",
    "experiment = \"sudoku\"           \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": "f3b920e4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "8, 0, 0, 0, 0, 0, 0, 0, 0\n",
      "0, 0, 3, 6, 0, 0, 0, 0, 0\n",
      "0, 7, 0, 0, 9, 0, 2, 0, 0\n",
      "0, 5, 0, 0, 0, 7, 0, 0, 0\n",
      "0, 0, 0, 0, 4, 5, 7, 0, 0\n",
      "0, 0, 0, 1, 0, 0, 0, 3, 0\n",
      "0, 0, 1, 0, 0, 0, 0, 6, 8\n",
      "0, 0, 8, 5, 0, 0, 0, 1, 0\n",
      "0, 9, 0, 0, 0, 0, 4, 0, 0\n"
     ]
    }
   ],
   "source": [
    "# Check out specific input problem file as expected\n",
    "if not utils.file_exists(data_path):\n",
    "  raise ValueError(f\"Specified input data file do not exist: {data_path}\")\n",
    "with open(data_path, 'r') as f:\n",
    "    data_file = f.read()\n",
    "print(data_file)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "6fb7ddc9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution of sudoku problem:\n",
      "8 1 2 7 5 3 6 4 9\n",
      "9 4 3 6 8 2 1 7 5\n",
      "6 7 5 4 9 1 2 8 3\n",
      "1 5 4 2 3 7 8 9 6\n",
      "3 6 9 8 4 5 7 2 1\n",
      "2 8 7 1 6 9 5 3 4\n",
      "5 2 1 9 7 4 3 6 8\n",
      "4 3 8 5 2 6 9 1 7\n",
      "7 9 6 3 1 8 4 5 2\n",
      "\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']      = \"sudoku\"                            # only cnf | sudoku | latin_square are supported\n",
    "os.environ['PROB_TYPE']        = \"smt\"                               # 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": "d8c19dc3",
   "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
}