%% nav-debut : généré par gen_navigation.py, ne pas modifier à la main %% > [!nav] > ↩ [[Code et Développement/Programmation/Optimisation de problème/Optimisation de problème|Accueil · Optimisation de problème]] %% nav-fin %% # Atelier 3 - Professeur débordé Cet atelier reprend la situation de l'[[Code et Développement/Programmation/Optimisation de problème/Atelier 2 - Professeur populaire|atelier 2]] avec jusqu'à 1000 élèves. La force brute n'est plus possible. Le problème se traduit en formule logique 2-SAT, que l'on sait résoudre en temps polynomial. L'atelier s'appuie sur le chapitre [[Code et Développement/Programmation/Optimisation de problème/03_Satisfaisabilité (SAT)|Satisfaisabilité (SAT)]]. Énoncé repris de la Battle Dev Hello Works de novembre 2018 (isograd.com). Niveau : ★★★. ## Énoncé Chaque élève propose deux créneaux de 60 minutes. Le professeur doit donner cours à chaque élève sur l'un de ses deux créneaux. Comme dans l'atelier 2, le professeur ne donne cours qu'à un élève à la fois, et il ne peut pas terminer un cours et en commencer un autre à la même minute. Il faut dire s'il est possible de donner cours à tous les élèves, et si oui sur quel créneau. ### Format des données - Ligne 1 : un entier N, de 3 à 1000, le nombre d'élèves. - Lignes 2 à N + 1 : deux entiers de 0 à 300 000, les débuts en minutes des deux créneaux de l'élève. La sortie est `KO` s'il est impossible de prendre tous les élèves. Sinon, c'est le numéro du créneau retenu pour chaque élève, 1 ou 2, dans l'ordre de l'entrée. Toute solution valide est acceptée. ### Exemples Avec les 5 élèves de l'atelier 2, la réponse est `KO` : quel que soit le choix, deux créneaux se chevauchent. Avec les 4 premiers de ces élèves, `1 2 1 1` est une solution : l'élève 1 de 205 à 265, l'élève 2 de 370 à 430, l'élève 3 de 290 à 350 et l'élève 4 de 120 à 180. ## Données Les cinq jeux de test sont chargés dans le dossier de Python de cette page. Les fichiers `input4.txt` et `input5.txt` comptent 1000 élèves. Le fichier `outputN.txt` contient `KO`, ou bien seulement le créneau du premier élève dans une solution possible. Une autre solution valide peut commencer autrement. La fonction `valide` contrôle donc une solution sans la comparer à un fichier. ```sq-fichier nom: input1.txt --- 5 205 300 210 370 290 380 120 305 390 110 ``` ```sq-fichier nom: output1.txt --- KO ``` ```sq-fichier nom: input2.txt --- 4 205 300 210 370 290 380 120 305 ``` ```sq-fichier nom: output2.txt --- 1 ``` ```sq-fichier nom: input3.txt --- 100 6969 338 15605 16525 10281 6820 11985 8172 14092 2699 7839 9936 1071 19114 7185 7483 1953 1276 333 10936 2542 4268 15370 7340 786 4676 8588 6208 4094 19444 6722 304 18946 1884 9402 3953 18409 1935 19347 9852 6361 15662 18686 1857 12526 1460 12225 3501 10193 2684 19446 1696 1926 3070 17162 15106 2841 15895 5817 18251 12995 12861 12991 1781 13202 9798 4168 1532 2365 12525 11410 8157 13934 14575 18067 1109 10711 1510 12333 16987 18835 10340 7282 15732 16072 2946 17202 18089 9639 15388 10506 8631 2301 988 7003 1871 13193 18217 13316 2262 17065 15612 6016 8301 13230 5075 5056 15330 4954 11005 2888 3825 11278 15577 5057 17589 9323 12519 17090 17052 10506 11505 1265 3229 8880 4149 14455 16961 3033 19231 4928 9934 13138 18725 4354 11931 17243 16553 8286 12792 14378 19286 19367 15461 17727 10443 8039 550 14046 14354 19206 18512 111 13864 14084 8582 19416 8482 16459 5745 10433 9354 4482 12920 2207 7320 3513 8480 10196 6938 3687 258 3006 17418 3318 19042 4937 1864 8665 7156 377 1712 1737 4833 6509 8474 14928 9404 15744 19080 10777 10027 6096 9997 9090 6039 17698 18021 11963 10244 ``` ```sq-fichier nom: output3.txt --- 1 ``` ```sq-fichier nom: input4.txt --- 1000 55511 160483 64343 90479 24119 67860 206539 21448 18455 71921 62681 96411 180983 184803 214187 119970 61124 68220 48938 114883 109713 154600 164603 216012 99081 130007 124032 32395 114987 24211 50470 203445 50417 151834 86422 54914 47717 143081 28573 150643 151718 75394 151132 66426 122981 110834 84734 170473 32170 150380 178661 84045 191358 117763 51969 52684 24156 149515 146641 103096 131159 198221 54002 100116 67655 114234 48332 60111 169648 84408 146984 189621 18313 212569 35410 53192 57546 73972 15396 9908 152904 184031 210876 172565 158798 122697 25813 6506 208028 26994 103764 191287 185690 177401 87758 38045 56446 194903 103769 150423 101979 34706 19053 10303 155229 149031 33991 33713 63605 86337 125782 3071 12858 193066 20148 91277 213431 9044 216270 138158 202417 184481 60296 128152 50042 22720 107872 118396 92087 197943 17510 104514 106827 145858 205572 216903 128598 151655 192487 66014 204882 136856 46992 3829 144141 127550 103711 17061 168926 125144 61581 23684 53523 65381 80819 134688 141424 60430 160869 189756 107528 159978 101707 9008 97624 185395 175482 135853 146489 75679 181310 30682 19337 192267 156846 118553 144939 187147 112646 73374 166790 27327 122958 117795 4986 42369 44184 127957 52465 80150 164886 131543 31677 28499 157747 1991 146450 114897 73085 208313 115886 86841 104124 190162 184569 107437 14712 194216 53206 40618 101743 160526 184928 4035 182566 202832 113013 48623 31777 101244 41523 153927 30583 121082 153419 143683 203315 92247 53430 153646 167615 99006 58236 59751 171574 101353 44654 12214 63875 161714 198373 168687 116097 18439 94845 49663 10477 136518 68456 69544 168924 33235 197179 13502 47842 217146 189794 194368 130378 185100 79587 92488 205528 191445 72307 93967 64749 10371 41491 5946 81866 40608 136875 1400 146305 159148 22701 60835 108952 190551 138264 166614 59605 179073 113664 205633 49871 66583 157230 194927 215687 121668 166523 104319 164064 203801 144123 97542 3623 110361 103863 111654 56188 168470 199672 45148 197409 119282 49620 96396 133994 39325 209002 48306 110024 49874 43148 180582 153997 56178 127544 188359 144582 121095 77252 182546 27415 137352 154407 140227 99249 56673 9049 51 80835 113587 173487 31699 27667 195825 184502 130960 130665 68055 48886 71094 39536 37999 155166 139577 51299 214911 106398 85604 127968 117650 160312 102596 178175 131102 179328 24381 215198 84131 93350 201213 108656 176781 165150 16335 203814 19063 145221 149562 6974 209453 160410 201448 162016 121189 175198 207421 171902 141898 205091 105420 163107 45358 22041 206484 55654 75953 115413 5867 27055 79646 154793 187704 96672 58562 147806 105783 93732 90308 51174 27464 97042 58262 111649 121162 147123 45450 57842 120569 152033 201888 19517 39932 100745 101469 167306 53732 128854 27842 153065 90934 178526 57298 96765 40932 134340 39086 10343 145957 131505 212510 154482 193081 51507 184118 177216 184674 216485 166865 213546 131046 83101 91862 39349 136698 178214 161631 102222 111603 187685 37189 98052 101196 156424 43243 150028 71646 156902 81664 143438 1951 206243 191464 117419 91677 17407 148398 18909 22510 73092 128409 196800 116786 45638 6206 133304 115314 161661 162532 79855 179524 200571 37339 171290 67582 179429 196313 102645 885 55711 177412 124519 185150 201722 88823 173774 141496 17718 8866 60849 33214 101423 49567 86664 27623 129020 15778 126356 128501 56814 1083 118058 18453 150433 70051 210410 121989 67833 53790 201567 34498 167698 57328 90378 145530 140058 212626 12019 141975 246 76601 126253 167216 198068 88486 185738 186860 89564 192384 179567 74468 204872 147704 78626 12465 24501 35813 38706 34319 118888 43716 147599 55032 68280 188166 164963 196615 215411 87865 35081 99472 126112 152343 59832 15539 80041 195634 85976 129987 156141 50335 119577 177844 132029 130740 63770 147811 24691 34956 106841 85599 3413 15289 28510 195375 128119 65610 173713 84438 41497 14424 86522 178271 135429 202628 153027 141405 134319 199334 14560 140969 101563 196081 92122 103654 2820 150134 216648 183693 137402 42234 154632 11922 207637 120147 89648 111020 112831 111922 67454 6641 65482 160680 179445 192991 90086 165410 95229 161991 1456 51068 54812 98628 38750 70152 97235 19483 131729 57504 63310 91034 109105 124170 141736 160317 87899 200954 175754 31752 6670 21436 40293 3407 57171 72434 146191 187054 195281 94845 30003 204435 113844 68960 31436 10671 198330 75672 105908 142490 38945 47010 77604 55542 156157 167170 30364 145264 179349 213048 195839 1358 115616 216217 35838 143404 56035 117693 134738 143931 39703 8377 63744 63872 158000 131819 69388 94461 18459 108462 102825 11602 196132 143110 171257 128438 168611 211810 56812 98418 150131 22364 54271 164139 54377 79896 14671 188442 72646 41680 94907 122443 79436 171847 119936 217022 158859 1056 77692 175002 72061 173608 89696 180277 94998 29721 210608 86105 8203 11702 157229 44723 166400 52102 186535 132361 115568 33851 87533 111200 82048 213341 221 21953 174594 52797 159946 55171 94818 189907 77233 82304 1103 203264 190088 86203 175115 41878 145134 26478 120118 43565 194913 41998 116686 189900 25866 177088 211492 42678 166403 96892 164353 138257 157839 154984 173035 100046 143829 65395 29052 139602 135104 175015 209044 193052 22654 60899 190313 133603 151200 160819 188442 76958 179233 118564 51797 143439 110801 192097 143861 91422 2055 32051 145665 30274 168159 58279 180416 146250 25212 25411 32005 60379 107725 70240 215611 49417 186993 93979 172955 34078 71387 66262 164210 200840 161344 113870 21819 9673 197851 38941 192034 122879 57188 88093 158969 137081 109143 89272 87623 136386 4942 34176 198634 215659 22278 163897 14206 191594 175396 75191 132798 17111 207317 77098 79326 46654 37055 203483 100535 13148 206730 42255 21090 194522 29088 45320 206830 194033 99660 108010 109517 175157 214260 187417 4049 123310 171359 143668 207099 194203 5842 193853 211966 96228 55701 35141 97069 24073 62872 162311 136454 217977 186297 173800 195737 160 168840 119019 7983 183731 2312 193243 106113 27627 51305 107165 160421 206597 188525 13461 87105 152904 141419 34860 140135 122552 200621 102152 3048 13838 188156 179278 3670 103062 53776 181340 19100 102382 84039 88714 2278 65448 194276 204642 40153 10771 175172 110087 70913 174723 213699 60186 32888 139908 21726 191020 28732 29752 203513 107161 167155 133850 155752 146337 106669 114925 215045 61883 64054 9631 109149 8637 79427 203236 84986 45119 133138 139756 16563 97458 45832 41244 19871 48388 89 41135 1574 189286 61131 13970 180536 157155 158137 151016 8276 145428 3896 158540 140790 90842 127020 120650 31479 113289 92102 28038 113465 179542 92912 190306 28504 79515 48507 214846 133476 95368 162758 180160 131302 85813 98224 168451 112484 138394 184445 126634 44019 123160 163626 210377 193184 207482 147135 99463 52181 162134 137761 163632 185213 153001 165064 160237 194465 40841 29040 183886 27497 193143 215943 180197 202077 7717 2582 50802 77712 61725 173564 149739 7763 38639 151586 114947 133622 156271 197254 176770 188430 112720 12727 12345 86453 101093 97686 127684 99073 8924 48137 54941 70470 164931 120994 66920 100765 116844 216953 183819 136364 45136 72550 204841 153820 157689 115401 33587 72907 18855 122915 88397 204439 73211 29969 145194 79901 22883 201632 36600 138845 170909 108383 11394 103188 51095 178858 75389 200870 199812 84408 214325 201533 148636 25720 6940 162589 183596 152021 109291 197374 172634 181596 32236 50539 7934 56215 210929 19114 61549 201864 125367 104378 107550 88677 81534 143299 88228 27116 118646 68147 179776 102302 16289 90933 5482 8207 167707 97832 79052 134686 128453 62990 175425 112663 76898 66287 15334 187929 60646 141974 168335 100463 154512 212298 39546 201631 184137 108752 43279 55349 49354 67822 107089 204446 32059 122979 191213 11453 18448 64205 207130 153037 181311 116293 196809 115340 173515 43643 58159 107835 215107 126184 6799 39307 109634 207375 110428 212903 103227 213527 20711 4830 26231 136922 158575 196129 154915 106447 169601 153900 117956 82434 57904 120710 107150 83418 80164 127069 104891 215235 116322 201010 160729 55627 170604 121818 198885 156017 58590 38081 199742 51934 100703 143550 150563 91855 45102 45377 183730 115080 201988 52892 20369 3157 190890 212712 68597 193584 48924 76429 138796 8820 37941 35124 109734 92990 117662 185333 207475 9086 67401 205685 132997 74717 212467 89445 132174 150723 48175 66543 115503 48521 4748 68997 63343 71022 94651 167398 174562 170668 214001 22005 147573 10834 71172 183243 86617 69928 192876 112969 158822 151312 214397 6608 61083 63387 173896 65658 182084 191013 204594 163358 23978 116568 180682 66103 87243 153648 29016 26997 136116 125731 206266 35828 184488 58211 4713 138025 149200 147270 33749 15108 188773 6521 143131 49532 169388 131725 6883 33100 39705 26288 69765 145662 175554 91918 216289 193104 40472 114610 213820 140296 198374 159800 104325 130940 192976 8864 151272 184951 32102 177451 21472 66330 106144 147812 133945 59112 175528 50666 48599 170173 123191 122413 195142 51551 54014 127357 117952 143485 215076 209537 18567 145497 63342 60718 68896 180344 61087 78474 36299 56750 142610 35842 195167 197709 51223 103118 148368 176921 84889 179682 69491 157884 67293 17700 15279 177858 201277 134736 185951 65807 147278 145216 167600 52735 212688 62682 154244 106591 199112 122337 28040 10242 185962 158306 216180 190426 85239 182910 121886 206752 179420 87951 120648 44548 69057 152591 206075 86436 186677 53498 130604 80415 160544 50630 38911 174149 189485 31044 101210 162245 198814 48210 114935 175195 132492 205964 117275 48831 146148 159936 12605 11440 190344 131182 42658 154383 172423 138271 173921 151827 49634 199661 54583 148475 77716 202596 99791 198173 99936 97324 3293 183341 96703 89715 144729 33703 204730 191133 85136 207208 206354 126028 96022 73407 21535 144485 68215 87778 122853 166064 178641 211024 141074 113895 23012 45429 166309 37438 144312 188373 212535 101069 69133 103296 61022 19294 26916 83227 134486 139019 1088 17770 200489 216760 154491 25231 216978 151056 126289 171736 108109 188685 21769 110838 106769 200040 33837 67287 185045 9686 124333 103503 194428 142444 6279 104232 117489 65919 75560 172732 148346 202779 60976 157654 196849 4843 34556 164856 84294 153398 38024 118092 27909 195392 117569 196140 25890 72261 169516 209391 185315 55088 117194 73925 79016 49517 86394 88703 199114 92017 19422 130720 39879 186939 215829 67400 190219 28357 112940 10238 118407 40368 135532 71879 84856 126075 70084 21775 155013 23284 213644 100447 103470 201974 80839 16959 38246 170997 157753 131517 214482 158449 13865 76384 67771 163291 121025 128289 184147 51101 70626 88347 114482 86799 214951 171038 189281 87130 160069 36579 61293 159095 106601 189129 31002 31055 205561 167035 9795 104618 44004 216601 16056 156038 70851 182897 187955 44746 169678 192934 146909 98885 164294 85435 128649 66156 28583 142414 164049 170884 217697 95361 87288 68907 97529 158301 120204 51937 18479 204971 195881 23165 55544 102046 105983 20860 134605 176932 107978 113334 20164 137520 144310 32768 17122 35464 67413 165963 33662 16018 191549 129802 28757 8155 18144 174437 188605 199840 48715 114788 62157 186450 173848 82887 203896 107515 14365 166578 82750 76068 207568 136121 69246 83937 181377 70438 204483 116193 66058 49374 49579 92799 209345 194595 16732 67872 14986 23118 48910 61322 104937 32582 113910 63971 167780 98303 104676 205555 43119 185041 183072 52875 2483 186159 46982 70531 47437 217069 195484 49887 130547 189243 55867 96656 45381 77713 33710 39686 19811 73541 114684 203178 145717 154300 7822 156960 123338 78290 70790 118474 97040 204617 108484 79887 129370 99161 109909 195779 13119 69664 64056 99309 34251 80848 215021 26262 181513 4093 197323 128404 123457 212719 164343 77732 95175 92349 210874 23819 1080 15689 30488 49193 4720 154207 5138 116220 35873 214066 78722 27363 60695 173478 65046 116605 125979 105497 141056 143694 69074 166781 175578 150951 17086 89552 11014 186651 69658 88872 116286 45795 170002 95938 171513 58408 8337 180346 210776 171218 214442 37773 148390 161755 16535 214636 145174 104897 174486 209558 46078 86127 138405 5697 211996 204422 35582 134467 16393 191984 173599 146682 97101 24475 148353 173152 2563 44737 128289 131030 23825 194941 14707 127152 119151 92722 58197 200283 76166 16254 165860 118705 106677 41374 25204 195200 79418 88331 212067 162502 138889 118956 212341 106761 33872 213433 40823 209335 91262 66894 14467 80006 161222 134289 141936 85289 130388 125685 202108 177374 195992 13034 143932 158064 93841 217414 42114 72316 11347 155935 71070 75016 61250 173527 212314 166294 69982 153905 168046 41252 194607 83831 36870 194800 173439 52059 175834 148392 145924 50567 49627 40913 208999 11904 53135 59557 158315 77608 67618 209211 27120 179537 30923 26431 93488 164327 146484 66708 47260 146882 21600 38032 65364 22773 146518 52883 50991 87687 170 4647 8428 21681 169622 106044 168215 58195 150333 48272 46722 186071 165763 129664 134906 154899 200972 68651 126956 151601 172981 73681 213366 66537 60634 206779 23683 119622 83958 ``` ```sq-fichier nom: output4.txt --- KO ``` ```sq-fichier nom: input5.txt --- 1000 154303 183783 200935 2254 208280 116743 30779 186454 51939 200210 84884 179581 101871 27515 163109 48047 56362 22450 55680 206807 41925 11636 17020 11211 118700 96291 85042 79308 121729 1567 99864 95602 35247 185125 117878 70913 164527 100828 111594 78390 148044 117029 9589 118331 179107 200681 204413 106921 128675 157252 10396 183927 53528 80461 144350 165739 191406 210421 17641 140588 45508 928 30938 97817 124346 127700 65388 42045 143844 110737 108609 14911 80840 4277 174496 146275 133911 132092 60039 2094 207295 50661 75080 93635 85415 28524 39277 82472 37358 59329 203753 63132 123735 153893 9031 41706 103678 76875 64387 167074 42000 4881 136822 26320 175105 93858 173186 49598 107551 177049 122106 22880 18347 130385 93564 62161 85235 100075 65715 133527 115001 150079 144938 71632 31432 96643 9700 84129 88819 66611 120889 189678 28004 126195 52781 116568 208405 106515 149510 151554 53011 153877 3166 191537 178786 27780 96743 101026 70845 140496 168508 155910 196441 114799 18762 182797 135175 199911 203293 25935 8287 207284 38916 183498 33014 86759 15448 15268 48693 17686 213879 78880 112329 131911 40253 181837 214768 132272 143275 122115 209091 164605 60402 170962 57514 41201 216165 28771 149128 176697 202701 73130 9624 22582 51778 190029 10687 122625 124776 22386 27690 186229 155170 113926 133231 100204 29691 111498 73868 117898 200728 65323 161887 113843 81632 193735 113025 60916 144379 99435 122567 110636 156361 97353 173426 72691 177366 31709 116148 1931 7624 47263 133047 40959 75202 99107 43032 102592 174895 75628 86040 71053 49438 80708 216981 10553 38042 195573 158491 217254 55110 4584 72214 148209 202277 141504 87287 80173 178749 62267 116991 9336 173739 195693 102190 201925 71266 159032 203905 99930 25784 207614 35764 206586 145196 172117 52029 193700 171312 199615 67626 125411 215261 100749 168813 36936 191649 87891 75553 57152 57535 19732 117200 129851 216145 115667 65085 194171 215734 32062 56033 11395 112573 95592 131885 102550 180549 39030 190751 21206 72914 172062 78256 5886 193092 124143 128770 151905 200179 29459 33799 45632 208135 198490 19583 6116 109669 139958 88174 120744 181180 89999 187785 169601 73028 39164 97453 9755 104933 195607 177415 121213 47977 101233 35931 75295 203708 146433 46189 152989 4119 135304 46703 18677 174271 5392 147535 133515 28021 30622 137240 36337 102163 133995 60189 199711 157274 161028 186258 64505 185134 112017 32068 139776 6751 12571 42968 53924 12292 199662 132153 53266 129376 24798 92884 133458 161115 121242 132303 103567 198239 125747 6052 103599 92371 151399 201905 174055 85496 49791 43711 207308 150635 305 81351 157691 9887 36591 57055 58497 98247 1800 73746 137433 30916 83125 177057 65882 77449 215959 101888 146091 152448 170223 140641 128361 104890 150840 77504 129697 2483 77850 105674 140197 119554 110261 63470 41784 95469 48816 213275 49171 174860 160381 212712 59875 124082 195940 211796 152653 182219 61579 178233 156854 173121 136024 134454 210115 30118 85865 155458 83170 206977 194757 212430 3103 86526 21791 130238 181327 57391 150622 14329 217224 204645 54237 83782 137312 170367 39940 33392 34905 12992 38796 99618 109758 118797 143583 56752 140420 137484 47557 23378 137993 73246 111423 157071 200459 209623 5929 97103 142779 57364 189082 89898 66968 24792 113491 107620 6864 45921 96360 183373 45058 204604 157304 144965 37108 35868 58344 2538 53427 204458 67452 28069 21353 36868 208982 203592 29304 19477 214004 141026 96678 133303 29021 177084 8495 182742 49382 122211 194636 66496 200901 149631 92334 23040 204655 209296 110724 58993 139830 75791 63506 112869 66180 8774 207949 182032 51188 90613 141223 23421 98136 68155 68806 211302 100604 141525 181767 29878 58449 211605 1622 130374 171691 129605 124673 84529 165150 115159 157351 185293 177058 84738 149995 92001 92480 186115 21125 217876 57098 131243 7974 15334 4433 11946 185093 8396 123876 47079 7681 124837 209441 9572 75859 116000 31357 161355 11918 94819 170023 144289 200073 68501 83045 199062 62315 40925 113303 84432 164167 73074 88822 209790 44754 123163 145759 70195 86663 76144 137481 195400 205202 14702 143 25207 28600 143489 33219 131480 152577 153249 45555 189615 12034 28335 51917 136491 170994 22297 202697 142651 184635 146323 17608 142397 107804 177404 68472 39809 136467 61362 59702 63130 201594 139441 140672 112573 16407 53164 155362 196063 61553 164236 144392 34726 108035 111610 208428 13196 144673 14506 48217 189431 175458 137647 120666 137180 178607 115875 77847 156564 143015 126183 53745 109922 168694 53969 54622 206369 196073 5555 90264 145359 89387 142199 40720 36532 56440 133858 201176 1950 212744 107946 181463 151816 159315 14378 154093 37214 162093 206412 87528 149648 73085 187695 79553 79396 197727 154498 35189 180425 120287 217835 68379 115972 217897 57575 78963 44864 44500 94105 182607 57202 173046 8841 152469 86527 120458 100567 65689 64054 137514 179462 123528 112714 158348 146757 2375 62129 141681 99065 12841 217802 74204 151337 125402 215418 121935 207540 18179 163277 151438 64498 41995 187495 179147 162432 183882 17853 11425 86772 2041 199917 181790 109881 112320 93980 46151 121469 152883 25806 72596 60825 160125 66530 160462 101982 40707 79120 187600 38086 93347 46713 2991 108840 188316 85498 106063 20703 5128 169353 7819 60397 199874 43597 207143 120978 116796 166340 120091 15763 163731 159549 103371 168945 32104 59773 171997 216255 107189 76176 96612 121664 69251 160558 99357 125999 28355 149010 5516 23265 85648 110484 217893 28080 72833 126393 78320 44339 58138 25217 171315 213167 126480 113904 114942 213535 208935 82946 149502 40978 203173 120167 118698 16747 114735 113183 81756 166586 17352 100303 9033 175878 66916 148225 102133 1591 214896 47339 62308 150632 111266 95563 215844 24605 66522 59406 125439 135554 12581 159442 13606 27745 157935 49236 40788 22711 199127 12795 171336 7778 127842 164782 47459 36281 163614 48122 128411 163102 83347 87025 211061 74281 132605 140032 120337 195194 129141 31176 101545 113513 46284 185367 17805 7177 83816 188852 58112 196441 203071 156605 197923 78743 27192 86018 161992 94733 195995 109867 141813 97812 157964 86771 108573 52751 191200 46290 28182 202781 95733 196691 36626 216645 66158 186329 41858 164635 177667 49514 151542 213241 196133 121378 198062 25894 12687 96289 74339 190929 203541 8140 153104 143481 176967 25767 200516 16333 21387 42607 55454 203310 178923 177151 75730 58869 157598 193021 103550 75877 150615 46051 6466 137030 99942 132131 54294 65621 98592 22831 162857 22018 99613 76207 185291 186912 181190 141865 69899 24116 94769 194188 50343 18133 53697 114109 165648 72283 162621 174613 26961 69807 38005 191770 95127 110254 186744 10809 165123 74690 48909 110139 90010 117020 77244 74583 151565 136712 45784 112124 152565 115085 85043 203449 84674 73374 19501 192651 154814 215633 194130 177247 131730 83701 188993 174419 160571 167628 20445 146389 154776 125138 168100 194927 74885 69546 203329 84950 114711 107452 22871 168505 124073 94937 129307 129371 38685 171876 94250 104215 79448 78599 162183 150862 18281 57017 89785 13068 100837 173426 212270 120876 53138 204275 125138 4965 71804 206607 160130 52729 68906 75675 159120 19824 214558 74992 119624 101419 87607 103336 163925 164618 179450 137401 73221 148399 41867 217910 194730 122064 116346 18963 195239 10068 65469 137297 94272 126266 216870 58119 152540 162763 16540 97388 83649 122146 99214 106566 193037 198283 140449 122668 12466 101605 176175 215802 51608 197108 72055 146340 6899 53596 206865 166687 150926 178982 138979 40812 126561 112578 17745 62937 200114 89481 186414 147891 50714 79804 182093 76237 178593 21775 183035 209369 137160 39721 46532 170478 71007 141003 31969 31304 9866 118453 132969 171726 147933 194502 17176 91568 18683 170287 206997 41099 157758 6461 64477 128311 77610 139032 179387 148808 90008 78712 74781 39499 88059 20633 197883 26635 43220 27929 196480 118545 122107 172027 103683 196870 115679 22847 196019 178851 173776 64300 38807 92566 200120 1783 35018 63384 1030 103753 109950 122484 207896 63844 138572 335 83367 156937 166493 13679 155028 42610 180196 30417 100947 141591 15855 7865 160416 137109 18906 61234 140560 105422 110854 167777 113479 38712 2547 59390 210754 155241 207877 156831 139529 20997 59284 7253 148073 144601 114516 14451 92192 201682 50474 42442 184338 211299 88484 40334 131557 145201 10815 171652 63730 34079 79665 133985 56012 205035 44648 41304 29123 134856 84363 32660 145880 31155 215024 99387 178651 66759 135693 74168 26996 26625 20561 13180 116736 13054 187794 217822 69195 151378 1940 186172 200616 178744 41850 140329 161723 160401 150519 177911 48616 47881 17200 194606 7495 37706 209319 127745 75832 206943 138684 58004 10043 171965 9174 57213 44076 178926 36261 151123 6742 148565 205548 97468 197328 97613 123941 50616 55107 27511 162508 143732 129842 156455 152589 184684 195318 105525 130308 107074 72041 121260 189963 136973 11680 177074 42691 84752 193415 181608 28983 142317 125172 173935 3348 142997 40430 194416 205091 50169 217287 110453 145272 196548 8145 26175 108133 54155 112885 42303 105828 166158 81117 21742 46015 126346 198398 49538 211677 67314 51026 139731 16370 182155 148379 6986 49411 89093 94489 197118 173697 75553 117573 3293 126358 162319 198535 1815 112041 151058 70570 156603 159963 30789 124429 162813 25097 58061 179339 99746 158296 84803 102301 27231 143915 160746 151807 9015 138819 95955 111408 77517 156523 110973 3675 116043 134617 27478 195261 49824 152673 132564 95987 148510 95466 8199 178599 111707 26258 138008 67419 118552 110578 59380 47093 113420 98033 190287 64502 94223 58716 125874 96274 89955 38901 14303 2452 94244 54604 189558 90930 101856 66952 124608 36902 126979 52407 74533 31633 71238 217896 159443 106333 165117 57095 38944 182255 100660 172448 105049 38529 48028 9964 99664 111025 102199 148816 11184 56248 118481 85830 141854 50214 191800 183402 84565 91539 96142 173832 213395 149025 50926 18677 36797 82528 126418 186911 47610 162788 73732 23239 47505 29577 57558 112033 182036 129811 103003 5556 15256 128736 171891 78087 189951 59181 7652 200222 101286 166871 93968 183524 193982 59166 74783 202580 56034 212075 110086 54570 125910 101396 65649 68303 87120 168858 17682 11901 42550 180351 12513 44011 12117 167646 42696 74723 15603 196909 131618 11307 99988 9028 172173 55650 68147 54008 197710 131413 17547 154023 42929 37541 184925 168336 4180 167191 176696 80181 171943 124862 16727 133171 82239 161860 122812 104955 48067 125591 131314 62609 177782 50775 11228 66504 197624 94857 155059 88542 63387 114457 110115 25486 94448 74630 165045 6288 107511 215729 4244 195772 203863 19412 157850 114175 164438 199917 213267 76055 41054 10159 101168 6902 121253 185733 19634 102202 84896 161379 200354 15253 42248 5251 11664 124513 202622 61678 71216 66847 10194 133721 44878 211810 205272 138689 70550 94792 30938 103332 30760 172526 89375 93461 184323 175846 160441 150941 136687 63288 69791 67856 166887 55007 185009 127661 146899 207693 6610 124722 166925 37234 198313 55536 215341 50888 82558 209924 3427 10581 57729 173916 208184 12745 175237 72448 120666 71171 206423 118371 51487 95548 12445 56369 185646 125575 141981 206044 146026 102454 151074 398 44063 139308 150959 187917 182607 52830 53295 187206 131434 86072 136649 158345 69893 59808 54107 150286 191811 123824 203144 96903 138347 172647 45216 154401 128640 48732 160483 205847 170035 170026 190221 19954 47426 198677 83997 154048 3396 60333 157117 176275 213229 98578 139731 12080 4695 175658 114201 62344 144342 152327 141537 29644 192626 191469 106269 191636 138013 74806 200848 175860 81083 58068 101404 71772 113898 71850 16503 194975 50760 181983 8505 174925 111542 92662 111219 8641 187768 86105 127032 148730 74512 130200 45696 170347 31542 9822 141010 24345 110161 22701 26136 76616 125415 30703 158833 51098 143280 203107 192385 44607 121138 44594 133332 99986 32264 93391 105412 6371 48505 209027 107666 19113 217100 143266 6916 112671 59316 199005 87814 81475 146188 168698 25152 179242 72941 115575 103673 157684 123199 111351 195488 119561 15177 169843 199708 7382 215880 8285 56781 63662 95311 134897 65794 134939 147093 15329 110879 87569 127728 43191 77981 200320 186188 48169 149489 192852 147722 104305 150680 215796 1070 98509 184377 193630 186801 26767 175640 140256 79439 18865 189906 126658 91331 11182 172693 96466 29558 84467 92133 106003 152850 123489 168415 183265 175731 60620 209562 34819 102863 98260 2251 203577 43953 182969 153446 60096 167506 63115 154151 136487 74858 207469 156271 154808 64501 49985 131556 58536 55699 76229 90507 79565 140062 71260 103502 15320 201280 69463 49330 158555 196673 144277 205319 203158 98954 212738 190387 159291 155495 16236 1312 17555 15939 121519 20188 22685 75065 153874 126669 185668 36955 18619 15501 114149 31503 196728 130930 77793 46265 53556 97748 71474 214741 214764 8548 195472 66954 128061 175434 189622 34765 35579 150672 217222 23802 189560 140508 128048 71048 36520 13932 9814 101751 139512 ``` ```sq-fichier nom: output5.txt --- 1 ``` ## Lire un fichier et contrôler une solution La fonction `lire_creneaux` renvoie un tuple `(debut1, debut2)` par élève. La fonction `valide` vérifie qu'une liste de choix donne un créneau à chaque élève sans chevauchement. Exécutez cette cellule avant les suivantes. ```sq-python def lire_creneaux(nom): with open(nom) as f: lignes = [ligne.strip() for ligne in f if ligne.strip()] N = int(lignes[0]) return [tuple(int(x) for x in l.split()) for l in lignes[1:N + 1]] def valide(creneaux, choix): if len(choix) != len(creneaux) or any(c not in (1, 2) for c in choix): return False debuts = sorted(creneaux[i][choix[i] - 1] for i in range(len(creneaux))) return all(debuts[k] + 60 < debuts[k + 1] for k in range(len(debuts) - 1)) exemple = lire_creneaux("input2.txt") print(exemple) print(valide(exemple, [1, 2, 1, 1]), valide(exemple, [1, 1, 1, 1])) #--- sortie [(205, 300), (210, 370), (290, 380), (120, 305)] True False ``` ## Question 1 : détecter un chevauchement Deux créneaux de 60 minutes qui commencent en `a` et `b` sont compatibles si l'un commence strictement après la fin de l'autre : `a + 60 < b` ou `b + 60 < a`. Écrivez `chevauchent(a, b)`, qui renvoie `True` si les deux créneaux ne sont pas compatibles. ```sq-python def chevauchent(a, b): # à compléter return False print(chevauchent(205, 210), chevauchent(120, 180), chevauchent(120, 181)) #--- correction def chevauchent(a, b): return not (a + 60 < b or b + 60 < a) print(chevauchent(205, 210), chevauchent(120, 180), chevauchent(120, 181)) #--- tests assert chevauchent(205, 210), "205-265 et 210-270 se chevauchent" assert chevauchent(120, 180), "un cours fini à 180 interdit un cours qui commence à 180" assert not chevauchent(120, 181), "un cours qui commence à 181 suit un cours fini à 180" assert not chevauchent(181, 120), "l'ordre des arguments ne compte pas" #--- sortie True True False ``` ## Question 2 : traduire le problème en variables booléennes On associe une variable booléenne à chaque créneau. L'élève `i` (numéroté à partir de 0) a deux variables : - `variable(i, 0) = 2 × i + 1` est vraie si l'élève a cours sur son premier créneau ; - `variable(i, 1) = 2 × i + 2` est vraie s'il a cours sur son second créneau. Une clause est une liste d'entiers. Un entier positif désigne une variable vraie, un entier négatif sa négation. La clause `[1, 2]` se lit « x1 ou x2 ». La clause `[-1, -2]` se lit « non x1 ou non x2 ». Chaque élève a cours sur exactement un de ses créneaux. Cela donne deux clauses par élève : au moins un créneau, `[x1, x2]`, et pas les deux, `[-x1, -x2]`. Écrivez `clauses_eleves(N)`, qui renvoie ces 2 × N clauses. ```sq-python def variable(i, c): return 2 * i + c + 1 def clauses_eleves(N): clauses = [] # à compléter return clauses print(clauses_eleves(2)) #--- correction def variable(i, c): return 2 * i + c + 1 def clauses_eleves(N): clauses = [] for i in range(N): clauses.append([variable(i, 0), variable(i, 1)]) clauses.append([-variable(i, 0), -variable(i, 1)]) return clauses print(clauses_eleves(2)) #--- tests assert clauses_eleves(2) == [[1, 2], [-1, -2], [3, 4], [-3, -4]], "deux élèves donnent [[1, 2], [-1, -2], [3, 4], [-3, -4]]" assert len(clauses_eleves(1000)) == 2000, "1000 élèves donnent 2000 clauses" #--- sortie [[1, 2], [-1, -2], [3, 4], [-3, -4]] ``` ## Question 3 : interdire les chevauchements Si deux créneaux de deux élèves différents se chevauchent, ils ne peuvent pas être retenus tous les deux. Pour leurs variables `a` et `b`, on ajoute la clause `[-a, -b]`. Comparer chaque créneau à tous les autres demande environ (2N)² = 4 000 000 comparaisons pour 1000 élèves. On fait mieux en triant les 2N créneaux par début. Pour chaque créneau, il suffit alors d'examiner les suivants tant qu'ils commencent au plus 60 minutes plus tard. Écrivez `conflits(creneaux)`, qui renvoie la liste des paires `(a, b)` de variables en conflit. ```sq-python def conflits(creneaux): paires = [] # à compléter return paires print(len(conflits(exemple)), sorted(tuple(sorted(p)) for p in conflits(exemple))) #--- correction def conflits(creneaux): tous = sorted((creneaux[i][c], i, c) for i in range(len(creneaux)) for c in range(2)) paires = [] for k in range(len(tous)): d1, i1, c1 = tous[k] j = k + 1 while j < len(tous) and tous[j][0] <= d1 + 60: d2, i2, c2 = tous[j] if i1 != i2: paires.append((variable(i1, c1), variable(i2, c2))) j += 1 return paires print(len(conflits(exemple)), sorted(tuple(sorted(p)) for p in conflits(exemple))) #--- tests assert len(conflits(exemple)) == 5, "les 4 élèves de input2.txt ont 5 paires de créneaux en conflit" assert {frozenset(p) for p in conflits(exemple)} == {frozenset((variable(i, c), variable(j, d))) for i in range(4) for j in range(i + 1, 4) for c in range(2) for d in range(2) if chevauchent(exemple[i][c], exemple[j][d])}, "les paires doivent être celles que donne chevauchent" assert len(conflits(lire_creneaux("input4.txt"))) == 1121, "input4.txt compte 1121 paires en conflit" #--- sortie 5 [(1, 3), (2, 5), (2, 8), (4, 6), (5, 8)] ``` ## Question 4 : résoudre avec un solveur SAT La formule complète est la conjonction des clauses des questions 2 et 3. Chaque clause a deux littéraux : c'est une formule 2-SAT. Le solveur `Glucose3` du module `pysat` reçoit les clauses par `add_clause`. La méthode `solve()` renvoie `True` si la formule est satisfaisable. La méthode `get_model()` renvoie alors la liste des variables, positives si elles sont vraies, négatives si elles sont fausses. Écrivez `resoudre(nom)`, qui renvoie `"KO"` ou la liste des choix 1 ou 2. Vérifiez les cinq jeux de test. ```sq-python from pysat.solvers import Glucose3 def resoudre(nom): creneaux = lire_creneaux(nom) g = Glucose3() # à compléter : ajouter les clauses, résoudre, lire le modèle return "KO" for k in range(1, 6): r = resoudre("input" + str(k) + ".txt") print(k, r if r == "KO" else "valide : " + str(valide(lire_creneaux("input" + str(k) + ".txt"), r))) #--- correction from pysat.solvers import Glucose3 def resoudre(nom): creneaux = lire_creneaux(nom) g = Glucose3() for clause in clauses_eleves(len(creneaux)): g.add_clause(clause) for a, b in conflits(creneaux): g.add_clause([-a, -b]) if not g.solve(): return "KO" modele = set(g.get_model()) return [1 if variable(i, 0) in modele else 2 for i in range(len(creneaux))] for k in range(1, 6): r = resoudre("input" + str(k) + ".txt") print(k, r if r == "KO" else "valide : " + str(valide(lire_creneaux("input" + str(k) + ".txt"), r))) #--- tests assert resoudre("input1.txt") == "KO", "input1.txt n'a pas de solution" assert valide(lire_creneaux("input2.txt"), resoudre("input2.txt")), "input2.txt doit recevoir une solution valide" assert valide(lire_creneaux("input3.txt"), resoudre("input3.txt")), "input3.txt doit recevoir une solution valide" assert resoudre("input4.txt") == "KO", "input4.txt n'a pas de solution" assert valide(lire_creneaux("input5.txt"), resoudre("input5.txt")), "input5.txt doit recevoir une solution valide" #--- sortie 1 KO 2 valide : True 3 valide : True 4 KO 5 valide : True ``` ## Pour aller plus loin : 2-SAT sans solveur Une formule 2-SAT se résout en temps linéaire sans solveur général. Chaque clause `[a, b]` donne deux implications : « non a entraîne b » et « non b entraîne a ». On construit le graphe de ces implications sur les 2 × 2N littéraux. La formule est insatisfaisable si et seulement si une variable et sa négation sont dans la même composante fortement connexe. Sinon, une variable est vraie quand sa composante vient avant celle de sa négation dans l'ordre où l'algorithme de Tarjan termine les composantes. La correction calcule les composantes avec l'algorithme de Tarjan, écrit sans récursion pour supporter 4000 sommets. ```sq-python def resoudre_2sat(nom): creneaux = lire_creneaux(nom) # à compléter return "KO" #--- correction def resoudre_2sat(nom): creneaux = lire_creneaux(nom) n = 2 * len(creneaux) def noeud(l): return 2 * (abs(l) - 1) + (0 if l > 0 else 1) graphe = [[] for _ in range(2 * n)] def clause(a, b): graphe[noeud(-a)].append(noeud(b)) graphe[noeud(-b)].append(noeud(a)) for a, b in clauses_eleves(len(creneaux)): clause(a, b) for a, b in conflits(creneaux): clause(-a, -b) # composantes fortement connexes, algorithme de Tarjan sans récursion index, bas, sur_pile, pile, comp = {}, {}, set(), [], [-1] * (2 * n) compteur, nb = 0, 0 for depart in range(2 * n): if depart in index: continue travail = [(depart, 0)] while travail: v, k = travail.pop() if k == 0: index[v] = bas[v] = compteur compteur += 1 pile.append(v) sur_pile.add(v) if k < len(graphe[v]): travail.append((v, k + 1)) w = graphe[v][k] if w not in index: travail.append((w, 0)) elif w in sur_pile: bas[v] = min(bas[v], index[w]) continue if bas[v] == index[v]: while True: w = pile.pop() sur_pile.discard(w) comp[w] = nb if w == v: break nb += 1 if travail: parent = travail[-1][0] bas[parent] = min(bas[parent], bas[v]) vrai = {} for x in range(1, n + 1): if comp[noeud(x)] == comp[noeud(-x)]: return "KO" vrai[x] = comp[noeud(x)] < comp[noeud(-x)] return [1 if vrai[variable(i, 0)] else 2 for i in range(len(creneaux))] for k in range(1, 6): r = resoudre_2sat("input" + str(k) + ".txt") print(k, r if r == "KO" else "valide : " + str(valide(lire_creneaux("input" + str(k) + ".txt"), r))) #--- tests assert resoudre_2sat("input1.txt") == "KO", "input1.txt n'a pas de solution" assert valide(lire_creneaux("input3.txt"), resoudre_2sat("input3.txt")), "input3.txt doit recevoir une solution valide" assert resoudre_2sat("input4.txt") == "KO", "input4.txt n'a pas de solution" assert valide(lire_creneaux("input5.txt"), resoudre_2sat("input5.txt")), "input5.txt doit recevoir une solution valide" #--- sortie 1 KO 2 valide : True 3 valide : True 4 KO 5 valide : True ``` ## À retenir - Le choix d'un créneau par élève se traduit par deux variables booléennes et deux clauses. - Un chevauchement entre deux élèves se traduit par une clause de deux littéraux négatifs. - Toutes les clauses ont deux littéraux : le problème est un 2-SAT, résoluble en temps polynomial. - Le tri des créneaux évite de comparer toutes les paires : le nombre de clauses reste proche du nombre réel de chevauchements. - Avec trois créneaux par élève, la clause « au moins un créneau » aurait trois littéraux. Le cas général 3-SAT est NP-complet : la méthode par composantes fortement connexes ne s'applique plus. %% nav-debut : généré par gen_navigation.py, ne pas modifier à la main %% > [!nav] > ↩ [[Code et Développement/Programmation/Optimisation de problème/Optimisation de problème|Accueil · Optimisation de problème]] %% nav-fin %%