{ "cells": [ { "cell_type": "code", "execution_count": 5, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "\n", " \n", " " ], "text/plain": [ "" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "import random\n", "from IPython.core.display import SVG\n", "import pyomo.environ as pyo\n", "from pysat.solvers import Solver\n", "from pysat.formula import CNF \n", "import py_svg_combinatorics as psc\n", "from ipywidgets import widgets, HBox\n", "from collections import Counter\n", "from pprint import pprint\n", "from random import randint\n", "import numpy as np\n", "from IPython.display import IFrame\n", "from IPython.display import display\n", "import IPython\n", "from copy import copy\n", "import os\n", "from pyomo_helpers import * \n", "import pandas\n", "from pathlib import Path\n", "from pyomo_helpers import pretty_solution\n", "nbname = ''\n", "try:\n", " nbname = __vsc_ipynb_file__\n", "except:\n", " if 'COCALC_JUPYTER_FILENAME' in os.environ:\n", " nbname = os.environ['COCALC_JUPYTER_FILENAME'] \n", "title_ = Path(nbname).stem.replace('-', '_').title() \n", "IFrame(f'https://discopal.ispras.ru/index.php?title=Hardprob/{title_}&useskin=cleanmonobook', width=1280, height=300)" ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "collapsed": false }, "outputs": [], "source": [ "d = 10\n", "n = 5 # Number of vectors in X\n", "M = 4\n", "\n", "vectors = np.random.randint(0, 2, size=(d, n))" ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 x0x1x2x3x4
010110
101110
211100
301010
400110
510111
610110
711100
811001
901000
\n" ], "text/plain": [ "" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "def visualize(vectors):\n", " df = pd.DataFrame(vectors, columns=[\"x\" + str(i) for i in range(vectors.shape[1])])\n", " s = df.style.set_table_styles( [{'selector': 'td',\n", " 'props': [\n", " ('border-left', '2px solid black !important'),\n", " ('border-right','2px solid black !important')\n", " ]}])\n", " return s\n", "visualize(vectors)" ] }, { "cell_type": "code", "execution_count": 8, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def модель(вектора, M):\n", " m = pyo.ConcreteModel()\n", " m.множества = range(M)\n", " m.В = range(вектора.shape[1])\n", " m.D = range(вектора.shape[0])\n", " m.вектора = вектора\n", " m.X = pyo.Var(m.В, m.множества, domain=pyo.Binary)\n", " m.является_покрытием = pyo.Var(m.множества, domain=pyo.Binary) \n", " \n", " @m.Objective(sense=pyo.maximize)\n", " def количество_покрытий(m, в):\n", " return sum(m.является_покрытием[...]) # важно указывать слайс при суммировании!\n", " \n", " @m.Constraint(m.В)\n", " def ровно_в_одном_множестве(m, в):\n", " return sum(m.X[в, ...]) == 1\n", " \n", " @m.Constraint(m.множества, m.D)\n", " def проверка_является_покрытием(m, мн, d):\n", " #Если хоть кто-то в мн 0 - то мн не покрытие\n", " return (m.вектора @ m.X)[d, мн] >= m.является_покрытием[мн]\n", "\n", " # @m.Constraint()\n", " # def wtf(m):\n", " # return m.X[1,0]==1\n", "\n", " return m" ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "2 Var Declarations\n", " X : Size=20, Index={0, 1, 2, 3, 4}*{0, 1, 2, 3}\n", " Key : Lower : Value : Upper : Fixed : Stale : Domain\n", " (0, 0) : 0 : None : 1 : False : True : Binary\n", " (0, 1) : 0 : None : 1 : False : True : Binary\n", " (0, 2) : 0 : None : 1 : False : True : Binary\n", " (0, 3) : 0 : None : 1 : False : True : Binary\n", " (1, 0) : 0 : None : 1 : False : True : Binary\n", " (1, 1) : 0 : None : 1 : False : True : Binary\n", " (1, 2) : 0 : None : 1 : False : True : Binary\n", " (1, 3) : 0 : None : 1 : False : True : Binary\n", " (2, 0) : 0 : None : 1 : False : True : Binary\n", " (2, 1) : 0 : None : 1 : False : True : Binary\n", " (2, 2) : 0 : None : 1 : False : True : Binary\n", " (2, 3) : 0 : None : 1 : False : True : Binary\n", " (3, 0) : 0 : None : 1 : False : True : Binary\n", " (3, 1) : 0 : None : 1 : False : True : Binary\n", " (3, 2) : 0 : None : 1 : False : True : Binary\n", " (3, 3) : 0 : None : 1 : False : True : Binary\n", " (4, 0) : 0 : None : 1 : False : True : Binary\n", " (4, 1) : 0 : None : 1 : False : True : Binary\n", " (4, 2) : 0 : None : 1 : False : True : Binary\n", " (4, 3) : 0 : None : 1 : False : True : Binary\n", " является_покрытием : Size=4, Index={0, 1, 2, 3}\n", " Key : Lower : Value : Upper : Fixed : Stale : Domain\n", " 0 : 0 : None : 1 : False : True : Binary\n", " 1 : 0 : None : 1 : False : True : Binary\n", " 2 : 0 : None : 1 : False : True : Binary\n", " 3 : 0 : None : 1 : False : True : Binary\n", "\n", "1 Objective Declarations\n", " количество_покрытий : Size=1, Index=None, Active=True\n", " Key : Active : Sense : Expression\n", " None : True : maximize : является_покрытием[0] + является_покрытием[1] + является_покрытием[2] + является_покрытием[3]\n", "\n", "2 Constraint Declarations\n", " проверка_является_покрытием : Size=40, Index={0, 1, 2, 3}*{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}, Active=True\n", " Key : Lower : Body : Upper : Active\n", " (0, 0) : -Inf : является_покрытием[0] - (X[0,0] + 0*X[1,0] + X[2,0] + X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 1) : -Inf : является_покрытием[0] - (0*X[0,0] + X[1,0] + X[2,0] + X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 2) : -Inf : является_покрытием[0] - (X[0,0] + X[1,0] + X[2,0] + 0*X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 3) : -Inf : является_покрытием[0] - (0*X[0,0] + X[1,0] + 0*X[2,0] + X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 4) : -Inf : является_покрытием[0] - (0*X[0,0] + 0*X[1,0] + X[2,0] + X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 5) : -Inf : является_покрытием[0] - (X[0,0] + 0*X[1,0] + X[2,0] + X[3,0] + X[4,0]) : 0.0 : True\n", " (0, 6) : -Inf : является_покрытием[0] - (X[0,0] + 0*X[1,0] + X[2,0] + X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 7) : -Inf : является_покрытием[0] - (X[0,0] + X[1,0] + X[2,0] + 0*X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (0, 8) : -Inf : является_покрытием[0] - (X[0,0] + X[1,0] + 0*X[2,0] + 0*X[3,0] + X[4,0]) : 0.0 : True\n", " (0, 9) : -Inf : является_покрытием[0] - (0*X[0,0] + X[1,0] + 0*X[2,0] + 0*X[3,0] + 0*X[4,0]) : 0.0 : True\n", " (1, 0) : -Inf : является_покрытием[1] - (X[0,1] + 0*X[1,1] + X[2,1] + X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 1) : -Inf : является_покрытием[1] - (0*X[0,1] + X[1,1] + X[2,1] + X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 2) : -Inf : является_покрытием[1] - (X[0,1] + X[1,1] + X[2,1] + 0*X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 3) : -Inf : является_покрытием[1] - (0*X[0,1] + X[1,1] + 0*X[2,1] + X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 4) : -Inf : является_покрытием[1] - (0*X[0,1] + 0*X[1,1] + X[2,1] + X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 5) : -Inf : является_покрытием[1] - (X[0,1] + 0*X[1,1] + X[2,1] + X[3,1] + X[4,1]) : 0.0 : True\n", " (1, 6) : -Inf : является_покрытием[1] - (X[0,1] + 0*X[1,1] + X[2,1] + X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 7) : -Inf : является_покрытием[1] - (X[0,1] + X[1,1] + X[2,1] + 0*X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (1, 8) : -Inf : является_покрытием[1] - (X[0,1] + X[1,1] + 0*X[2,1] + 0*X[3,1] + X[4,1]) : 0.0 : True\n", " (1, 9) : -Inf : является_покрытием[1] - (0*X[0,1] + X[1,1] + 0*X[2,1] + 0*X[3,1] + 0*X[4,1]) : 0.0 : True\n", " (2, 0) : -Inf : является_покрытием[2] - (X[0,2] + 0*X[1,2] + X[2,2] + X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 1) : -Inf : является_покрытием[2] - (0*X[0,2] + X[1,2] + X[2,2] + X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 2) : -Inf : является_покрытием[2] - (X[0,2] + X[1,2] + X[2,2] + 0*X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 3) : -Inf : является_покрытием[2] - (0*X[0,2] + X[1,2] + 0*X[2,2] + X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 4) : -Inf : является_покрытием[2] - (0*X[0,2] + 0*X[1,2] + X[2,2] + X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 5) : -Inf : является_покрытием[2] - (X[0,2] + 0*X[1,2] + X[2,2] + X[3,2] + X[4,2]) : 0.0 : True\n", " (2, 6) : -Inf : является_покрытием[2] - (X[0,2] + 0*X[1,2] + X[2,2] + X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 7) : -Inf : является_покрытием[2] - (X[0,2] + X[1,2] + X[2,2] + 0*X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (2, 8) : -Inf : является_покрытием[2] - (X[0,2] + X[1,2] + 0*X[2,2] + 0*X[3,2] + X[4,2]) : 0.0 : True\n", " (2, 9) : -Inf : является_покрытием[2] - (0*X[0,2] + X[1,2] + 0*X[2,2] + 0*X[3,2] + 0*X[4,2]) : 0.0 : True\n", " (3, 0) : -Inf : является_покрытием[3] - (X[0,3] + 0*X[1,3] + X[2,3] + X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 1) : -Inf : является_покрытием[3] - (0*X[0,3] + X[1,3] + X[2,3] + X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 2) : -Inf : является_покрытием[3] - (X[0,3] + X[1,3] + X[2,3] + 0*X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 3) : -Inf : является_покрытием[3] - (0*X[0,3] + X[1,3] + 0*X[2,3] + X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 4) : -Inf : является_покрытием[3] - (0*X[0,3] + 0*X[1,3] + X[2,3] + X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 5) : -Inf : является_покрытием[3] - (X[0,3] + 0*X[1,3] + X[2,3] + X[3,3] + X[4,3]) : 0.0 : True\n", " (3, 6) : -Inf : является_покрытием[3] - (X[0,3] + 0*X[1,3] + X[2,3] + X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 7) : -Inf : является_покрытием[3] - (X[0,3] + X[1,3] + X[2,3] + 0*X[3,3] + 0*X[4,3]) : 0.0 : True\n", " (3, 8) : -Inf : является_покрытием[3] - (X[0,3] + X[1,3] + 0*X[2,3] + 0*X[3,3] + X[4,3]) : 0.0 : True\n", " (3, 9) : -Inf : является_покрытием[3] - (0*X[0,3] + X[1,3] + 0*X[2,3] + 0*X[3,3] + 0*X[4,3]) : 0.0 : True\n", " ровно_в_одном_множестве : Size=5, Index={0, 1, 2, 3, 4}, Active=True\n", " Key : Lower : Body : Upper : Active\n", " 0 : 1.0 : X[0,0] + X[0,1] + X[0,2] + X[0,3] : 1.0 : True\n", " 1 : 1.0 : X[1,0] + X[1,1] + X[1,2] + X[1,3] : 1.0 : True\n", " 2 : 1.0 : X[2,0] + X[2,1] + X[2,2] + X[2,3] : 1.0 : True\n", " 3 : 1.0 : X[3,0] + X[3,1] + X[3,2] + X[3,3] : 1.0 : True\n", " 4 : 1.0 : X[4,0] + X[4,1] + X[4,2] + X[4,3] : 1.0 : True\n", "\n", "5 Declarations: X является_покрытием количество_покрытий ровно_в_одном_множестве проверка_является_покрытием\n" ] } ], "source": [ "m = модель(vectors, M)\n", "m.pprint()\n", "\n" ] }, { "cell_type": "code", "execution_count": 10, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "# ==========================================================\n", "# = Solver Results =\n", "# ==========================================================\n", "# ----------------------------------------------------------\n", "# Problem Information\n", "# ----------------------------------------------------------\n", "Problem: \n", "- Name: unknown\n", " Lower bound: 1.0\n", " Upper bound: 1.0\n", " Number of objectives: 1\n", " Number of constraints: 36\n", " Number of variables: 23\n", " Number of binary variables: 24\n", " Number of integer variables: 24\n", " Number of nonzeros: 4\n", " Sense: maximize\n", "# ----------------------------------------------------------\n", "# Solver Information\n", "# ----------------------------------------------------------\n", "Solver: \n", "- Status: ok\n", " User time: -1.0\n", " System time: 0.0\n", " Wallclock time: 0.01\n", " Termination condition: optimal\n", " Termination message: Model was solved to optimality (subject to tolerances), and an optimal solution is available.\n", " Statistics: \n", " Branch and bound: \n", " Number of bounded subproblems: 0\n", " Number of created subproblems: 0\n", " Black box: \n", " Number of iterations: 0\n", " Error rc: 0\n", " Time: 0.03879690170288086\n", "# ----------------------------------------------------------\n", "# Solution Information\n", "# ----------------------------------------------------------\n", "Solution: \n", "- number of solutions: 0\n", " number of solutions displayed: 0\n" ] } ], "source": [ "solver = pyo.SolverFactory('cbc')\n", "# solver = pyo.SolverFactory('scip')\n", "solver.solve(m).write()" ] }, { "cell_type": "code", "execution_count": 11, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def solve_d_vectors(vectors, M, solver_name='cbc'):\n", " m = модель(vectors, M)\n", " solver = pyo.SolverFactory(solver_name)\n", " solver.solve(m)\n", " cover = np.array([pyo.value(m.является_покрытием[i]) for i in range(M)])\n", " solution = np.array([[int(pyo.value(m.X[i, j])) for j in range(M)] for i in range(vectors.shape[1])])\n", " solution = solution[..., cover > 0]\n", " answer = m.количество_покрытий()\n", " return answer, solution" ] }, { "cell_type": "code", "execution_count": 12, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def visualize_solution(solution):\n", " df = pd.DataFrame(solution, columns=[\"s\" + str(i) for i in range(solution.shape[1])], index=[\"x\" + str(i) for i in range(solution.shape[0])])\n", " return df.style.background_gradient()" ] }, { "cell_type": "code", "execution_count": 13, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 s0
x00
x11
x21
x30
x40
\n" ], "text/plain": [ "" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "visualize_solution(solve_d_vectors(vectors, M)[1])" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "## Сведение Sat к d-vector covering\n", "### Идея\n", "\n", "Подробнее посмотрим на условие, что k-е подмножество покрывает i-ю координату вектора: \n", "$\\sum_{j}{V_{ij} S_{jk} > 0}$, \n", "\n", "где \n", "- $V$-матрица векторов, \n", "- $S$ - матрица множеств.\n", "\n", "\n", "Или иначе $\\lor_{j}{(V_{ij} = S_{jk} = 1)}$. Это дизъюнкция. \n", "\n", "Значит размерность `d` будет отвечать за число дизъюнкций в КНФ. \n", "А размерность `n` — число переменных в формуле. \n", "\n", "Рассмотрим на примере следующей КНФ: \n", "\n", "$(x1 \\lor \\overline{x2} \\lor x3) \\land (\\overline{x1} \\lor x2 \\lor \\overline{x4})$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "| closure| $x1$ | $\\overline{x1}$ | $x2$ | $\\overline{x2}$ | $x3$ | $\\overline{x3}$ | $x4$ | $\\overline{x4}$ |\n", "|------------------------------------------|------|-----------------|------|-----------------|------|-----------------|------|-----------------|\n", "|$x1 \\lor \\overline{x2} \\lor x3$ | **1**| 0| 0| **1**| **1**| 0| 0| 0|\n", "|$\\overline{x1} \\lor x2 \\lor \\overline{x4}$| 0| **1**| **1**| 0| 0| 0| 0| **1**|" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Тогда покрывающее множество векторов - решение КНФ\n", "\n", "### Как не взять всё? \n", "В текущем подходе есть проблема - можно взять всё. Например одновременно переменную и её отрицание. \n", "\n", "Решение: будем разбивать переменные в два множества. Их условно можно назвать `True` и `False`. КНФ решаема тогда и только тогда когда все переменные можно непротиворечиво разбить на два этих множества.\n", "\n", "Осталось только форсировать непротиворечивое разбиение. \n", "Для этого добавим тавтологические дизъюнкции в КНФ $xn \\lor \\overline{xn}$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "| closure| $x1$ | $\\overline{x1}$ | $x2$ | $\\overline{x2}$ | $x3$ | $\\overline{x3}$ | $x4$ | $\\overline{x4}$ |\n", "|------------------------------------------|------|-----------------|------|-----------------|------|-----------------|------|-----------------|\n", "|$x1 \\lor \\overline{x2} \\lor x3$ | **1**| 0 | 0 | **1**| **1**| 0 | 0 | 0 |\n", "|$\\overline{x1} \\lor x2 \\lor \\overline{x4}$| 0 | **1**| **1**| 0 | 0 | 0 | 0 | **1**|\n", "| $x1 \\lor \\overline{x1}$| **1**| **1**| 0 | 0 | 0 | 0 | 0 | 0 |\n", "| $x2 \\lor \\overline{x2}$| 0 | 0 | **1**| **1**| 0 | 0 | 0 | 0 |\n", "| $x3 \\lor \\overline{x3}$| 0 | 0 | 0 | 0 | **1**| **1**| 0 | 0 |\n", "| $x4 \\lor \\overline{x4}$| 0 | 0 | 0 | 0 | 0 | 0 | **1**| **1**|" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Теперь чтобы получить 2 покрывающих множества одно из них обязано содержать переменную а второе её отрицание. \n", "\n", "Если вдруг в одном множестве окажется и переменная и отрицание, то второе не сможет покрыть всё.\n", "\n", "Например пусть разбиение следующее $\\{x1, \\overline{x1}, x2, x3, x4\\}, \\{\\overline{x2}, \\overline{x3}, \\overline{x4}\\}$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "| closure| $x1$ | $\\overline{x1}$ | $x2$ | $x3$ | $x4$ | sum|\n", "|------------------------------------------|------|-----------------|------|------|------| --:|\n", "|$x1 \\lor \\overline{x2} \\lor x3$ | 1 | 0 | 0 | 1 | 0 |**2**|\n", "|$\\overline{x1} \\lor x2 \\lor \\overline{x4}$| 0 | 1 | 1 | 0 | 0 |**2**|\n", "| $x1 \\lor \\overline{x1}$| 1 | 1 | 0 | 0 | 0 |**2**|\n", "| $x2 \\lor \\overline{x2}$| 0 | 0 | 1 | 0 | 0 |**1**|\n", "| $x3 \\lor \\overline{x3}$| 0 | 0 | 0 | 1 | 0 |**1**|\n", "| $x4 \\lor \\overline{x4}$| 0 | 0 | 0 | 0 | 1 |**1**|\n", "\n", "\n", "| closure| $\\overline{x2}$ | $\\overline{x3}$ | $\\overline{x4}$ | sum|\n", "|------------------------------------------|-----------------|-----------------|-----------------| --:|\n", "|$x1 \\lor \\overline{x2} \\lor x3$ | **1**| 0 | 0 |**1**|\n", "|$\\overline{x1} \\lor x2 \\lor \\overline{x4}$| 0 | 0 | **1**|**1**|\n", "| $x1 \\lor \\overline{x1}$| 0 | 0 | 0 |**0**|\n", "| $x2 \\lor \\overline{x2}$| **1**| 0 | 0 |**1**|\n", "| $x3 \\lor \\overline{x3}$| 0 | **1**| 0 |**1**|\n", "| $x4 \\lor \\overline{x4}$| 0 | 0 | **1**|**1**|" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Как видно, второе множество не является покрывающим\n", "\n", "### Как найти второе решение\n", "У текущего подхода есть ещё одна проблема. В общем случае неверно, что если $(x1, x2, \\ldots)$ решение SAT то $(\\overline{x1}, \\overline{x2}, \\ldots)$ тоже решение.\n", "Но надо как то сделать так, чтобы отрицание было покрывающем множеством. Для этого введем новую переменную (назовем её $f$). И объявим её ложной. \n", "\n", "То есть сделаем ещё одно эквивалентное преобразование: $(x1 \\lor \\overline{x2} \\lor x3) \\Rightarrow (x1 \\lor \\overline{x2} \\lor x3 \\lor False) \\Rightarrow (x1 \\lor \\overline{x2} \\lor x3 \\lor f)$ при $f = False$\n", "Проделаем так с каждой **оригинальной** скобкой в КНФ: \n" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "| closure| $x1$ | $\\overline{x1}$ | $x2$ | $\\overline{x2}$ | $x3$ | $\\overline{x3}$ | $x4$ | $\\overline{x4}$ | f |\n", "|------------------------------------------|------|-----------------|------|-----------------|------|-----------------|------|-----------------|-----|\n", "|$x1 \\lor \\overline{x2} \\lor x3$ | **1**| 0 | 0 | **1**| **1**| 0 | 0 | 0 |**1**|\n", "|$\\overline{x1} \\lor x2 \\lor \\overline{x4}$| 0 | **1**| **1**| 0 | 0 | 0 | 0 | **1**|**1**|\n", "| $x1 \\lor \\overline{x1}$| **1**| **1**| 0 | 0 | 0 | 0 | 0 | 0 | 0 |\n", "| $x2 \\lor \\overline{x2}$| 0 | 0 | **1**| **1**| 0 | 0 | 0 | 0 | 0 |\n", "| $x3 \\lor \\overline{x3}$| 0 | 0 | 0 | 0 | **1**| **1**| 0 | 0 | 0 |\n", "| $x4 \\lor \\overline{x4}$| 0 | 0 | 0 | 0 | 0 | 0 | **1**| **1**| 0 |" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "### Итого: \n", "- Если нашлось разбиение на 2 множества, то ни одно из них не содержит одновременно переменную и её отрицание\n", "- Множество не содержащее $f$ является решением КНФ." ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "collapsed": false }, "outputs": [], "source": [ "cnf_vars = 5\n", "cnf_clauses = 20\n", "\n", "cnf3 = CNF(from_clauses=psc.rand3cnf(cnf_clauses, cnf_vars))\n", "clauses = cnf3.clauses" ] }, { "cell_type": "code", "execution_count": 15, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def solve_sat(cnf_vars, cnf_clauses, clauses):\n", " vectors = np.zeros((cnf_clauses + cnf_vars, 2*cnf_vars + 1))\n", " for i in range(cnf_clauses):\n", " for j in clauses[i]:\n", " vectors[i][j + cnf_vars] = 1\n", " vectors[i][cnf_vars] = 1 # Contradict\n", "\n", " for i in range(1, cnf_vars+1):\n", " vectors[cnf_clauses + i - 1][cnf_vars - i] = 1\n", " vectors[cnf_clauses + i - 1][cnf_vars + i] = 1 \n", " sol = solve_d_vectors(vectors, 2)\n", " return sol[0] == 2" ] }, { "cell_type": "code", "execution_count": 16, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "solve_sat(cnf_vars, cnf_clauses, clauses)" ] }, { "cell_type": "code", "execution_count": 17, "metadata": { "collapsed": false }, "outputs": [], "source": [ "cnf_vars = 5\n", "cnf_clauses = 1\n", "\n", "cnf3 = CNF(from_clauses=psc.rand3cnf(cnf_clauses, cnf_vars))\n", "clauses = cnf3.clauses" ] }, { "cell_type": "code", "execution_count": 18, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "[[-3, 2, 1]]" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "clauses" ] }, { "cell_type": "code", "execution_count": 19, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "solve_sat(cnf_vars, cnf_clauses, clauses)" ] }, { "cell_type": "code", "execution_count": 20, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def test_sat_iter(N, cnf_vars, cnf_clauses):\n", " mistakes = 0\n", " for _ in range(N):\n", " cnf3 = CNF(from_clauses=psc.rand3cnf(cnf_clauses, cnf_vars))\n", " clauses = cnf3.clauses\n", " sol_this = solve_sat(cnf_vars, cnf_clauses, clauses)\n", " py3sat_test_solver = Solver(bootstrap_with=cnf3)\n", " sol_other = py3sat_test_solver.solve()\n", " if sol_this != sol_other:\n", " mistakes += 1\n", " return mistakes" ] }, { "cell_type": "code", "execution_count": 21, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def stress_test():\n", " for i in range(100):\n", " if test_sat_iter(20, 4, 20) > 5:\n", " print(\"Failed\")\n", " return\n", " if i % 10 == 0:\n", " print(\"Passed \", i)" ] }, { "cell_type": "code", "execution_count": 22, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Passed 0\n", "Passed 10\n", "Passed 20\n", "Passed 30\n", "Passed 40\n", "Passed 50\n", "Passed 60\n", "Passed 70\n", "Passed 80\n", "Passed 90\n" ] } ], "source": [ "stress_test()" ] } ], "metadata": { "kernelspec": { "argv": [ "python", "-m", "ipykernel_launcher", "-f", "{connection_file}" ], "display_name": "Python 3 (ipykernel)", "env": {}, "language": "python", "metadata": { "debugger": true }, "name": "python3", "resource_dir": "/usr/local/share/jupyter/kernels/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.12.2" } }, "nbformat": 4, "nbformat_minor": 4 }