From 88ecc3df9354e9e74ccd2bc2ab5b64a19032d7e9 Mon Sep 17 00:00:00 2001 From: tawada Date: Thu, 22 Aug 2019 16:02:58 +0900 Subject: [PATCH] remove cyclic paths --- satsolver.ipynb | 40112 ++++++++++++++++++++++++++++++++++++++++++++++ solver.py | 135 +- 2 files changed, 40233 insertions(+), 14 deletions(-) create mode 100644 satsolver.ipynb diff --git a/satsolver.ipynb b/satsolver.ipynb new file mode 100644 index 0000000..9b7747a --- /dev/null +++ b/satsolver.ipynb @@ -0,0 +1,40112 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 44, + "metadata": {}, + "outputs": [], + "source": [ + "# パッケージ\n", + "%matplotlib inline\n", + "import numpy as np\n", + "import cv2 as cv # opencv\n", + "import matplotlib\n", + "import matplotlib.pyplot as plt # matplotlibの描画系\n", + "from matplotlib import cm\n", + "from collections import OrderedDict\n", + "import os\n", + "import math\n", + "import re\n", + "import glob\n" + ] + }, + { + "cell_type": "code", + "execution_count": 45, + "metadata": {}, + "outputs": [], + "source": [ + "def split(string):\n", + " re_list = re.split('[ X#@,()\\t\\n]',string)\n", + " while '' in re_list:\n", + " re_list.remove('')\n", + " return re_list\n", + " \n", + "def readQ(filename):\n", + " Q = {'BLOCK':{}}\n", + " with open(filename, 'r') as file:\n", + " while True:\n", + " str_line = file.readline()\n", + " if not str_line:\n", + " break\n", + " result = split(str_line)\n", + " if result == []:\n", + " continue\n", + " if result[0] == 'SIZE':\n", + " Q['w'] = int(result[1])\n", + " Q['h'] = int(result[2])\n", + " elif result[0] == 'BLOCK_NUM':\n", + " Q['n'] = int(result[1])\n", + " elif result[0] == 'BLOCK':\n", + " index = int(result[1])\n", + " w = int(result[2])\n", + " h = int(result[3])\n", + " bs = Q['BLOCK']\n", + " cells = {}\n", + " bs[index] = {'index':index,'w':w,'h':h,'cells':cells}\n", + " for i in range(h):\n", + " subline = file.readline()\n", + " subr = split(subline)\n", + " for j in range(w):\n", + " if subr[j] != '0':\n", + " cells[(j,i)] = subr[j]\n", + " return Q\n", + "def readA(filename):\n", + " A = {'BLOCK':{}}\n", + " with open(filename, 'r') as file:\n", + " i = 0\n", + " while True:\n", + " str_line = file.readline()\n", + " if not str_line:\n", + " break\n", + " result = split(str_line)\n", + " if result == []:\n", + " continue\n", + " if result[0] == 'SIZE':\n", + " A['w'] = int(result[1])\n", + " A['h'] = int(result[2])\n", + " A['map'] = np.zeros((A['h'],A['w']), dtype=int)\n", + " elif result[0] == 'BLOCK':\n", + " index = int(result[1])\n", + " x = int(result[2])\n", + " y = int(result[3])\n", + " bs = A['BLOCK']\n", + " cells = {}\n", + " bs[index] = {'index':index,'x':x,'y':y}\n", + " else:\n", + " for j in range(A['w']):\n", + " A['map'][i,j] = int(result[j])\n", + " i += 1 \n", + " return A\n", + "\n", + "def index2color(index, mode='cell'):\n", + " if mode == 'cell':\n", + " if index == -1:\n", + " R,G,B,Alpha = 1,1,1,1\n", + " else:\n", + " R,G,B,Alpha = cm.tab20((index*2)%20)\n", + " else:\n", + " R,G,B,Alpha = cm.tab20((index*2+1)%20)\n", + " return np.array([R,G,B])\n", + "\n", + "def QA2img(Q,A):\n", + " w_grid = 5\n", + " w_line = 25\n", + " len_cell = 50\n", + " margin = (len_cell + w_grid - w_line)//2\n", + " white = [1,1,1]\n", + " black = [0,0,0]\n", + " red = [1,0,0]\n", + " w_max, h_max = Q['w'],Q['h']\n", + " w,h,n = A['w'],A['h'],Q['n']\n", + " map_A = A['map']\n", + " bs_q = Q['BLOCK']\n", + " bs_a = A['BLOCK']\n", + " img = np.zeros((h_max*len_cell+w_grid,w_max*len_cell+w_grid,3))\n", + " img[:,:] = white\n", + " img[[i for i in range(h_max*len_cell+w_grid) if (i%len_cell)" + ] + }, + "metadata": { + "needs_background": "light" + }, + "output_type": "display_data" + } + ], + "source": [ + "show(13)" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "A015.txt\n", + "問題サイズ10×10,解答サイズ9×6\n", + "矩形領域の割合0.54\n" + ] + }, + { + "data": { + "image/png": "iVBORw0KGgoAAAANSUhEUgAAAQkAAAD8CAYAAABkQFF6AAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDMuMC4yLCBodHRwOi8vbWF0cGxvdGxpYi5vcmcvOIA7rQAAFctJREFUeJzt3X2sXVWZx/HvY8uL41t5G1PaaunQaBhGkXSUtyADMkA1ljAdAmOGau6kipCoDJEyyDQdJAMzxKpRKY0llonKu7bp4HRKITYIArfyVsDKhcjQ0rGKLWqcFxmf+eOsc7vv6bnr7nvOWufsfc/vk5zcvdfZ+znPvbn7OWuvffY65u6IiIzndf1OQESqTUVCRKJUJEQkSkVCRKJUJEQkSkVCRKKyFAkzO9vMtpvZiJkty/EaItIblvpzEmY2DfgJcCawA3gUuNDdn0n6QiLSEzl6Eu8FRtz9BXf/X+BWYFGG1xGRHpieIeYs4KXC+g7gfbEdDjfzuRkSEamjrflC/8Ldj5jsTjmKRClmthRYCvA2YLhfiYhUjOUL/WInO+UoEjuBOYX12aFtDHdfDawGWGDmoTFpImbWfK1Kx8wVt0655opbp1zJnGuncoxJPArMN7OjzOxA4AJgfYbXEZEeSN6TcPfXzOxSYCMwDbjZ3Z9O/Toi0htZxiTc/R7gnhyxRaS3kn9OohMLzHwY9huT+O/vPdWXfOrq4HP+ZMx67Lx5ZOQLPclpKjj66Mv2a8s5JpFrbA7Y6u4LJru/PpYtIlEqEiIS1bfPSUzWvKGzRpdfWLMxecxccaue66mn3jC6vGXL5clj5opb9VynkloUiXlDZyU7KIoxId3BljtujpinnnrDmIOidb3TmLDvYGs9CLuJ24tcU8Sdaip/utE86OYNnbXfu2m3XlizMXnMppRxm0Uyx99AZCKVv7rR7qBI8Y7aq7i9zHWyVzd6cVqQKm67HkmOuO1iDvrVjVqcbsC+g6L5bpri4CvGSPkOXadc63K6UYyZKq5ON8qp/OlGuwMs9WBgzi58qgKh0wzpl9r0JHKNR+QYaMw9zpEy19RXDLZsuXz0HTm11DHb5apexP4qPyYh5ekTl3loTGKKaD1AYGrcelyFQtl6kNTp9msVyu5VfkxCRPpLRUJEolQkRCRKRUJEoipVJMxszKObfYv7t3uu00eOmLG4Kf5+sddLHbdqf9sUf4Mq5JoibqcqVSREpHoqdQm0m8t/7S5xNavoVz6+ubvECi696YzkMVPFbd03HvPxruPmugR6w/kfTBbz8tv/teuY7fZtxtVs2SIy8FQkRCRKRUJEoio1JlF3l7xne6ntvvrYOzJnIpKOehIiEqUiISJRtTndyDEDdQ5HrrhmzPrLy69OErdOs2XXiWbLnlgtikSO2bJzKRaFI1dcw5ErrklWKOowW3adaPq6cipfJNpNMVeHgtHao+hG698g18xUg0p/g7jajEm8sGZjLYpDq1S9CNj3N8g1Pd6gvYO2+30H7W9QRuWLRB0LA+wrDil6FDkL5JYtl48+Bu0dtXi6kWN276mi8qcbTXWZLTrlGERR7t9fB4eMpxZFotjFrnrP4uXlV4/2HlKfaqT+G7T2Hgatq93aexi037+sWhQJqH5xKMrRk4A8fwMdGPobTKQ2RWJQrVn38yxxN95wXJa4dbLuqvv6nUItTDhwaWY3m9luM9tWaDvUzDaZ2XPh5yGh3czsy2Y2YmZPmtnxOZMXkfzKXN34BnB2S9syYLO7zwc2h3WAc4D54bEUuDFNmiLSLxMWCXffAvyypXkRsDYsrwXOLbTf4g0/BGaY2cxUyYpI75X6mj8zmwtscPdjw/ped58Rlg3Y4+4zzGwDcJ27PxCe2wxc4d74Fr/xNL/mr3WSrf+658nSv8jrF76r9La5+KqvldrOPvHJzJlIHTWPxO6nrh1XR1/z1/WHqbxRZSY9KZ+ZLTWzYTMbzjM0JyIpdHp142dmNtPdd4XTid2hfScwp7Dd7NC2H3dfDayGRk8itI3ZJtVEuD37LtCbyg3BVCLXBHFTTlgLaSatHS/mS1dsSRYTYM71p6aPG2JOlYlw1wNLwvISYF2h/aJwleME4FV339VVhiLSVxP2JMzs28BpwOFmtgNYDlwH3G5mQ8CLwPlh83uAhcAI8FvgYxlyFpEemrBIuPuF4zx1RpttHbik26REpDoqfxeoiPSXPpYtlXfyZz7X8b4PhX13dPH6s7/7uy72rj/1JEQkqjY9iTpNX5fjVvFBd9555+3XdvfddyePmyLmVFOLnkRdJpyBsTNRpZznUqRfKt+TyDWVfC45Z8seZMV3+PPOOy/ZO34zTrueijTUoidRVJdehU458sh5MOtUo73aFIm6zZadciJcGUsHc29VvkjUqTBIPaU8fZmKKj8m0VS304wmnW6ko4O5P2pRJOrUm8g1W7boNKNfalEk6kbFIa0frPx8x/uWuVX8kYtugwH/VGVM5cckRKS/VCREJEpFQkSiVCREJKrUbNm5abZskSk8W7aITG2VugR67DeOTbrvto9u6zrueDE1W3a+uClnoM4yq3Uh7vLly9MFXbECmDqzZYvIgFCREJEoFQkRiarUmMTAaDN2MXplpOS4Rhk5YiaL+/GL0yTThU1Df9TxvjcPtf1iukl58Zuru47RC+pJiEiUioSIRNXmdKMus2Xnmk+iGDflXaY54tZtTo2r3t/4fNG13x9OHjN13H6oRU9i3tBZo9PXVblANL28/Oqk09c1J9NtPlJNiZcjbnEujaoXBxh7MBeXU8RsFodUcful8j2JZg+iLj2JHHNbts7AnTpuHXLNod3BfNX7FyR552/GuPb7w7UvErXoSUD9JsJtqsO7aVOdck2htTik1IxX9wIBNSoSRXWY7zLXbNk5DuTUpzHFuFWXY7xgqpxmNFW+SDR7D/OGzhotDlXuUeToYje/5CdH3HbL3cas+mlGq2KhSFU0rv3+cO0HLJsqPyYBjaJQhwIBeSbCbcbMFbe4niIm1OfLiXJdhchxxaRfalEkoPrFoSjXKUEOdYubWq6DeCoUh6ZKF4k/3f1X/U5hcrr4qPGUuFU88ce/cztzzfMd75vlVvGKmnBMwszmmNn9ZvaMmT1tZp8K7Yea2SYzey78PCS0m5l92cxGzOxJMzs+9y8hIvmUGbh8Dfhbdz8GOAG4xMyOAZYBm919PrA5rAOcA8wPj6VAvd5eRGSMCYuEu+9y9x+F5V8DzwKzgEXA2rDZWuDcsLwIuMUbfgjMMLOZyTMXkZ6Y1ES4ZjYX2AIcC/yHu88I7QbscfcZZrYBuM7dHwjPbQaucPdxR3LGmwhX6qXsRMCgyYDbqf1EuGb2RuAu4NPu/qvic96oNJMaHTOzpWY2bGbDP5/MjiLSU6WubpjZATQKxDfdvfmtrT8zs5nuviucTuwO7TuBOYXdZ4e2Mdx9NbAaGj0JSDthLfRhItwuNK8YPPOOdyaLecz2HwPgy9+cLCaArfhV13Hb7Zsi7ngx337FhmQxAV68/kPp44aYtZsIN5xKrAGedfcvFJ5aDywJy0uAdYX2i8JVjhOAV919V1dZikjflOlJnAz8NfCUmT0e2v4OuA643cyGgBeB88Nz9wALgRHgt8DHkmYsIj01YZEIA5Dj9VfOaLO9A5d0mZeIVETlb/ASkf6q9Meyc1n12idKb/uJ6asyZtI/D77nodLbnvTYiRkzKeGUzi+X+qbm0gMdx5h77ykd7zsVqCchIlEDXST+8uprRx+DbPHFH0geM9scGBetnXgjSWpgi8SgF4ZWKQtFjslsIF+BOPKitSo+EQM5JlF0xzVX9TuFvsrRi6jTZLgqDhMb+CJR7FEMWsHIUSCachSHl29ZkvygfvmWxucBVSzGN7BForUgDNrpR7sCsfjiD3DnjfcmiZ9rImDpvYEdkxh0qYqBTH0D25No7TkM2qkG7CsUzV5FqsKh3sPUMrA9iTuuuWq0MAxigSi688Z7k/YsigOXdZkQtzk2Ifsb2J5E06AXiFyyzcKtg7nnBr5ISEK7lk28TSceKD/jVatc80kMkoE93RCRclQkRCRKRUJEoiY1W3YuvZ4t+4Gvf6X0tqf8zaUZM+mfH3z36dLbnnzuH2fMRJpqP1u2iAymSl3d6NUM1L+cRIzWfZszUKec1TpX3NHZstv8XR9c90zpOK37Z/+OUc2WnS4mPZgtW0QGm4qEiESpSIhIVKXGJGR/e66/q+N9fxB+Tmb8oYpu+ujnOt531UebS53/Df5x1TEd7zsVqCchIlEqEiISNdCnG3WbUyL1vA+546a24qSVo8vLH/xM8pgp404lA1skmgWi6oUht5zzXKa04qSVYw7g1vVOY8K+wrDipJVJ4k41A3+6UZe5LetyMOeS48Bd/uBnVBBKGOgi0Zydqupf0JPzNKPqpxjttJ4ipIyporG/gS0SxdOMupxyNIvF4os/0HXPohir2Fb1HosO5t4b6DGJZnGoci8CxvYgUr37t8ZsbauiHAVCRWdiA1skmqcZzWWptuIpRqoDu13MFHGnmoEtElDP4pDj3b7qPQjIN3ApExvIInHoP5efdKbfDrniLzreN3areJ18/Buf73hfTYTbvQkHLs3sYDN7xMyeMLOnzWxFaD/KzB42sxEzu83MDgztB4X1kfD83Ly/gojkVObqxv8Ap7v7u4HjgLPN7ATgemClux8N7AGGwvZDwJ7QvjJsJyI1NWGR8IbfhNUDwsOB04E7Q/ta4NywvCisE54/w7qdGkdE+qbU5yTMbJqZPQ7sBjYBzwN73f21sMkOYFZYngW8BBCefxU4LGXSItJD7l76AcwA7gdOAUYK7XOAbWF5GzC78NzzwOFtYi0FhoHht4G7Hnro4Q5OvsfwZI735mNSn7h0972hSJwIzDCz5tWR2cDOsLwzFA3C828BXmkTa7W7L3D3BUdMJgkR6akJL4Ga2RHA79x9r5m9HjiTxmDk/cBi4FZgCbAu7LI+rD8Unr/PJ7gGt5XGdw1km305YdzsM0UPaK654irX7mfLLvM5iZnAWjObRmMM43Z332BmzwC3mtnngceANWH7NcC/mNkIjdnrL+gqQxHpq0p8g5eZOajap45bp1xzxVWuY3oS+gYvEUlPRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEoir1DV65Zt7PEVe51iuucu2cehIiElWpnoSmGBvcXHPFVa7d90zUkxCRKBUJEYlSkRCRKBUJEYlSkRCRKBUJEYlSkRCRKBUJEYlSkRCRKBUJEYlSkRCRKBUJEYlSkRCRKBUJEYlSkRCRqNJFwsymmdljZrYhrB9lZg+b2YiZ3WZmB4b2g8L6SHh+bp7URaQXJtOT+BTwbGH9emClux8N7AGGQvsQsCe0rwzbiUhNlSoSZjYb+CDw9bBuwOnAnWGTtcC5YXlRWCc8f4ZVbdI+ESmtbE/ii8Bngd+H9cOAve7+WljfAcwKy7OAlwDC86+G7UWkhiac49LMPgTsdvetZnZaqhc2s6XA0pa2VOFbX6sWMXPFrVOuueIq186VmQj3ZODDZrYQOBh4M/AlYIaZTQ+9hdnAzrD9TmAOsMPMpgNvAV5pDeruq4HVAGaWduZPEUlmwiLh7lcCVwKEnsTl7v4RM7sDWAzcCiwB1oVd1of1h8Lz93nJ6X81o/Hg5porrnLt72zZVwCXmdkIjTGHNaF9DXBYaL8MWNZVhiLSV5a6anWURDjdULUf3FxzxVWuY3oSW919wWT31ycuRSRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEolQkRCRKRUJEosrMcdkzmqxUueaKq1w7p56EiERVqiehKcYGN9dccZVrfyfCFZEBoCIhIlEqEiISpSIhIlEqEiISpSIhIlEqEiISpSIhIlEqEiISpSIhIlEqEiISpSIhIlEqEiISpSIhIlEqEiISVapImNlPzewpM3vczIZD26FmtsnMngs/DwntZmZfNrMRM3vSzI7P+QuISF6T6Un8mbsf5+4LwvoyYLO7zwc2h3WAc4D54bEUuDFVsiLSe92cbiwC1obltcC5hfZbvOGHwAwzm9nF64hIH5UtEg78u5ltNbOloe2t7r4rLP8n8NawPAt4qbDvjtAmIjVUdo7LU9x9p5n9IbDJzH5cfNLd3cwmNTFfKDZLW9omE2Iyr1WLmLni1inXXHGVa+dK9STcfWf4uRv4DvBe4GfN04jwc3fYfCcwp7D77NDWGnO1uy8ojHGISAVN2JMwszcAr3P3X4flPwf+AVgPLAGuCz/XhV3WA5ea2a3A+4BXC6cl4/kNsL2zX6HnDgd+0e8kSlKu+dQp32aub+9k5zKnG28FvhO6QNOBb7n7v5nZo8DtZjYEvAicH7a/B1gIjAC/BT5W4jW216VHYWbDyjW9OuUK9cq321wnLBLu/gLw7jbtrwBntGl34JJOExKRatEnLkUkqipFYnW/E5gE5ZpHnXKFeuXbVa6W+ivFRGRqqUpPQkQqqu9FwszONrPt4YawZRPvkT2fm81st5ltK7RV8mY2M5tjZveb2TNm9rSZfaqq+ZrZwWb2iJk9EXJdEdqPMrOHQ063mdmBof2gsD4Snp/bq1wLOU8zs8fMbEOVc81+A6a79+0BTAOeB+YBBwJPAMf0OadTgeOBbYW2fwKWheVlwPVheSHwPcCAE4CHe5zrTOD4sPwm4CfAMVXMN7zmG8PyAcDDIYfbgQtC+yrg4rD8SWBVWL4AuK0P/wuXAd8CNoT1SuYK/BQ4vKUt2f9AT//obX65E4GNhfUrgSv7mVPIY25LkdgOzAzLM2l8rgPgJuDCdtv1Ke91wJlVzxf4A+BHND5s9wtgeuv/A7ARODEsTw/bWQ9znE3j7ubTgQ3hoKpqru2KRLL/gX6fbtTlZrDK38wWurjvofEOXcl8Q/f9cRof4d9Eoxe5191fa5PPaK7h+VeBw3qVK/BF4LPA78P6YVQ316w3YJa9wUsC98nfzJabmb0RuAv4tLv/qniDUJXydff/A44zsxk07gF6Z59TasvMPgTsdvetZnZav/MpIfkNmEX97kmUuhmsArq6mS0nMzuARoH4prvfHZormy+Au+8F7qfRZZ9hZs03q2I+o7mG598CvNKjFE8GPmxmPwVupXHK8aWK5opnuAGzqN9F4lFgfhg1PpDGoM/6PufUTvNmNtj/ZraLwojxCZS7mS0Za3QZ1gDPuvsXqpyvmR0RehCY2etpjJ08S6NYLB4n1+bvsBi4z8NJdG7ufqW7z3b3uTT+J+9z949UMVcze4OZvam5TOMGzG2k/B/o1eBKZNBlIY1R+eeBqyqQz7eBXcDvaJyvDdE4v9wMPAfcCxwatjXgqyH3p4AFPc71FBrno08Cj4fHwirmC7wLeCzkug34+9A+D3iExg2BdwAHhfaDw/pIeH5en/4fTmPf1Y3K5RpyeiI8nm4eQyn/B/SJSxGJ6vfphohUnIqEiESpSIhIlIqEiESpSIhIlIqEiESpSIhIlIqEiET9PzJFKXsQoGb+AAAAAElFTkSuQmCC\n", + "text/plain": [ + "
" + ] + }, + "metadata": { + "needs_background": "light" + }, + "output_type": "display_data" + } + ], + "source": [ + "show(14)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "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.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/solver.py b/solver.py index 36e4559..f54d5dd 100644 --- a/solver.py +++ b/solver.py @@ -1,6 +1,6 @@ # パッケージ -%matplotlib inline +#%matplotlib inline import numpy as np import cv2 as cv # opencv import matplotlib @@ -84,6 +84,22 @@ def readA(filename): i += 1 return A +def strA(A): + r = [] + w = A['w'] + h = A['h'] + num_b = A['num_b'] + r.append(f'SIZE {w}X{h}\n') + for i in range(h): + r.append(','.join(map(str,A['map'][i]))) + r.append('\n') + block_list = A['BLOCK'] + for i in range(1, num_b+1): + x = block_list[i]['x'] + y = block_list[i]['y'] + r.append(f'BLOCK#{i} @({x},{y})\n') + return ''.join(r) + def index2color(index, mode='cell'): if mode == 'cell': if index == -1: @@ -168,9 +184,7 @@ def show(index, read=None): cv.imwrite(f'A{index+1:03}.png', img_uint8) plt.imshow(img) - - - + def add(e, _dict): if e not in _dict.keys(): _dict[e] = len(_dict) + 1 @@ -194,6 +208,7 @@ def read_satA(filename, Q, nodes, TF=None): str_line = file.readline() if str_line.startswith('UNSAT'): print('UNSAT') + return None else: print('SAT') str_line = file.readline() @@ -214,6 +229,8 @@ def read_satA(filename, Q, nodes, TF=None): A['map'] = np.zeros((h,w), dtype=int) num_b = len(Q['BLOCK']) num_l = Q['num_l'] + A['num_b'] = num_b + A['num_l'] = num_l for i in range(1, num_b+1): A['BLOCK'][i] = {'index':i,'x':0,'y':0} for i in range(h): @@ -233,6 +250,85 @@ def read_satA(filename, Q, nodes, TF=None): index = nodes[key] if TF[index]: A['map'][i][j] = l + ## 閉路の削除 + validation_map = np.zeros((h, w), dtype=int) + check_flag = np.zeros(num_l+1) + map = A['map'] + + # 端点から探索し + for b in range(1, num_b): + for dx,dy in Q['BLOCK'][b]['cells'].keys(): + c = Q['BLOCK'][b]['cells'][(dx,dy)] + + # 配線でないならcontinue + if c == '+' or c == '0': + continue + c = int(c) + + # 探索済みならcontinue + if check_flag[c] == 1: + continue + + x, y = A['BLOCK'][b]['x']+dx, A['BLOCK'][b]['y']+dy + while True: + validation_map[y, x] = 1 + x -= 1 + if x >= 0 and map[y, x] == c and validation_map[y, x] == 0: + continue + x += 2 + if x <= w-1 and map[y, x] == c and validation_map[y, x] == 0: + continue + x -= 1 + y -= 1 + if y >= 0 and map[y, x] == c and validation_map[y, x] == 0: + continue + y += 2 + if y <= h-1 and map[y, x] == c and validation_map[y, x] == 0: + continue + y -= 1 + break + check_flag[c] = 1 + # validation_mapが0 => 端点と接続していない => 閉路 + A['map'] = A['map'] * validation_map + + ## 最小矩形に更新 + map_l = A['map'] + h, w = map_l.shape + map_b = np.zeros((h, w), dtype=int) + for b in range(1, num_b+1): + x = A['BLOCK'][b]['x'] + y = A['BLOCK'][b]['y'] + for dx,dy in Q['BLOCK'][b]['cells'].keys(): + map_b[y+dy,x+dx] = b + i = 0 + while True: + if i >= h: + break + if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): + np.delete(map_l, i, axis=0) + np.delete(map_b, i, axis=0) + for b in range(1, num_b+1): + if A['BLOCK'][b]['y'] > i: + A['BLOCK'][b]['y'] -= 1 + h -= 1 + i -= 1 + i += 1 + j = 0 + while True: + if j >= w: + break + if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): + np.delete(map_l, j, axis=1) + np.delete(map_b, j, axis=1) + for b in range(1, num_b+1): + if A['BLOCK'][b]['x'] > j: + A['BLOCK'][b]['x'] -= 1 + w -= 1 + j -= 1 + j += 1 + A['map'] = map_l + A['h'] = h + A['w'] = w return A def debug_satA(filename, Q, nodes, TF=None): @@ -263,14 +359,20 @@ def debug_satA(filename, Q, nodes, TF=None): return A -def generate_sat(Q): +def generate_sat(Q, WH=None): nodes = {} cnfs = [] num_b = len(Q['BLOCK']) num_l = Q['num_l'] - w = Q['w'] = 20 - h = Q['h'] = 20 + w = Q['w'] + h = Q['h'] + + if not WH is None: + w = WH[0] + h = WH[1] + Q['w'] = WH[0] + Q['h'] = WH[1] # ラインからブロック番号, 位置を逆引き l2b = [[] for _ in range(num_l+1)] @@ -547,7 +649,7 @@ def generate_sat(Q): def main(): - Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') + #Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') #Q = readQ('./adc2019problem/Q002_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q003_10X10_b5_l5.txt') #Q = readQ('./adc2019problem/Q004_10X10_b8_l9.txt') @@ -560,17 +662,22 @@ def main(): #Q = readQ('./adc2019problem/Q013_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q014_10X10_b9_l9.txt') #Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt') + #Q = readQ('./adc2019problem/QRAND327_20X20_b20_l15.txt') + Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') - start_time = time.time() - nodes,cnfs = generate_sat(Q) + #start_time = time.time() + nodes,cnfs = generate_sat(Q, WH=None) print_cnf(nodes, cnfs) os.system('minisat p.txt a.txt') A = read_satA('a.txt', Q, nodes) + if A is None: + return + print(strA(A)) #A = debug_satA('a.txt', Q, nodes) - end_time= time.time() - print(f"経過時間：{end_time - start_time}") - img = QA2img(Q,A) - plt.imshow(img) + #end_time= time.time() + #print(f"経過時間：{end_time - start_time}") + #img = QA2img(Q,A) + #plt.imshow(img) main() -- 2.22.0