{ "cells": [ { "cell_type": "markdown", "id": "5e4d2601", "metadata": { "tags": [ "COP", "easy", "AllDifferent", "Increasing", "objVar", "symmetry-breaking", "academic" ] }, "source": [ "# Problem *Golomb Ruler*" ] }, { "cell_type": "markdown", "id": "e6407392", "metadata": {}, "source": [ "A Golomb ruler is defined as a set of $n$ integers $0 = a_1 < a_2 < ... < a_n$ such that the $n \\times (n-1)/2$ differences $a_j - a_i$, $1 \\leq i < j \\leq n$, are distinct. \n", "Such a ruler is said to contain $n$ marks (or ticks) and to be of length $a_n$. \n", "The objective is to find optimal rulers (i.e., rulers of minimum length). " ] }, { "attachments": { "golomb.png": { "image/png": "iVBORw0KGgoAAAANSUhEUgAABAAAAAInCAYAAAAGZCs3AAAABmJLR0QA/wD/AP+gvaeTAAAgAElEQVR4nOzdd7xsd13v/9dJJ51mqBJCh0DoTRFFBRRQsWFFES8WvHZB5KJeRUFFEVEUpYjXgp0qWMCooCIqCEgvoUhvCQkhpJzfHyvnl1NmZs/ee/asPXuez8djPZLMWvv7fc/ZJzPr+1nf9V0FAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABywb+wAV7pe9YDqztVtqhtVp1YnVZ+uLqj+p3pD9ZrqxdW7RknKXnT96jerB03Y91/V7ZcbBwD2tGtVb6yuPeOYF1cPXE4cgG07tfqihvHszaubNXzGnXzldll14ZXbxxrGsu+s3tEw3nhtdcnSUy/ZMdU3Vv9aXVHt3+T2X9UjqhOWHZw9Y1/1XdX5Tf979trR0gHA3vSHbXye96LR0gHM55SGscQrqkvb/Hj24O2S6tXVUxuKnycu8X0sxQMaKh7b+UM6sH2w+pblxmcPuHn1D23890sBAAAW50HNd36nAADsVtesntxwNX8R49lJ28XVS6pzlvSedsxJzVf13cr20oZfBsxyTPXohv+p5vl7pQAAAItxWvW+FACA1bSv+qHqk+3cwP/wbeEXuo9ZdIMzfG71gmZXMS6u/qI6t3p7w9TsU6qzqi+ovvbK/57kftW/VV9R/fdCErPX3KF65pX/BACW60kN6+4ArJrrVP+v+pIZx3ym+sfqldWbG2aqf6o6tjq9YTx81+q+DWve7WnXb/aU/8uqX62uvkE7J1ePb7hHYlpbH65uufB3wCo7oXpiW7s3xwwAANi+L25z379mAAC7xdnV+5v+efXW6rsbZrvP46jqyxsWuF/6DIBlOL1hpddpb+qC6v6bbPPzqo/OaPN91Q0WkJ3Vd++G/ym3Ou1GAQAAtuekNr/2kwIAsBvctWHV/kmfU5dWP1Edt8W2j6t+fUrbK10AeF7T39Al1Rdusd07VxfNaPsVLfcWB3aXU6vfavYTJv6h4bYRBQAA2Dm/2uYL8AoAwNhuUX28yZ9RH2u4RX0Rnjalj5UsAHx/sz/c//c22//WDdr/+W22z2p6ULMXGTq/4ZEd+5pdoFIAAIDtuUd1eQoAwGq5RvW2po8l7rLAvo6v3jKlr5UqAFy/YdGDWVfo9y2gn7+a0cel1W0W0Aer4drVc5t9QvGCDl2ASAEAAHbG8U2+DfSCNr49TwEAGNPzm/759NU70N/XT+lrpQoAf9zsD/bPW1A/t232NO+/X1A/7H7f1/S/Bx+qHjLhZxQAAGBnPL7J362PbHjikwIAsBs9tOmfTc/eoT6Pa/JaAytTADin2R/qL19wf3+5QX+zHtfA3jGtAPCchmk8kygAAMDi3b7JT9/5p4YZoOdO2KcAAIztWk2/7/+C6owd7HvSuGThBYCjFt3glR6zwf6nL7i/jdrbKA9707sbnjDxbQ3/IwMAO++Y6lkduRjzZ6rvbDipBdiNHtv0R9P/RsOs4p3ysoa1AA7ezt/B/hbmhtVlTa/oXtBwT9giHVV9YEaf+6s7LLhPdp8DMwAur57SfM/iNAMAABbrMU3+Tj34gsy5U44xAwAYyw0bCpWTPpMu7dB1xFbWTswAeGh19Iz9L214/N8iXVG9cINjvm3BfbI7vbFhfYkfaHhMJACwPLesfmrC66+pfmnJWQA244ebfqH6b6r/WWKWlfLmZld0H7ZD/X7VBv1+uCOnorG3nNWwgMZmmAEAAItxVPXKJl85O3wm5rkTjjMDABjLidUnmv6Z9NDxou1uZzf7w3x/ddMd6vtac/R9nx3qm9WlAAAAi/H9Tf4ufcKEY8+dcqwCADCG72j659EVDY8b3xMWfQvA/TfY/+Hq7Qvu84CPNiyUMMtG+QAA2Lwzq5+f8Ppbq/+73CgAm/bNM/a9ofrIsoLstEUXAO63wf6dvpr6XxvsVwAAAFi83+nIxXf3Vw9vWFQLYLe6evUFM/a/cllBlmGRBYCjqntscMzrF9jfJK/bYP/Z1Wk7nAEAYJ08vPqSCa//ZvWKJWcB2Kwvb/ZacXvqluBFFgBu1caPXXvzAvub5E0b7N9X3WmHMwAArIvrVk+a8Pp7qh9fchaArfjSDfZvdJF5pSyyAHDnOY551wL7m+S8OY6ZJycAABv7zer0Ca9/d/WpJWcB2IqNZrHv1Bp2o1hkAeA2cxxz3gL722r78+QEAGC2h1RfOeH1369esuQsAFtxzermM/Zf1B5aALBm3+uwWTeZ45j3L7C/ST5eXVIdP+OYs3Y4AwDAXnet6qkTXv9w9YNLzgKwVRvNDn/fBvuPr+5Z3bs6p+GR99dpuDX+uOri6sIr2zmvek31qob1US7Zaujd4rXNfp7rhUvK8d4Ncux0EYLV8rxm/33ZU4t+AMCC/EGTvzcfMufPnzvl5w9sL1psXICJfqDZn0XTFjK9dfVbDRegZ/38tO2C6g+re+3Ae1qajd78Tt//f8B/bJDjioZqDJQCAABs1gOb/J35/E20ce6UNhQAgGX6jWZ/Fh3+uXaD6rnV5Rv83Ga2f2njdQgWZlFrABzT8PzEWT65oL42slE/+xru9QAAYHNObbjqdbjzq+9ZchaA7brZBvsPHls+rPrvhplOi1xL7+7VKxsWVT1hge1OtKg1AOYZUC/rFoB5+rlW9YGdDgIAsMc8qbr+hNd/LLdZAqvnBhvs/0x1dPVr1fdOOeaS6m+qf2h47P1Hrnzt5OpG1e2rL2/2YvT7Gp6eco8rj931n6e3buOpDctaDXbaPWkHb1+4pCzsfm4BAID5fFGTvytfvoW2zp3SllsAgGX6aLM/i36jYcr/pH0XVT9TXWPOvu5Z/dMG/R24df7G235nO+wubfxG/mJJWX5njiwPWFIWdj8FAADY2IkNz8KedAI8z5OgDnfuhLYUAIBlOrphfbhZn0WfnvL6f1e32EKf+6pHz9Hvm5u/sLApi7p3YZ5F9S5fUF+L6GfWYwIBADjU45s80P/J6h1LzgKwCNdsGJDPcrUJr72hYfX+t2yhz/3VL1TfucFxt2iY2b5wiyoAzDOgvmxBfW1kngKApwAAAMzn7g2Pyjrcq6tfXXIWgEWZNLjfyIXVgxqegLcdz6p+eYNj7t8OLK66yKcAbGRZMwDmKTQoAAAAbOy46pkdec54afXwlnd+B7BoW5kV/vjqvAX1/5PV+zY45ufa+Gl7m7KoAsA8H/6LfFTCLEfPccyyZiMAAKyyxzUs9ny4J1SvX3IWgEXabAHg7dWTF9j/p6tHbXDM1RuesrIwixqUf3aOYxb1yMGNzFMAuGTHUwAArLZzGharOtx/N1yVAlhlx27y+Gc037h3M55bvXeDYx7RAtewW2YBYJ6B+SLMU2hY9C8OAGAvOabhHtXDT5CvaJj671wKWHWbmRW+v/qjHciwv/rjDY65ZvVVi+pwUQWAT89xzAkL6msj81RHLt7xFAAAq+tHqztOeP3XqlctOQvATthMIfNV1Xt2KMc8hYWvWFRniyoAzLMK4skL6msjp8xxzMd2PAUAwGq6RfVTE15/V/XYJWcB2CmbKQC8esdS1Gsani4wy/0W1dmiCgAfneOYZRUA5ulnnrwAAOtmX8N9rpNmbv6v5pv1CbAKNhp0H+y/dizFcBvAGzY45prVWYvobFEFgEva+A/w1AX1tZF5+jEDAADgSI+sPn/C68+qXrbkLAA76WMNg+95vG4ngzTfU1Vuv4iOFvlovo2eYXitBfY1y+dssP/jqV4DABzuRg2P9zvcB6ofWXIWgJ12efWJOY/9wE4Gqd42xzFnLqKjRRYA3rHB/tPb/KMWtuLaG+zfKCcAwDr67SbfSvnI6pNLzgKwDB+a87hP7WiKumCOY26wiI7meWTevN45xzHXaePnHG7HydVJGxwzT04AgHXypdV9J7z+keqcK7dFOnOD/TevfnoT7b2n4TYFgM14V3WrOY7b6QLAPO0v5Jb6RRYA3jTHMWe2swWAM+c45s072D8AwCo6bcrr127yEwF22s022e8rUwAANm+eqfefqa7Y4RzzzAA4cREdLfIWgP+Y45gbL7C/Sc6c45h/3+EMAAAA7H5vneOY4xuekLKT5ikwLCTDIgsA/1VdusExN19gf1ttXwEAAACA/5zjmH1tfJv5dp0yxzELWch+kQWAS9r4D/DsBfY3ye022P/u6oM7nAEAAIDd7zXVZ+c4bp4B+nbMc3//PLcJbGiRBYCqv9lg/6IXkDncRgWAl+5w/wAAq+jPGq5yLWv7hw3yvHiT7X3+tt49sK4uaSgCbOT0Hc4xT4HhPYvoaNEFgL/eYP+ZDU8C2AknpwAAAADA/DYaw1bdcocznDnHMQt5mt2iCwD/2sbPUrzXgvs84O7V0TP2X1T93Q71DQAAwOp58RzH3HaHM2x0IbvmW3R/Q4suAFxe/cEGx0x6xuwi3H+D/X9ZXbhDfQMAALB6Xt3Gj6rf6bXsNiowvO/KbdsWXQCoes4G+x+0Q/1+5Qb7N8oFAADAetlfPXuDY76gnRnDVt2susYGx7xwUZ3txJt4XXXujP1nVPdZcJ93rm46Y/8bqpctuE8AAABW3zOrK2bsP6O69w71/ZA5jvnTRXW2U1WMJ2yw/xEL7u+7Ntj/xIbKDgAAABzsPdVzNzjm63eo72/YYP8bm32Bfdd4RcOge9J2WcNUh0W4fnXxjL7e1OzFAVlvz2v635391WvHiwYAe9a5zf7+fdFoyYB1dfOGceq0z6ULGmYCLNK9Z/R3YHvYgvvcMbdv9h/gHy+on9+e0cf+6osX1A97kwIAACzfuSkAALvPrzf7s+m3F9jXUQ1jjVn9/Wc7N2t/Rzy52W/oQdts/94N92pMa/8Pt9k+e58CAAAs37kpAAC7zykNtwPMmsl+lwX19cgZ/eyvLq3utqC+lub4hqrFtDf1kWYv3jfLDRoehTCt7XdUp20jO+tBAQAAlu/cFACA3ek+zZ7J/u6G29C34/Orz8zoY3/1qG32MZqbVB9r+ht7Z3WLTbb5udV/z2jzoupOC8jO3qcAAADLd24KAMDu9YPN/ox6e3XLLbb9ZdWnNmj/GdvIPtO+nWr4MHdueAzfqVP2f7L64ep3G97wLF9XPbXpCzB8tuHWgr/ZdEr2iq9uWMRjHt9a3XrG/g9UvzZnWx9q42eIAsBe9n3VyXMc94jqxjP2v7l6zhztfKJ6+hzHAWzWLzT7KvyF1U83rBtwyRztXfvK47+n2ePwP6i+rbp8npC72T2qDze70vHm6tEN9zpcozqmunp1x4YqzEaLJHyqesCy3hC71kZX9XdqM1sAgHX3wZb73fv25bwtYE09rtlrzu1vGOM+peEi9I2rExsW7julOrv6loa16WY9ue7A9vMt7yL9Utyoek078wXwjuq2y3sr7GIKAAAwDgUAYK95YLNvaV/E9oHq/st6Q8t2bPUT1adbzB/WpdUvNVRaoBQAAGAsCgDAXnTd6pkN0/IX+Rn26eoJTb9Vfk+5XvXEhnu3tvKHdVHD/RY3WXZwdj0FAAAYhwIAsJfdunpadUHb++x6c/Xj1TWXG3933F9wfPVFDffu37nhD3VSBeSi6k0NtxD8VcMif59eUkYAAACoYfb5vasvre7S8FS7a0859sKGRwe+tvq3hnHsm5eQcaLdUACY5PSGIsCJDYslfKqrZgoAAADAbnJydVp1UsM4++KGmQKfHDMUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAADsdvvGDnCY+1R3mbH/L6u3LikL6+Go6sdm7P9E9dtLygIAe8k51f1n7P/H6l+WlAVgp9y8evCM/a+uXr6kLCvnl6v9M7avHi8ae9Qxzf4797bxogHASntEs79jf2K8aAAL89XN/qz75fGiHemosQMAAAAAO08BAAAAANaAAgAAAACsAQUAAAAAWAMKAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANaAAgAAAACsAQUAAAAAWAMKAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANaAAgAAAACsAQUAAAAAWAMKAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANaAAgAAAACsAQUAAAAAWAMKAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANbAMWMH2KQ/HzsAa+em1f6xQwDAHvRzV24ALIkZAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANbAbnsM4Merd44dAgAAABbg42MHAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA2AH7xg7AQt24ekZ1n8Nev1n19uXHAQCAHXPD6m5XbnesrlNd48rts9UnrtzeW72q+tfqn6uLxggLsChHVT9QXVjtn7DddLxoAACwMDeqHlX9Z5PPezfazq+eWt1q2cEBFuEW1Sub/UGnAAAAwCq7V/WS6oq2NvA/fLuiekp14jLfBMBWHV09urq4jT/gFAAAAFhFt6le0exz3X+pHld9aXXbhlsDblV9YfXY6t9m/Oxbq9st680AbMVtq39v/gqnAgAAAKvoO5t+jvu6hvv/5/GA6j1T2vl4dfuFpgZYgGOrn25Y1OTwD66/nPCaAgAAAKtsWgHgRdUJm2zreg1Fg0ntvbdh8UCAXeHOTf7Aen/1ldXJE/YpAAAAsMomFQD+uzppi+3dpLpgQpv7q2dvNyzAInx+dVlHfkg9qzr9ymMUAAAA2GsmFQC+bJtt/siENvdXlzcssA0wqq/q0A+n86r7HnaMAgAAAHvN4QWANy6gzVObPgvgFxfQPuxaR40dgE3ZXz2tOrv6m5GzAADAsv35Atq4oPr7KfseuID2YddSAFgdb2t4lMkjqwvHjQIAAKP4lwW188opr9+qYWYt7EnHjB2AubyqOqe6eOwgAACwRBdV/3PQf79hQe2+e8a+sxoW3wbYtawBAAAA87lv08+d7zViLthRbgEAAADWzeUz9l22tBSwZAoAAADAujltxr4PLS0FLJkCAAAAsG6uP+X1j1fvWmYQWCYFAAAAYN3cdsrr5zasAwB7kgIAAACwbu4+5fX/t9QUAFvkKQAAALCxM5t8zvy+PCadPc4MAAAAYJ18w5TXH58nAAArwgwAAACY7ZjqvR15vvyW6tgRcwFsigIAAADM9vCOPFe+orr3mKEANksBAAAApju1+mBHnis/bcxQAFuhAAAAANM9rSPPk/+rOmHMUABboQAAAACTPbAjz5HPr24+ZiiArVIAAACAI31u9eEOPT++tLrfmKEAtkMBAAAADnVywzT/w8+Pv3vMUADbpQAAAABXObp6QUeeG//kmKEAFkEBAAAABvuq3+vI8+JfGjMUwKIoAAAAwOCpHXlO/JRREwEskAIAAADUkzvyfPjJoyYCWDAFAAAA1t2v5Mo/sAYUAAAAWGe/3JHnwb82aiKAHaIAAADAunpSR54D//qoiQB2kAIAAADr6Bc78vz3aaMmAthhCgAAAKybX+jIc9/fbHgMIMCepQAAAMA6eWJHnvc+va0N/h9TPe/K7dmLCgiwUxQAAABYF0/oyHPe327rV/6fd1A7H1xEQICdpAAAAMA6+PmOPN99Rtub9q8AAKwUBQAAAPa6n+vIc91ntv17/hUAgJWiAAAAwF72+I48z312ddQC2lYAAFaKAgAAAHvVz3TkOe5zWszgvxQAgBWjAAAAwF70f5t+nrsTmwIAsOspAAAAsNc8quUO/hUA2NMWNWWGnTdrgL+/+tSMn33bBj+rQAAAwG50n7EDwF6iAHCkz62OHjsEVd2gOnbsEADAyrpedfzYIYBRHN0wtuMgCgBXOalhwHlxdfnIWRh8qDqrOm3sIADASjm2YfB/dHXJyFmAcVzeMLa7fsNYj7b/vMy94OTqkQ3V4Z8ZOcssR1dftkNtv7z69A61vQhfUn1D9YTqHSNnAQB2r2Orh1Z3bji/u2LcOCzAtaoTltzn5dUHltwnO+v/VhdVT6suHDkLI7l69cTqgoYrzSeOG4cN/FHDh/ELqzuMnAUA2F2uVj264Zzukkz7BQ51UsPnwwUNY8CrjxuHZTqlekz1ka5aBO9xoyZiHnfoqt/XpdXvZvFCAFh3x1X/q3pXV50n/P6oiYDd6qe76nPiI9WPN4wN2aOu0VDt+VSHroB/RXXmeLHYhNd16O/OjAAAWE8HX/E//OlG9x0xF7B7ndnkJ6k9sWGsyB5xavXY6qNNfgTea8aLxiY9vsm/w0ur51Q3Hy8aALAEx1XfVZ3X5HOCT155DMAkr2/yZ8dHG8aMZgSssDOqp3TkFf/Dt18ZKyCb9iXN/l1e0TAj4I5jBQQAdsSJDVf8P9zsc4EXjxUQWAm/1uzPkE81jCHPGCsgmzfvwP/A9pBxYrIFp1SXtfHv9EAh4E7jxAQAFmTegf+B7SfHiQmsiG9qvs8ShYAVcFrDh/7Hm++XemA7e4ywbNl5zf+7vaxhIaBbjhEUANiy46vvrd7T5s7rvmaMsMDKOKfNfaZ8vGHB+NPGCMtk12mozlzY5n6ZB7aTlx+Zbfj7Nv87PjAj4M4j5AUA5ndqw0rdBz+taTOb2X/ALKe2tc+WCxvGnNdZfuTF2jd2gG04vfqN6qsapodtxUXVDy8sEcvwsOruW/zZ/dW/Vw9vWAAEANgdTqieUH1b23s+9482TN0FmOZXG54kshWfrp5XPbJh0dGVs4oFgOs2PLPx4dVJI2dhdf1d9ZiGggAAMI5TGy7GPLK61shZAOZ1UfXMhsLlB0fOsimrVAAw8Gcn/F31E9Wrxw4CAGvktOqHMvAHVtuBQsATqw+MnGUuq1IAOKF6bvWVYwdhT3pn9YDqzWMHAYA1cFTDY5j/95X/DrDqnld9Y/WZsYNsZFU+dD/TcK//7as/bbiXG7brLdXXVzfL4B8AluWK6germ1a/3fDUHoBVs79hbHr76sGtwOB/lZ1T/UlbW8HRZntr9XWtTgEMAPayG1dPry5v/HMEm81mm2f7k4Yx6cpZlVsApvnq6lHV3bb48xdVt1tcHJbgKdUDt/iz/1M9rWHaoQodAOwu92pYoPd+bb1If8/qQwtLBOw1+xqeBrbVpwC8qvqF6i8XlogtOTAj4Io2X72x8Mxq+Zc2/zt+c674A8CqODAj4NI2/53/eSPkBVbHGW3+c+WKVviK/1537+rcNvcLvdMYQdmyDzT/7/a86hHVcWMEBQC25bbVn7W5WwO+aZSkwKq4a5sbK/59wxiTXe7u1Qubb0bAI0bKyOZdP1f8AWDdbGZGwJNGygishu/JFf89bZ5CwDNHS8dmfU0G/gCwruYpBLxitHTAKnhOswf+L2wYQ7LivrDptwa8c7RUbNZTm/w7fHf1XZnqDwDr4HYNtwZMusDzmerU8aIBu9i+hnHDpPHEuQ1jRvaYAzMCDv+F32XMUMzlqOqDHfp7e0uu+APAupo2I+BbxgwF7Fp3zxX/tfVF1T901S//18eNwxzu36FX/L87V/wBgGFGwJ931YyAvx03DrBLPS1X/NfegULAxdX1Rs7CdPuqV2bgDwBMd05XFQLuOXIWYHe5QcMtQv/QMAZkzd29+pHq6LGDMNGDMtUfAJjPWdWPVSeOHQTYFY6ufjRT/Zng+nncw25yversDPwBgM27ZnW3hpmEwHo6JzO92cAxmQmwWxw/dgAAYKXty62DsK6ObhjbAQAAAAAAAAAAAAAAAAAAAOw6VkUFYLe7acNK3re5crtJdfXqtIbFvS6ozq8+Ur22+o/q3OptI2QFAAAA5nRS9ZDqWdW7q/1b3F5RfVseJQoAAAC7ygOqP64uauuD/knbq6rbL/F9AADsSm4BAGC3OK+60Yz9r6v+vGFA/z8N0/5PrK5V3aW6f3W/KT97SfU11YsXlBUAAADYovOafAX/PU0f2B/udtVrprRzSXXfhSYGAAAANu28jhy0v7G65ibbuVr19xPa2l+9tzp5MXEBAACArTivQwfrn67O2mJb1254KsCkIsDPbzcoAAAAsHXndehA/QnbbO+xTb+lAAAAABjJeR06UL/JNts7q8kFgP3VnbbZNgDAyvFsZAB2o7dU79hmG++s3j9l36222TYAwMpRAABgN3r9gtp535TXr7ug9gEAVsYxYwcAgCt9fld9L12woDY/OeV1TwIAANaOAgAAu8W0q/XbccqU1z+2A30BAOxqbgEAYC+79pTXz1tmCAAAAGDnXLO6vCOfAHB5dfqIuQAARmEGAAB71X2b/D33101fGwAAAABYIUdVr+vIq//7q3uOmAsAAABYoMc0efD/a2OGAgAAABZjX/VDTR78v6Q6brxoAAAAwCJ8QfXyJg/+n1kdO140AIDx7Rs7AABswu0bvrtOrk6rblTdsbp3dZMJx7+l+sHqpcsKCAAAAGzPMU2+un/49vHqT6ovS6EbAOD/d8zYAQBggc6v/qj61+r1DQUBAAAAYIXMOwPgwHZ59bLqGzMTAAAAAFbWSdUNqjtX39cw7f+SJhcDXl3dbZyYAAAAwKJdt3pydUVHFgE+W337aMkAAACAhfvyhvUAJs0G+L4RcwEAAAAL9qAmzwS4tPq8EXMBAAAAC/bUJs8CeGt19Ii5AAAAgAW6YcO9/5OKAN80Yi4AAABgwV7U5ALAy8cMBQCwbEeNHQAAdtg/Tnn9ntXVlhkEAGBMCgAA7HWvnvL68dUdlhkEAGBMCgAA7HUfnbHvjKWlAAAYmQIAAHvdx2fsu+bSUgAAjEwBAIC97tixAwAA7IaZxXwAABkUSURBVAYKAACM7ZyGafoHti9fcPvXmrHvkwvuCwBg11IAAGBsxzZMxT+w3WrB7d9sxr53LrgvAIBdSwEAgN3mrgtu7z5TXr+4esOC+wIAAACmuHO1/6DtwupqC2r7xOrDh7V/YHvhgvoAAFgJZgAAsNucVH3fgtp6ZHXtKfuetaA+AAAAgDkcPgNgf3VBddNttnuH6tMT2t5f/Ue1b5vtAwAAAJswqQCwv3pXdeYW27xd9d4p7X6m4ckDAAAAwBJNKwDsr86vvrs6bs62jm+4feCiKe1dVn39ArMDAAAAc7pj0wsAB7YPV79WPaS6RcPjAo+tTqluXD2g+uXqf2a08YnqK5b0ngAAAIAJ7lk9p+HRfBsVA7ay/VF1xtLeDQAAwAQ3q64zdgjYJa5efVf1/OpTbW/Q/4nq6dXdlvoOYPc7trpLdfTYQQBYLisgw3hOaljg7L0NK54Dhzqu+ryG1fzPrm5TfW51WnW1g477bEOx4KPV66vXVP9Znduw4B9wpH3V51y5vX7kLAAAe9bJ1aOqV1WnjpwFVtUx1enVCWMHgRX3mIYZN3ccOwgAwF5y9eqJDVf791ffMm4cAOjYhkdu7q9eUd1n3DgAAKvtlIYrLB/pqnuT399wBRMAxvborvp+uqJ6QcPjOQEAmNM1Gq74T1rI7Ckj5gKAg92oYeB/+HfVK6ovHjEXAMCud0r12IYFyaatTv6lo6UDgCO9vunfWS+q7jpeNACA3eeMhiv7Gz267NKGJwAAwG7xtDZ+tOYrqi8ZKyAAwG5wavV/qo8137PJPW4JgN3mYc33Hba/+qvq7uPEBAAYx3Wa74r/4dufjhEWAGa4e5v7LjswI+BBY4QFAFiWAwP/C9v8ydL+6heXHxkAZjqjrX2nKQQArJB9YweAFXJ69dPV9zY8N3mrXlu9bRGBAGCBvrbtnRu+pfqO6p8XEweARVMAgI1dp3pM9fAs3gcAG/nnhsfgvnDsIAAcSgEAprtu9eMZ+APAVigEAOwyR40dAHax61Q3zeAfALbixtVZ1TFjBwFgYAYAbOw21aOrb07RDAA28o7qZ6o/qi4dOQsAB1EAgPndtXpSda9ttvOx6vztxwGAhbpx2zs3/HT12Orp1cULSQQAMLKzq9+rLm9rj0v6ueVHBoCZrtnWHwP49uqhbe8JOQAAu9pWCwF/MEZYAJjhThn4AwBs6G7VXzX/CdO/jBMTAKb62ub/HvtA9UPV1UZJCgCwC8w7I+Di6riRMgLAJL+UK/4AAJs2z4yAO4+WDgCO9A9tfMX/xNHSAQDscmdXf1Jd0ZEnUz8zYi4AONjnVJd15HfVOxqu+Ju1BgAwp7tXL+nQk6o3jpoIAK7y8A79jvpg9cO54g8AsGWHzwh4wLhxAKCjGorSrvgDAOyAu1cvrf61OnrkLACst2/IFX8AgB13j+qeY4cAYG2dWH1bBv4AAEuxr7pLdZ2xgwCwNo6t7lpdfewgAAAAAAAAAAAAAAAAAAAAAAAAAAAAALCj7lPtn7LdcsRcAAAAwIKcUL0tBQAAAHbIUWMHAKCqn6puOnYIAAAAYOfcrrq06Vf/zQAAAACAFXdU9W/NHvwrAAAAAMCK+8E2HvwrAAAAAMAKu1F1YVcN8q9IAQAAgB1iEUCA8fxmddJB//2MsYIAAAAAO+MbO/QK/weq0zMDAAAAAPaMa1Qf6tAB/tdfuU8BAAAAAPaIZ3fo4P6FB+1TAAAAAIA94Is7dGD/qepzD9qvAAAAAAAr7mrV2zt0YP+Dhx2jAAAAAAAr7okdOqh/dXX0YccoAAAAAMAKO6e6tKsG9JdVd5hwnAIAAAAArKijG672Hzyg/6UpxyoAAAAAwIr6oQ4dzL+zOnHKsQoAAAAAsIJuVF3YoYP5+804XgEAAAAAVtBLOnQg/wcbHK8AAAAAACvmmzp0EP+x6tob/IwCAAAAAKyQa1Yf7tBB/MPm+DkFAAAAAFghv9uhA/iXz/lzCgAAAACwIr6kQwfvF1c3m/NnFQAAAABgBVytenuHDt4fu4mfVwAAAACAFfALHTpwf3117CZ+XgEAAAAAdrnbV5d21aD98uoem2xDAQAAAAB2saOrV3fooP03ttCOAgAAAADsYj/coQP291WnbqEdBQAAAADYpc6sLuzQAfuDt9iWAgAAAADsUi/p0MH6X26jLQUAAAAA2IW+uUMH6udX199GewoAAADsiGPGDgCwwo6vnnzYay9r8yv/z+O+1dkz9l9SvXAH+gUAAIC1d3rTr9gve/voDr9XAABW3FFjBwAAAAB2ngIAAAAAAMCSWQQQAIAdYQYAAAAArAEFAAAAAFgDCgAAAACwBhQAAAAAYA0oAAAAAMAaUAAAAACANaAAAAAAAGtAAQAAAAAAYMG+s9q/4O2JS30HAACsJDMAAAAAYA0oABzqutWdqqPHDgIAsEOOre5aXXPsIAAs176xA+wS16m+snpmddnIWYC97YbVOQtu8+3VmxfcJrD3Xa16WPXc6uMjZwGAHXed6leqi6q7j5wFAGDZvqI6v/rZ6hojZwGAHXFW9XvVZxsW0Hr+uHEAAEbzTw3nQxdVT2m4JRIAVt4ZXXXF/+AVtO8/ZigAgBF9a4eeF5kRAMBKO3DF/5KOfHzWh7LoHwCwvk6pPt2R50hmBACwUs6ofrkjr/gfvP3RaOkAAHaHlzX9XOn86meqq4+WDgBmmHXF//Dt+0fKCACwW/xsG58zmREAwK4yzxX/w7fPGyUpAMDu8eDmP3f6ZGYEADCiG1RPb74r/odv1xkhLwDAbnK7Nn8OdWFmBACwRNsZ+O9vWPBm39JTAwDsLqe2tXMphQCAFbKqg9/PqR5V/WDbW8H/ioaFbQAA1t12p/R/tnpi9avVJ7YfB4BFW7UCwA2qx1XfXh03bhQAACa4qHpm9YTqgyNnAeAgq1IAOKFhddrvqU4aOQsAABs7v3py9XPVZSNnAaDtTZ9fpsuqD1TXqG7b6hQuAADW0WXV71e/UX185CwAXGkVB9JnN9z//83VUSNnAQDgKpdVz2pYC+BdI2cB4DCrWAA44G7VMxoKAlv16eqpi4kDALCy9lU/1vbODf+t+s7q9QtJBAATnF39XnV5m39szRUN6wsAAKyzG7a1RwBe2vBI5hsvPzIA6+zs6k8aBvWb+eK6xRhhAQB2kXtl4A/ACrp79ZLm/wL7inFiAgDsGt/Z/LMn/7y63TgxAWCyeWcEPGGsgAAAu8Qzm++K/1ljBQSAeWw0I+Dc0ZIBAOwOb2r2Ff9zxosGAJt32ybPCLi8uu6IuQAAxnTrXPEHYI+6R/XSDv2S++5REwEAjOdxHXrF/y9yxR+APebgGQHvro4bNw4AwNKdUn20uixX/AFYAwdmBHz/2EEAAJbs8bniD8AaumN19bFDAAAswb7q2g0zIgFgLR1d3aI6auwgAAA75Jjqlg1FAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA2zeNfAIB1dvXqpB1s/+LqYzvYPgAAADCHZ1T7d3B73vLeCgDMdtTYAQAAAICdpwAAAAAAa0ABAAAAANaAAgAAAACsgWPGDgAAsEv8QfUtY4cAgJ1iBgAAAACsAQUAAAAAWAMKAAAAALAGFAAAAABgDSgAAAAAwBpQAAAAAIA1oAAAAAAAa0ABAAAAANaAAgAAAACsgWPGDgAAsAL2VadUx1UXVxeNGwcANk8BAADgSPeoHlzdqbptda2GIsABn6neU72u+ufqxdVbl5wRAAAAmNMzqv1Xbr9ffW3DQH7/FrZ/rr5mufEBAACAeRxcAPhsWxv4H769srr5Mt8EAMzDIoAAAINjD/r3K6p/qn6gumt1w+r46trVbapvr/60oWhwuHtW/1l95Q5mBQAAADbh4BkAB7a/q24158/ftPqrCW3sry6vvm7BeQEAAIAtOLwA8PgOXexvHvuq32pyEeCS6i6LCgsAAABszcEFgMdvs63nNbkI8PbqhG22DQAAAGzD1arTr9y263rVJ5tcBPjxBbQPAAAA7BK/2OQCwIcaFhEEAAAA9oBbNv3xgA8eMRcAAACwYG9ucgHg2WOGAoCjxg4AALDH/OeU1++51BQAcBgFAACAxXrtlNdvlnUAABiRAgAAwGJ9ZMrr+6obLDMIABxMAQAAYLHOn7HvtKWlAIDDKAAAACzWp2fscwsAAKNRAAAAWKyTZ+z7zNJSAMBhFAAAABZr1jT/TywtBQAc5pixAwAAjOBaXXWl/rPV+xfY9hlTXr+i+p8F9gMAAABs4Per/VduH1pw2392UNsHb/+94H4AYFPcAgAArLvPqU5aYHt3mvL6KxbYBwBsmgIAAEB93oLauXN15pR9L1hQHwCwJQoAAAD1VQtq52FTXn9f9dcL6gMAAACY08FrAOyvLqquu802b97wmL9J9///wDbbBgAAALbg8ALA/upPttHeMdU/Tmhzf/WG6tjthAUAAAC2ZlIBYH/1S9W+TbZ1XPWXU9q7qDp7MZEBAACAzZpWANhf/W11yznbuVv1b1Pa+Ux134WmBoBtOGbsAEBVp1Xnjx0CYI1cMmPfl1RvbCgE/E316upDDZ/TpzU8NvAu1VdUX9DkGQMfrr66euXiIgOwCUdXJzTMxALYFY5vOIk8cewgAGvmmIYB+kurK5o+G2Ar23MbigQAjOuW1fXb/K1dAAt1VvU71TljBwGgM6sfrl7WMDNgK4P+T1f/r7rjcqMDMIefrR6RGfDAkp1R/XLDVKRfHzkLAEc6pbpf9aiGAf2/V++qPl5d1lAg+HjDLQJ/VT2xemBmcgHsZmc0FGpf2zD7y4wAYEcdPPDfX13acMUJAADYeb/RVbO2Xls9OIUAYMHOqn6vI6eU/tWYoQAAYM3cviNv33pHw60BR4+YC9gDDr/if/j28PGiAQDAWnpHk8/NzQgAtuQG1dPbeBGpG40VEAAA1tTTm32ObkYAMJd5B/77qw+MlBEAANbZdzTfk13eWD00hQDgMJ9TPanpU/0nbX89SlIAAFhvd25zj3h9TfVVuTUA1t5mrvgfvv3WCHkBAGDdXbPNn7vvqRkBKhmwOTepnlA9qDphi208q/qjhSUCAADm9YLqalv82XdUT6ue3FAYWDkKADCfG1SPqx5WHTtyFgAAYDxvqp5Y/UF1+chZNkUBAGY7MPD/9uq4caMAAAC7yMoVAhQAYLr7VM+vTh47CAAAsGu9pPrq6jNjB9nIUWMHgF3s5dXtqt+uLhs5CwAAsLu8o/q26itbgcF/mQEA87px9ePVw9sDq38CAABb9vbqZxsW9r505CybogAAm3P3hvt8vqCt///jKQAAADCO51cnbvFnP9ZwLv9T1cULSwTsemdWT2+o+G32OaK/tfy4AACw9q7Z5s/d91dvqx6ap4HB2rt1w9X8y5v/A+QloyQFAID1dsc2N/B/X/V91QljhAV2rzMbZgR8to0/SD40TkQAAFhr39F8A/+35oo/MIcbVU9pWAV01ofKjcYKCAAAa+rpzT5Hf0sG/sAW3LL6/YbHB076cPnW8aIBAMBaelOTz83fU31vdfx40YC9YNqMgBeMGQoAANbMbZt8xf/rqqNGzAXsQTevfq+rZgRcXJ0xaiIAAFgfT+iqgf+7q++qjhs1EbDnHVwI+IWRswAAwDq4RnV+dV4G/sAIPrd6UnWHsYMAAMAe97OZ6g/sAidX51THjB0EAAD2mBtW18+q/sAuckx1rbFDAADAHnJ0de2xQwAAAAAAAAAAAAAAAAAAAABMsm/sAADAUuyr7lR96ZX/vEV1nYankRxTXVhdUL2nemf1pupV1b9XnxohLwAAALAJp1aPaRjU79/Cdnn1r9X/qW695OwAAADAHP5X9eG2NvCftL10ufEBgEU6ZuwAAMDCnVY9u3rwYa/vr15evbh6bfW+6uLqlOrM6vOrh1Y3WFZQAAAAYGuuVf1nR169f1F18zl+/pjqcQ1T/80AAAAAgF3opCYP/n90C209fEI7CgAAAACwC/xZRw7aH7WN9p6XAgAAAADsKg9r8rT/7bhXCgAAAACwa1yr+kSHDtYvqc7aZrv7qk+mAAAAe4KnAADA6ntMdfphr/1h9c5ttru/+pHqulf+9zu22R4AAACwRddueJTf4dP/7zZmKAAAAGCxHtWRg//zxgwEAAAALN5bO7IA8DujJgIAdqWjxg4AAGzZbaqbTXj9n5YdBADY/RQAAGB1fcWU11+z1BQAAADAjnppR07/v7w6dsxQAAAAwOLsqz7RkQWA944ZCgDYvY4ZOwAAsCVnVadPeP19E147uvri6n7VXaqbVFevjmt4hOCHq3dWr67+tvrHhpkEAAAAwMi+rCOv/u+vXnTQMcdV399QFJh07LTt/dVjqhOX8D4AAACAGb6/yYP3379y/+2q1085Zt7tPdV9lvJuAIAd5ykAALCarj/l9c9UD6r+uTr7oNcvqJ5TfW115+pG1e2rB1ZPa7gN4HA3bLgl4H8vJjIAAACwWc9q8lX711efPey151afs0F7pzQUAqbNBnj4wt8BAAAAsKEXNN80/qdsst1HT2nn4oYZAwAAAMAS/W0bD/7/tuFxgZv1u1Pae1t17DZzAwAAAJvwj80e/F9a3WqLbZ/RsGbApHYftq3UAAAAwKb8c7MLAM/fZvu/MqXdN7W1WQUAAADAFvxTswsAD9lm+3ed0fY9t9k2ADACjwEEgNV0yQb7X7bN9v+t+siUfffeZtsAwAgUAABgNV04Y98Hqo8uoI/XT3n9CxbQNgCwZAoAALCaPjZj35sX1Me0AsA5C2ofAFgiBQAAWE0fnrHvkwvqY9osgmsuqH0AYIkUAABgNZ03Y98FC+pjWjvHVScvqA8AYEkUAABgNb19xr7LFtTHRTP2nbagPgCAJVEAAIDVNO3+/Frc1fkTZ+z77IL6AACWRAEAAFbTh5t+G8ApC+pjWjv7W9xtBgDAkigAAMDq+scpr19vQe1PW+zvQ9UlC+oDAFgSBQAAWF0vmfL6LaujF9D+2VNe/68FtA0AAADM6dSGhfr2T9huvYD23z+l7f+zgLYBAACATXhOkwfpj95mu+dMaXd/ddtttg0AAABs0h2aPEj/j222+/NT2v3XbbYLAAAAbNFfNHmwfv8ttnd69ZEpbT5ou2EBAACArTmzurAjB+tvqI7fQntPmdDW/qYvOggAAAAsyXc2edD+x9W+TbTzHVPa+UB1nQXmBQAAALboqU0evD+/OmODnz22/r/27ifU0rqO4/h7vDWouyKdwVFq7ogO1mKc2Si4CKlVm4hct2olKEaCIKKukoJALbDEUWgRtBAq2kS7aNGiFu0kCFq4URDaNOOdfy6eucyfe8c5586953fPmdcLHg538cDn3Gf1+f2+5/f0UnV+m/v/13TWAAAAALAPHKh+2faLAJ9Uv6i+Wd1fHazuqU5WL1Yf3OC+D6sTC/wOAAAAwIx+2PZnAsx7vd+0SAAAsHIONL3beG10EAC4RUeqt6szzVf6L1Z/rp5cfGQA2DVr1Tea7xycleefccWRy58fVxsjgwDALvpy9d3q202j/OtN4/+bzlb/rf5V/bX6w+W/AWDZHay+0tR7PxychX3iq9Wvqh+PDgIAC3J39aXLnwCw6l6o3mrqftymjle/qy5U/2k6/RgAAIDV8sWmznehqQM+PDYOi3S06TeRG135veOzQxMBAACwl57rSv/bqH5dfW1kIPbW1Tv+Vx92dL6bvxsZAACA5XWorV1wcyLg+MBc7LL16p2u3fG/+vrbuGgAAAAsyN/bvhNuNHXG9XHRuFUnqj+2dZXn+usnowICAACwMD/t87vhhaYOeWJUQOb3YPVuda7Z3nf8vTExAQAAWKCnmq0jnqtOV8fGxGQWjzbbjv/1lxMgAQAAVt8jzdcVNycCHh0Rlu2dbHooF5vvYV66fM+di48MAADAgt3dznrjyiwEHBgd4BY8VL1XPdbOv8f/qzd3KxAAAAD72rPtfBP4YtNBgj+o/r1riRZoGRcATlavVt9pOfMDAACwvC5Vf6perv45OMtclqlAn6peSfEHAABgvM2FgFeqf4yNMpu10QFmdGf1UvX9liczAAAAq+tAdbSpo/6lOj82zs0t2076vdWPqmequwZnAQAA4PZ0pnqj+nn10eAsM1u2BYBNmwsBz1d3DM4CAADA7eFi9bOWrPivivXqnWqj+V/lcKnpLQDLuggCAADA7O6ozraz7rjR1D2PLjw1WxyqXmsaw5j3QR4ekBcAAIDFOtLONo1fa5pCZ59Zr04330TA40OSAgAAsEhPNP+O//qQpMzl/ur1ZpsIeGZQRgAAABbnuW7eD8807fgfGpSRW7A5EXCuGz/g3wxLBwAAwKL8ts/f8T+dHf+V8EA3ngj4uPrCuGgAAADssYPVJ22/4/960xQ5K+ZY9W5bJwKeHBkKAACAPfWtru2A57Ljf9u4fiLg/bFxAAAA2EO/79od/wfGxmGEzYmAs9XxwVkAAADYfV+vPm3qfscGZ2EfOFY9Xa2NDgIAAMCuWWt685vizxb3VaeyEAAAALDM1pq63eHRQQAAAAAAAAAAdtdnAGQrKKVCGxYAAAAASUVORK5CYII=" } }, "cell_type": "markdown", "id": "e408e0f7", "metadata": {}, "source": [ "An optimal Golomb ruler with 4 ticks. Image from [commons.wikimedia.org](https://commons.wikimedia.org/wiki/File:Golomb_Ruler-4.svg) \n", "" ] }, { "cell_type": "markdown", "id": "597fb726", "metadata": {}, "source": [ "This problem (and its variants) is said to have many practical applications including sensor placements for x-ray crystallography and radio astronomy. " ] }, { "cell_type": "markdown", "id": "8486fb03", "metadata": {}, "source": [ "Dimitromanolakis has computed relatively short Golomb rulers\n", "and thus showed with computer aid that the optimal ruler for $n \\leq 65,000$ has length less than $n^2$." ] }, { "cell_type": "markdown", "id": "9490f408", "metadata": {}, "source": [ "To build a COP (Constraint Optimization Problem) model, we need first to import the library PyCSP$^3$:" ] }, { "cell_type": "code", "execution_count": 1, "id": "af6594e6", "metadata": {}, "outputs": [], "source": [ "from pycsp3 import *" ] }, { "cell_type": "markdown", "id": "cb32eabe", "metadata": {}, "source": [ "Then, we need some data. Actually, we just need an integer $n$." ] }, { "cell_type": "code", "execution_count": 2, "id": "a34ab67c", "metadata": {}, "outputs": [], "source": [ "n = 4" ] }, { "cell_type": "markdown", "id": "9bc4dfe6", "metadata": {}, "source": [ "We start our COP model by introducing an array $x$ of variables. Becasue Dimitromanolakis has computed relatively short Golomb rulers, and thus showed with computer aid that the optimal ruler for $n \\leq 65,000$ has length less than $n^2$, we use $n^2$ as upper bound of the domains of the variables of $x$." ] }, { "cell_type": "code", "execution_count": 3, "id": "e18a903e", "metadata": {}, "outputs": [], "source": [ "# x[i] is the position of the ith tick\n", "x = VarArray(size=n, dom=range(n * n))" ] }, { "cell_type": "markdown", "id": "56d09f05", "metadata": {}, "source": [ "We can display the structure of the array, as well as the domain of the first variable (remember that all variables have the same domain)." ] }, { "cell_type": "code", "execution_count": 4, "id": "8a9c4c18", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Array x: [x[0], x[1], x[2], x[3]]\n", "Domain of any variable: 0..15\n" ] } ], "source": [ "print(\"Array x: \", x)\n", "print(\"Domain of any variable: \", x[0].dom)" ] }, { "cell_type": "markdown", "id": "c6e5257a", "metadata": {}, "source": [ "A simple model involves a single constraint *AllDifferent* that takes as parameters a list of expressions (and not directly some variables of our model)." ] }, { "cell_type": "code", "execution_count": 5, "id": "d421e596", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " # all distances are different\n", " AllDifferent(abs(x[i] - x[j]) for i, j in combinations(range(n), 2))\n", ");" ] }, { "cell_type": "markdown", "id": "828b5826", "metadata": {}, "source": [ "Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT. We can also display the found solution. Here, we call the function *values()* that collects (in the last found solution) the values assigned to a specified list of variables." ] }, { "cell_type": "code", "execution_count": 6, "id": "b471ec66", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[1, 0, 3, 7]\n" ] } ], "source": [ "if solve() is SAT:\n", " print(values(x))" ] }, { "cell_type": "markdown", "id": "a27d5032", "metadata": {}, "source": [ "The obtained solution does not necessarily give the ticks in increasing order. It means that many symmetries exist. We can break them by setting the first tick at 0, and ensuring a strict order with a constraint *Increasing*:" ] }, { "cell_type": "code", "execution_count": 7, "id": "05cd0621", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " # tag(symmetry-breaking)\n", " [x[0] == 0, Increasing(x, strict=True)]\n", ");" ] }, { "cell_type": "markdown", "id": "7e9193f0", "metadata": {}, "source": [ "Tagging (the list containing) these two constraint is relevant because it clearly informs us that they are inserted for breaking symmetries (and besides, tags may be exploited by solvers). Tagging is made possible by putting in a comment line an expression of the form *tag()*, with a token (or a sequence of tokens separated by a white-space) between parentheses. " ] }, { "cell_type": "markdown", "id": "ed51cfdc", "metadata": {}, "source": [ "We can run again the solver." ] }, { "cell_type": "code", "execution_count": 8, "id": "a6c860f0", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[0, 1, 3, 7]\n" ] } ], "source": [ "if solve() is SAT:\n", " print(values(x))" ] }, { "cell_type": "markdown", "id": "898415e1", "metadata": {}, "source": [ "This time, all ticks are increasingly given." ] }, { "cell_type": "markdown", "id": "9c75fda0", "metadata": {}, "source": [ "Concerning optimization, we want to minimize the length of the rule, which is equivalent to minimize the value of the rightmost variable (tick). " ] }, { "cell_type": "code", "execution_count": 9, "id": "64f7540e", "metadata": {}, "outputs": [], "source": [ "minimize(\n", " # minimizing the position of the rightmost tick\n", " x[-1]\n", ");" ] }, { "cell_type": "markdown", "id": "f67ab4ee", "metadata": {}, "source": [ "We can run again the solver, with this optimization task. Note that we need to check that the status returned by the solver is now OPTIMUM. " ] }, { "cell_type": "code", "execution_count": 10, "id": "9fe3600e", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[0, 2, 5, 6]\n" ] } ], "source": [ "if solve() is OPTIMUM:\n", " print(values(x))" ] }, { "cell_type": "markdown", "id": "1e0cdf65", "metadata": {}, "source": [ "This time, we have an optimal Golomb ruler of length 6 (for 4 ticks)." ] }, { "cell_type": "markdown", "id": "265fd0d1", "metadata": {}, "source": [ "We invite the reader to change the value of $n$ at the top of this page, and to restart the Jupyter kernel." ] }, { "cell_type": "markdown", "id": "c0e21d06", "metadata": {}, "source": [ "Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line)." ] }, { "cell_type": "raw", "id": "ac1bf8bd", "metadata": { "raw_mimetype": "text/x-python" }, "source": [ "from pycsp3 import *\n", "\n", "n = data\n", "\n", "# x[i] is the position of the ith tick\n", "x = VarArray(size=n, dom=range(n * n))\n", "\n", "satisfy(\n", " # all distances are different\n", " AllDifferent(abs(x[i] - x[j]) for i, j in combinations(range(n), 2)),\n", " \n", " # tag(symmetry-breaking)\n", " [x[0] == 0, Increasing(x, strict=True)]\n", ")\n", "\n", "minimize(\n", " # minimizing the position of the rightmost tick\n", " x[-1]\n", ") " ] } ], "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.7.12" } }, "nbformat": 4, "nbformat_minor": 5 }