From 3f54ad3f6e4dc85d5a86d339151d09a0b8425379 Mon Sep 17 00:00:00 2001 From: gothictomato Date: Sat, 5 Apr 2025 22:32:13 -0400 Subject: [PATCH] Commit most recent local copy --- 1lit.cnf | 4101 +++++++++++++++++++++++++++++++++++++++++++++++++++ csflocref.c | 630 ++++++++ csflocref.h | 5 + githubtoken | 1 + gpusolver.c | 4 +- main.c | 8 +- psatv0.cl | 278 ++++ 7 files changed, 5021 insertions(+), 6 deletions(-) create mode 100644 1lit.cnf create mode 100644 csflocref.c create mode 100644 csflocref.h create mode 100644 githubtoken create mode 100644 psatv0.cl diff --git a/1lit.cnf b/1lit.cnf new file mode 100644 index 0000000..5dc193c --- /dev/null +++ b/1lit.cnf @@ -0,0 +1,4101 @@ +c +c start with comments +c +c +p cnf 4096 4096 +-1 0 +-2 0 +3 0 +4 0 +5 0 +6 0 +7 0 +-8 0 +-9 0 +10 0 +-11 0 +-12 0 +13 0 +-14 0 +-15 0 +16 0 +17 0 +-18 0 +-19 0 +-20 0 +-21 0 +-22 0 +-23 0 +-24 0 +25 0 +26 0 +-27 0 +28 0 +-29 0 +-30 0 +-31 0 +32 0 +-33 0 +-34 0 +35 0 +-36 0 +37 0 +-38 0 +-39 0 +40 0 +-41 0 +-42 0 +43 0 +44 0 +-45 0 +46 0 +-47 0 +48 0 +49 0 +-50 0 +51 0 +52 0 +-53 0 +54 0 +55 0 +56 0 +-57 0 +-58 0 +-59 0 +-60 0 +-61 0 +-62 0 +-63 0 +-64 0 +-65 0 +66 0 +-67 0 +-68 0 +69 0 +-70 0 +71 0 +72 0 +-73 0 +74 0 +-75 0 +-76 0 +-77 0 +-78 0 +79 0 +-80 0 +-81 0 +-82 0 +83 0 +-84 0 +85 0 +86 0 +87 0 +-88 0 +89 0 +90 0 +-91 0 +92 0 +-93 0 +-94 0 +95 0 +-96 0 +97 0 +-98 0 +-99 0 +100 0 +-101 0 +-102 0 +-103 0 +104 0 +105 0 +106 0 +107 0 +108 0 +109 0 +110 0 +111 0 +-112 0 +113 0 +114 0 +-115 0 +116 0 +-117 0 +-118 0 +119 0 +120 0 +121 0 +122 0 +-123 0 +124 0 +-125 0 +126 0 +-127 0 +128 0 +129 0 +-130 0 +-131 0 +-132 0 +-133 0 +134 0 +135 0 +136 0 +-137 0 +-138 0 +139 0 +140 0 +141 0 +-142 0 +143 0 +144 0 +145 0 +-146 0 +-147 0 +148 0 +-149 0 +150 0 +-151 0 +152 0 +-153 0 +-154 0 +155 0 +-156 0 +-157 0 +158 0 +-159 0 +160 0 +161 0 +-162 0 +163 0 +-164 0 +165 0 +-166 0 +167 0 +168 0 +169 0 +-170 0 +171 0 +-172 0 +173 0 +-174 0 +175 0 +-176 0 +-177 0 +178 0 +-179 0 +-180 0 +-181 0 +-182 0 +-183 0 +184 0 +185 0 +186 0 +187 0 +188 0 +-189 0 +190 0 +-191 0 +192 0 +-193 0 +-194 0 +195 0 +196 0 +-197 0 +198 0 +199 0 +200 0 +201 0 +-202 0 +-203 0 +-204 0 +-205 0 +206 0 +207 0 +208 0 +209 0 +210 0 +211 0 +212 0 +213 0 +214 0 +-215 0 +-216 0 +-217 0 +-218 0 +219 0 +-220 0 +221 0 +-222 0 +-223 0 +224 0 +-225 0 +226 0 +227 0 +-228 0 +-229 0 +-230 0 +-231 0 +-232 0 +-233 0 +-234 0 +-235 0 +-236 0 +237 0 +238 0 +239 0 +-240 0 +-241 0 +242 0 +-243 0 +-244 0 +-245 0 +-246 0 +-247 0 +248 0 +-249 0 +-250 0 +251 0 +-252 0 +-253 0 +254 0 +255 0 +-256 0 +257 0 +258 0 +-259 0 +260 0 +261 0 +-262 0 +263 0 +264 0 +265 0 +266 0 +267 0 +-268 0 +269 0 +270 0 +271 0 +-272 0 +273 0 +-274 0 +-275 0 +-276 0 +-277 0 +278 0 +279 0 +-280 0 +281 0 +-282 0 +283 0 +-284 0 +-285 0 +-286 0 +287 0 +-288 0 +289 0 +-290 0 +291 0 +-292 0 +-293 0 +-294 0 +295 0 +296 0 +297 0 +-298 0 +-299 0 +-300 0 +301 0 +302 0 +303 0 +-304 0 +-305 0 +306 0 +-307 0 +-308 0 +-309 0 +-310 0 +311 0 +312 0 +-313 0 +-314 0 +-315 0 +316 0 +-317 0 +318 0 +319 0 +320 0 +321 0 +322 0 +-323 0 +324 0 +325 0 +326 0 +327 0 +328 0 +-329 0 +330 0 +331 0 +332 0 +-333 0 +-334 0 +-335 0 +-336 0 +337 0 +-338 0 +339 0 +-340 0 +-341 0 +-342 0 +343 0 +344 0 +-345 0 +346 0 +-347 0 +348 0 +349 0 +350 0 +-351 0 +-352 0 +-353 0 +-354 0 +-355 0 +-356 0 +-357 0 +358 0 +359 0 +-360 0 +-361 0 +-362 0 +363 0 +-364 0 +365 0 +366 0 +367 0 +-368 0 +-369 0 +-370 0 +-371 0 +-372 0 +-373 0 +-374 0 +375 0 +-376 0 +377 0 +378 0 +379 0 +-380 0 +381 0 +-382 0 +383 0 +384 0 +-385 0 +386 0 +387 0 +-388 0 +-389 0 +-390 0 +-391 0 +-392 0 +393 0 +-394 0 +-395 0 +-396 0 +397 0 +398 0 +-399 0 +400 0 +401 0 +402 0 +-403 0 +404 0 +405 0 +406 0 +-407 0 +-408 0 +409 0 +410 0 +411 0 +-412 0 +413 0 +-414 0 +415 0 +-416 0 +417 0 +418 0 +-419 0 +420 0 +421 0 +422 0 +423 0 +-424 0 +425 0 +426 0 +-427 0 +-428 0 +429 0 +430 0 +-431 0 +-432 0 +-433 0 +-434 0 +-435 0 +436 0 +437 0 +-438 0 +439 0 +-440 0 +441 0 +-442 0 +-443 0 +444 0 +-445 0 +-446 0 +447 0 +448 0 +449 0 +450 0 +-451 0 +-452 0 +-453 0 +454 0 +455 0 +456 0 +457 0 +458 0 +-459 0 +-460 0 +-461 0 +-462 0 +-463 0 +-464 0 +-465 0 +-466 0 +467 0 +468 0 +-469 0 +470 0 +-471 0 +-472 0 +473 0 +-474 0 +475 0 +-476 0 +-477 0 +-478 0 +479 0 +480 0 +481 0 +-482 0 +-483 0 +-484 0 +485 0 +486 0 +487 0 +-488 0 +-489 0 +490 0 +-491 0 +492 0 +493 0 +494 0 +495 0 +496 0 +497 0 +498 0 +499 0 +-500 0 +-501 0 +502 0 +-503 0 +504 0 +505 0 +506 0 +507 0 +-508 0 +509 0 +510 0 +511 0 +-512 0 +513 0 +-514 0 +-515 0 +-516 0 +517 0 +518 0 +519 0 +520 0 +-521 0 +522 0 +523 0 +524 0 +-525 0 +526 0 +527 0 +528 0 +-529 0 +530 0 +-531 0 +-532 0 +-533 0 +-534 0 +-535 0 +-536 0 +-537 0 +538 0 +-539 0 +540 0 +-541 0 +542 0 +543 0 +544 0 +-545 0 +546 0 +-547 0 +548 0 +549 0 +550 0 +-551 0 +552 0 +-553 0 +554 0 +555 0 +-556 0 +557 0 +-558 0 +559 0 +560 0 +-561 0 +562 0 +563 0 +-564 0 +565 0 +566 0 +-567 0 +568 0 +-569 0 +-570 0 +-571 0 +-572 0 +-573 0 +-574 0 +-575 0 +-576 0 +577 0 +-578 0 +579 0 +-580 0 +581 0 +582 0 +-583 0 +584 0 +585 0 +586 0 +587 0 +-588 0 +589 0 +-590 0 +591 0 +592 0 +593 0 +-594 0 +595 0 +596 0 +597 0 +598 0 +-599 0 +600 0 +-601 0 +602 0 +603 0 +-604 0 +605 0 +606 0 +-607 0 +-608 0 +609 0 +610 0 +611 0 +-612 0 +-613 0 +614 0 +615 0 +616 0 +-617 0 +-618 0 +619 0 +620 0 +-621 0 +-622 0 +623 0 +-624 0 +-625 0 +-626 0 +627 0 +628 0 +-629 0 +630 0 +-631 0 +-632 0 +-633 0 +-634 0 +-635 0 +636 0 +637 0 +-638 0 +-639 0 +640 0 +641 0 +642 0 +643 0 +644 0 +-645 0 +646 0 +647 0 +-648 0 +649 0 +-650 0 +651 0 +-652 0 +653 0 +-654 0 +-655 0 +656 0 +657 0 +658 0 +659 0 +660 0 +-661 0 +662 0 +663 0 +664 0 +665 0 +666 0 +-667 0 +668 0 +669 0 +-670 0 +-671 0 +-672 0 +673 0 +674 0 +675 0 +676 0 +-677 0 +-678 0 +679 0 +-680 0 +681 0 +682 0 +-683 0 +-684 0 +685 0 +-686 0 +687 0 +-688 0 +689 0 +-690 0 +691 0 +692 0 +-693 0 +-694 0 +-695 0 +696 0 +697 0 +698 0 +-699 0 +-700 0 +701 0 +-702 0 +-703 0 +704 0 +-705 0 +-706 0 +-707 0 +-708 0 +-709 0 +-710 0 +-711 0 +712 0 +713 0 +-714 0 +715 0 +-716 0 +-717 0 +718 0 +719 0 +720 0 +721 0 +-722 0 +723 0 +724 0 +725 0 +726 0 +727 0 +-728 0 +-729 0 +730 0 +731 0 +-732 0 +-733 0 +734 0 +735 0 +-736 0 +737 0 +738 0 +-739 0 +-740 0 +741 0 +742 0 +743 0 +-744 0 +745 0 +746 0 +747 0 +-748 0 +-749 0 +-750 0 +751 0 +752 0 +-753 0 +-754 0 +755 0 +756 0 +-757 0 +-758 0 +-759 0 +-760 0 +761 0 +762 0 +-763 0 +764 0 +-765 0 +766 0 +767 0 +-768 0 +769 0 +770 0 +-771 0 +-772 0 +773 0 +-774 0 +775 0 +-776 0 +-777 0 +778 0 +779 0 +-780 0 +781 0 +-782 0 +-783 0 +-784 0 +785 0 +-786 0 +-787 0 +788 0 +-789 0 +-790 0 +-791 0 +792 0 +793 0 +794 0 +-795 0 +-796 0 +-797 0 +-798 0 +799 0 +-800 0 +801 0 +802 0 +-803 0 +-804 0 +-805 0 +-806 0 +-807 0 +-808 0 +809 0 +810 0 +-811 0 +-812 0 +813 0 +-814 0 +-815 0 +-816 0 +817 0 +-818 0 +819 0 +820 0 +-821 0 +822 0 +-823 0 +824 0 +825 0 +826 0 +-827 0 +828 0 +829 0 +830 0 +831 0 +-832 0 +-833 0 +-834 0 +-835 0 +-836 0 +-837 0 +-838 0 +839 0 +840 0 +-841 0 +842 0 +843 0 +844 0 +-845 0 +846 0 +-847 0 +848 0 +-849 0 +850 0 +-851 0 +-852 0 +853 0 +854 0 +-855 0 +-856 0 +-857 0 +-858 0 +859 0 +860 0 +861 0 +862 0 +863 0 +864 0 +865 0 +866 0 +-867 0 +868 0 +869 0 +870 0 +-871 0 +872 0 +-873 0 +874 0 +875 0 +-876 0 +-877 0 +878 0 +879 0 +-880 0 +-881 0 +-882 0 +883 0 +884 0 +885 0 +886 0 +887 0 +888 0 +889 0 +890 0 +-891 0 +-892 0 +-893 0 +894 0 +895 0 +896 0 +-897 0 +898 0 +-899 0 +900 0 +-901 0 +-902 0 +903 0 +904 0 +905 0 +-906 0 +907 0 +908 0 +909 0 +910 0 +-911 0 +912 0 +913 0 +914 0 +915 0 +-916 0 +-917 0 +-918 0 +919 0 +920 0 +921 0 +922 0 +923 0 +924 0 +-925 0 +-926 0 +-927 0 +-928 0 +-929 0 +-930 0 +931 0 +-932 0 +-933 0 +-934 0 +935 0 +936 0 +-937 0 +938 0 +939 0 +940 0 +-941 0 +942 0 +943 0 +944 0 +-945 0 +-946 0 +947 0 +-948 0 +-949 0 +-950 0 +951 0 +-952 0 +953 0 +-954 0 +955 0 +956 0 +-957 0 +-958 0 +959 0 +-960 0 +-961 0 +-962 0 +963 0 +964 0 +965 0 +-966 0 +-967 0 +968 0 +969 0 +970 0 +971 0 +972 0 +-973 0 +-974 0 +-975 0 +-976 0 +-977 0 +978 0 +-979 0 +-980 0 +981 0 +982 0 +-983 0 +-984 0 +985 0 +-986 0 +987 0 +-988 0 +-989 0 +-990 0 +-991 0 +-992 0 +993 0 +994 0 +995 0 +-996 0 +-997 0 +-998 0 +999 0 +1000 0 +1001 0 +-1002 0 +1003 0 +-1004 0 +-1005 0 +1006 0 +-1007 0 +-1008 0 +1009 0 +1010 0 +1011 0 +-1012 0 +-1013 0 +1014 0 +1015 0 +-1016 0 +1017 0 +-1018 0 +-1019 0 +1020 0 +1021 0 +-1022 0 +-1023 0 +-1024 0 +-1025 0 +-1026 0 +-1027 0 +1028 0 +-1029 0 +1030 0 +-1031 0 +-1032 0 +1033 0 +1034 0 +1035 0 +-1036 0 +1037 0 +-1038 0 +1039 0 +-1040 0 +-1041 0 +1042 0 +-1043 0 +-1044 0 +-1045 0 +1046 0 +-1047 0 +1048 0 +-1049 0 +1050 0 +-1051 0 +1052 0 +1053 0 +-1054 0 +-1055 0 +1056 0 +1057 0 +1058 0 +-1059 0 +1060 0 +-1061 0 +-1062 0 +1063 0 +1064 0 +1065 0 +1066 0 +1067 0 +-1068 0 +1069 0 +-1070 0 +-1071 0 +-1072 0 +1073 0 +1074 0 +-1075 0 +-1076 0 +-1077 0 +-1078 0 +1079 0 +-1080 0 +1081 0 +1082 0 +1083 0 +1084 0 +-1085 0 +-1086 0 +-1087 0 +1088 0 +1089 0 +-1090 0 +-1091 0 +1092 0 +1093 0 +1094 0 +-1095 0 +-1096 0 +-1097 0 +1098 0 +1099 0 +-1100 0 +-1101 0 +1102 0 +-1103 0 +1104 0 +-1105 0 +-1106 0 +1107 0 +1108 0 +1109 0 +-1110 0 +1111 0 +-1112 0 +-1113 0 +1114 0 +1115 0 +-1116 0 +1117 0 +1118 0 +1119 0 +-1120 0 +-1121 0 +1122 0 +1123 0 +1124 0 +-1125 0 +1126 0 +1127 0 +1128 0 +-1129 0 +-1130 0 +1131 0 +-1132 0 +-1133 0 +1134 0 +-1135 0 +-1136 0 +1137 0 +1138 0 +1139 0 +-1140 0 +-1141 0 +1142 0 +1143 0 +-1144 0 +-1145 0 +-1146 0 +-1147 0 +1148 0 +-1149 0 +1150 0 +1151 0 +-1152 0 +-1153 0 +-1154 0 +1155 0 +-1156 0 +1157 0 +-1158 0 +1159 0 +1160 0 +1161 0 +-1162 0 +-1163 0 +1164 0 +1165 0 +-1166 0 +1167 0 +1168 0 +1169 0 +1170 0 +1171 0 +1172 0 +-1173 0 +-1174 0 +1175 0 +-1176 0 +1177 0 +1178 0 +1179 0 +1180 0 +-1181 0 +-1182 0 +1183 0 +-1184 0 +-1185 0 +-1186 0 +1187 0 +1188 0 +-1189 0 +-1190 0 +-1191 0 +1192 0 +1193 0 +-1194 0 +-1195 0 +-1196 0 +-1197 0 +-1198 0 +1199 0 +-1200 0 +1201 0 +1202 0 +1203 0 +1204 0 +1205 0 +1206 0 +1207 0 +-1208 0 +-1209 0 +-1210 0 +1211 0 +1212 0 +-1213 0 +-1214 0 +1215 0 +-1216 0 +-1217 0 +-1218 0 +1219 0 +1220 0 +1221 0 +1222 0 +-1223 0 +-1224 0 +-1225 0 +1226 0 +-1227 0 +-1228 0 +1229 0 +-1230 0 +-1231 0 +-1232 0 +1233 0 +-1234 0 +1235 0 +-1236 0 +1237 0 +-1238 0 +1239 0 +1240 0 +-1241 0 +-1242 0 +-1243 0 +-1244 0 +1245 0 +-1246 0 +-1247 0 +1248 0 +-1249 0 +1250 0 +-1251 0 +1252 0 +-1253 0 +1254 0 +1255 0 +-1256 0 +-1257 0 +-1258 0 +1259 0 +1260 0 +-1261 0 +1262 0 +1263 0 +1264 0 +1265 0 +-1266 0 +1267 0 +-1268 0 +-1269 0 +-1270 0 +-1271 0 +-1272 0 +1273 0 +-1274 0 +-1275 0 +-1276 0 +-1277 0 +-1278 0 +1279 0 +1280 0 +1281 0 +1282 0 +-1283 0 +-1284 0 +-1285 0 +1286 0 +-1287 0 +-1288 0 +-1289 0 +-1290 0 +-1291 0 +-1292 0 +-1293 0 +1294 0 +-1295 0 +1296 0 +1297 0 +1298 0 +-1299 0 +1300 0 +1301 0 +1302 0 +1303 0 +-1304 0 +1305 0 +-1306 0 +1307 0 +1308 0 +1309 0 +1310 0 +1311 0 +1312 0 +-1313 0 +1314 0 +1315 0 +-1316 0 +-1317 0 +1318 0 +1319 0 +-1320 0 +1321 0 +1322 0 +-1323 0 +1324 0 +-1325 0 +1326 0 +1327 0 +1328 0 +-1329 0 +1330 0 +-1331 0 +1332 0 +-1333 0 +-1334 0 +-1335 0 +-1336 0 +-1337 0 +1338 0 +1339 0 +-1340 0 +-1341 0 +1342 0 +1343 0 +-1344 0 +-1345 0 +-1346 0 +1347 0 +1348 0 +1349 0 +-1350 0 +1351 0 +-1352 0 +1353 0 +-1354 0 +1355 0 +1356 0 +1357 0 +-1358 0 +-1359 0 +1360 0 +1361 0 +-1362 0 +-1363 0 +-1364 0 +-1365 0 +-1366 0 +-1367 0 +1368 0 +-1369 0 +1370 0 +1371 0 +-1372 0 +-1373 0 +-1374 0 +1375 0 +1376 0 +-1377 0 +-1378 0 +-1379 0 +1380 0 +-1381 0 +1382 0 +1383 0 +1384 0 +1385 0 +-1386 0 +-1387 0 +-1388 0 +1389 0 +-1390 0 +1391 0 +-1392 0 +-1393 0 +-1394 0 +-1395 0 +1396 0 +-1397 0 +-1398 0 +-1399 0 +-1400 0 +-1401 0 +1402 0 +1403 0 +-1404 0 +1405 0 +-1406 0 +1407 0 +1408 0 +-1409 0 +1410 0 +-1411 0 +-1412 0 +1413 0 +1414 0 +1415 0 +-1416 0 +1417 0 +1418 0 +1419 0 +-1420 0 +1421 0 +-1422 0 +1423 0 +1424 0 +-1425 0 +1426 0 +-1427 0 +1428 0 +-1429 0 +-1430 0 +1431 0 +-1432 0 +1433 0 +-1434 0 +-1435 0 +-1436 0 +-1437 0 +-1438 0 +1439 0 +-1440 0 +1441 0 +1442 0 +-1443 0 +-1444 0 +-1445 0 +1446 0 +1447 0 +-1448 0 +-1449 0 +-1450 0 +-1451 0 +1452 0 +-1453 0 +1454 0 +1455 0 +1456 0 +1457 0 +1458 0 +-1459 0 +1460 0 +-1461 0 +1462 0 +1463 0 +1464 0 +-1465 0 +1466 0 +-1467 0 +-1468 0 +1469 0 +1470 0 +1471 0 +1472 0 +1473 0 +1474 0 +1475 0 +1476 0 +1477 0 +-1478 0 +1479 0 +1480 0 +-1481 0 +-1482 0 +1483 0 +1484 0 +1485 0 +-1486 0 +-1487 0 +-1488 0 +1489 0 +-1490 0 +1491 0 +1492 0 +1493 0 +-1494 0 +1495 0 +1496 0 +-1497 0 +1498 0 +-1499 0 +1500 0 +-1501 0 +1502 0 +-1503 0 +1504 0 +-1505 0 +-1506 0 +1507 0 +1508 0 +-1509 0 +-1510 0 +1511 0 +1512 0 +-1513 0 +-1514 0 +-1515 0 +-1516 0 +-1517 0 +-1518 0 +-1519 0 +1520 0 +-1521 0 +-1522 0 +1523 0 +1524 0 +-1525 0 +-1526 0 +1527 0 +-1528 0 +1529 0 +1530 0 +-1531 0 +1532 0 +-1533 0 +-1534 0 +1535 0 +-1536 0 +-1537 0 +-1538 0 +-1539 0 +-1540 0 +1541 0 +1542 0 +1543 0 +-1544 0 +1545 0 +-1546 0 +1547 0 +-1548 0 +1549 0 +-1550 0 +-1551 0 +-1552 0 +-1553 0 +-1554 0 +-1555 0 +-1556 0 +-1557 0 +1558 0 +1559 0 +1560 0 +1561 0 +1562 0 +-1563 0 +-1564 0 +1565 0 +-1566 0 +1567 0 +1568 0 +-1569 0 +-1570 0 +-1571 0 +1572 0 +1573 0 +1574 0 +1575 0 +-1576 0 +1577 0 +1578 0 +-1579 0 +1580 0 +1581 0 +-1582 0 +1583 0 +-1584 0 +1585 0 +-1586 0 +-1587 0 +1588 0 +1589 0 +-1590 0 +-1591 0 +-1592 0 +1593 0 +1594 0 +1595 0 +1596 0 +1597 0 +-1598 0 +-1599 0 +-1600 0 +-1601 0 +-1602 0 +1603 0 +1604 0 +1605 0 +1606 0 +1607 0 +1608 0 +-1609 0 +1610 0 +-1611 0 +1612 0 +-1613 0 +1614 0 +1615 0 +1616 0 +1617 0 +-1618 0 +-1619 0 +1620 0 +-1621 0 +1622 0 +1623 0 +1624 0 +-1625 0 +-1626 0 +-1627 0 +1628 0 +1629 0 +1630 0 +1631 0 +1632 0 +1633 0 +1634 0 +1635 0 +1636 0 +-1637 0 +-1638 0 +-1639 0 +-1640 0 +-1641 0 +-1642 0 +1643 0 +-1644 0 +1645 0 +1646 0 +1647 0 +1648 0 +1649 0 +1650 0 +-1651 0 +1652 0 +-1653 0 +1654 0 +-1655 0 +-1656 0 +-1657 0 +1658 0 +-1659 0 +1660 0 +-1661 0 +1662 0 +-1663 0 +1664 0 +-1665 0 +1666 0 +-1667 0 +-1668 0 +-1669 0 +-1670 0 +-1671 0 +-1672 0 +-1673 0 +-1674 0 +-1675 0 +-1676 0 +1677 0 +1678 0 +1679 0 +-1680 0 +-1681 0 +1682 0 +1683 0 +1684 0 +-1685 0 +1686 0 +1687 0 +-1688 0 +-1689 0 +1690 0 +1691 0 +-1692 0 +1693 0 +-1694 0 +-1695 0 +1696 0 +1697 0 +-1698 0 +-1699 0 +1700 0 +1701 0 +-1702 0 +1703 0 +1704 0 +-1705 0 +1706 0 +1707 0 +1708 0 +-1709 0 +-1710 0 +1711 0 +1712 0 +1713 0 +-1714 0 +-1715 0 +-1716 0 +-1717 0 +1718 0 +-1719 0 +-1720 0 +1721 0 +-1722 0 +1723 0 +-1724 0 +-1725 0 +1726 0 +1727 0 +1728 0 +1729 0 +1730 0 +1731 0 +-1732 0 +-1733 0 +-1734 0 +-1735 0 +-1736 0 +-1737 0 +1738 0 +-1739 0 +-1740 0 +-1741 0 +1742 0 +1743 0 +1744 0 +-1745 0 +1746 0 +1747 0 +-1748 0 +1749 0 +-1750 0 +-1751 0 +-1752 0 +-1753 0 +1754 0 +-1755 0 +-1756 0 +-1757 0 +1758 0 +1759 0 +-1760 0 +1761 0 +-1762 0 +-1763 0 +1764 0 +1765 0 +-1766 0 +1767 0 +1768 0 +-1769 0 +1770 0 +1771 0 +-1772 0 +1773 0 +1774 0 +1775 0 +1776 0 +-1777 0 +1778 0 +1779 0 +1780 0 +1781 0 +1782 0 +1783 0 +1784 0 +1785 0 +1786 0 +1787 0 +1788 0 +1789 0 +-1790 0 +1791 0 +-1792 0 +1793 0 +-1794 0 +-1795 0 +-1796 0 +-1797 0 +1798 0 +-1799 0 +-1800 0 +1801 0 +1802 0 +1803 0 +-1804 0 +1805 0 +-1806 0 +1807 0 +-1808 0 +1809 0 +-1810 0 +1811 0 +1812 0 +-1813 0 +1814 0 +-1815 0 +1816 0 +1817 0 +-1818 0 +1819 0 +-1820 0 +-1821 0 +1822 0 +1823 0 +-1824 0 +1825 0 +1826 0 +-1827 0 +-1828 0 +-1829 0 +-1830 0 +-1831 0 +1832 0 +1833 0 +1834 0 +-1835 0 +-1836 0 +1837 0 +1838 0 +-1839 0 +-1840 0 +-1841 0 +1842 0 +-1843 0 +-1844 0 +1845 0 +-1846 0 +1847 0 +-1848 0 +1849 0 +1850 0 +-1851 0 +1852 0 +-1853 0 +-1854 0 +1855 0 +1856 0 +1857 0 +1858 0 +1859 0 +-1860 0 +1861 0 +-1862 0 +1863 0 +1864 0 +1865 0 +1866 0 +1867 0 +1868 0 +1869 0 +-1870 0 +1871 0 +1872 0 +1873 0 +1874 0 +1875 0 +-1876 0 +-1877 0 +-1878 0 +-1879 0 +1880 0 +1881 0 +1882 0 +-1883 0 +1884 0 +1885 0 +1886 0 +1887 0 +-1888 0 +-1889 0 +-1890 0 +-1891 0 +1892 0 +-1893 0 +-1894 0 +-1895 0 +-1896 0 +1897 0 +-1898 0 +1899 0 +-1900 0 +-1901 0 +-1902 0 +1903 0 +1904 0 +-1905 0 +-1906 0 +-1907 0 +-1908 0 +1909 0 +-1910 0 +1911 0 +-1912 0 +1913 0 +1914 0 +-1915 0 +-1916 0 +-1917 0 +1918 0 +1919 0 +-1920 0 +1921 0 +1922 0 +1923 0 +-1924 0 +1925 0 +-1926 0 +-1927 0 +1928 0 +-1929 0 +1930 0 +1931 0 +-1932 0 +1933 0 +1934 0 +1935 0 +1936 0 +1937 0 +1938 0 +1939 0 +-1940 0 +-1941 0 +-1942 0 +1943 0 +1944 0 +1945 0 +1946 0 +-1947 0 +1948 0 +-1949 0 +1950 0 +1951 0 +1952 0 +-1953 0 +1954 0 +1955 0 +-1956 0 +1957 0 +1958 0 +1959 0 +1960 0 +-1961 0 +-1962 0 +1963 0 +-1964 0 +1965 0 +-1966 0 +1967 0 +1968 0 +-1969 0 +1970 0 +1971 0 +-1972 0 +1973 0 +-1974 0 +1975 0 +1976 0 +1977 0 +1978 0 +-1979 0 +1980 0 +-1981 0 +-1982 0 +1983 0 +1984 0 +1985 0 +-1986 0 +1987 0 +-1988 0 +-1989 0 +-1990 0 +1991 0 +-1992 0 +-1993 0 +-1994 0 +-1995 0 +-1996 0 +-1997 0 +-1998 0 +1999 0 +-2000 0 +2001 0 +-2002 0 +-2003 0 +-2004 0 +2005 0 +-2006 0 +2007 0 +-2008 0 +2009 0 +-2010 0 +-2011 0 +-2012 0 +-2013 0 +2014 0 +2015 0 +2016 0 +2017 0 +-2018 0 +2019 0 +2020 0 +-2021 0 +-2022 0 +-2023 0 +-2024 0 +-2025 0 +-2026 0 +-2027 0 +-2028 0 +-2029 0 +2030 0 +2031 0 +2032 0 +-2033 0 +2034 0 +-2035 0 +2036 0 +2037 0 +2038 0 +2039 0 +2040 0 +2041 0 +2042 0 +2043 0 +2044 0 +-2045 0 +-2046 0 +-2047 0 +-2048 0 +-2049 0 +2050 0 +-2051 0 +2052 0 +-2053 0 +2054 0 +-2055 0 +-2056 0 +2057 0 +2058 0 +2059 0 +-2060 0 +2061 0 +-2062 0 +-2063 0 +-2064 0 +-2065 0 +-2066 0 +-2067 0 +2068 0 +-2069 0 +-2070 0 +2071 0 +-2072 0 +-2073 0 +-2074 0 +2075 0 +-2076 0 +2077 0 +2078 0 +-2079 0 +2080 0 +-2081 0 +-2082 0 +2083 0 +-2084 0 +2085 0 +2086 0 +2087 0 +-2088 0 +2089 0 +-2090 0 +-2091 0 +-2092 0 +2093 0 +-2094 0 +-2095 0 +2096 0 +-2097 0 +-2098 0 +-2099 0 +-2100 0 +-2101 0 +2102 0 +2103 0 +-2104 0 +-2105 0 +-2106 0 +-2107 0 +2108 0 +2109 0 +-2110 0 +2111 0 +2112 0 +-2113 0 +-2114 0 +-2115 0 +2116 0 +2117 0 +2118 0 +2119 0 +-2120 0 +2121 0 +-2122 0 +-2123 0 +-2124 0 +-2125 0 +-2126 0 +2127 0 +2128 0 +-2129 0 +2130 0 +2131 0 +2132 0 +2133 0 +-2134 0 +2135 0 +2136 0 +2137 0 +-2138 0 +-2139 0 +-2140 0 +-2141 0 +2142 0 +-2143 0 +2144 0 +2145 0 +-2146 0 +-2147 0 +2148 0 +2149 0 +-2150 0 +2151 0 +-2152 0 +-2153 0 +-2154 0 +2155 0 +-2156 0 +-2157 0 +-2158 0 +2159 0 +2160 0 +-2161 0 +2162 0 +-2163 0 +2164 0 +2165 0 +2166 0 +-2167 0 +-2168 0 +2169 0 +-2170 0 +2171 0 +-2172 0 +-2173 0 +2174 0 +2175 0 +2176 0 +2177 0 +2178 0 +-2179 0 +-2180 0 +2181 0 +-2182 0 +-2183 0 +2184 0 +-2185 0 +2186 0 +-2187 0 +-2188 0 +-2189 0 +2190 0 +2191 0 +-2192 0 +-2193 0 +2194 0 +2195 0 +-2196 0 +2197 0 +2198 0 +-2199 0 +-2200 0 +2201 0 +2202 0 +-2203 0 +2204 0 +-2205 0 +2206 0 +2207 0 +2208 0 +2209 0 +2210 0 +2211 0 +-2212 0 +2213 0 +-2214 0 +-2215 0 +2216 0 +2217 0 +-2218 0 +-2219 0 +2220 0 +2221 0 +2222 0 +2223 0 +-2224 0 +2225 0 +-2226 0 +-2227 0 +-2228 0 +2229 0 +-2230 0 +-2231 0 +2232 0 +-2233 0 +2234 0 +-2235 0 +-2236 0 +-2237 0 +2238 0 +-2239 0 +2240 0 +2241 0 +2242 0 +-2243 0 +-2244 0 +2245 0 +-2246 0 +-2247 0 +2248 0 +-2249 0 +-2250 0 +-2251 0 +2252 0 +2253 0 +-2254 0 +2255 0 +-2256 0 +-2257 0 +2258 0 +-2259 0 +-2260 0 +-2261 0 +2262 0 +2263 0 +-2264 0 +-2265 0 +2266 0 +-2267 0 +-2268 0 +2269 0 +-2270 0 +-2271 0 +-2272 0 +-2273 0 +-2274 0 +-2275 0 +2276 0 +-2277 0 +-2278 0 +-2279 0 +-2280 0 +-2281 0 +2282 0 +2283 0 +-2284 0 +2285 0 +2286 0 +-2287 0 +2288 0 +-2289 0 +2290 0 +2291 0 +-2292 0 +-2293 0 +-2294 0 +-2295 0 +-2296 0 +-2297 0 +2298 0 +-2299 0 +2300 0 +2301 0 +-2302 0 +2303 0 +2304 0 +-2305 0 +2306 0 +2307 0 +-2308 0 +-2309 0 +2310 0 +2311 0 +2312 0 +-2313 0 +-2314 0 +-2315 0 +-2316 0 +2317 0 +-2318 0 +-2319 0 +-2320 0 +2321 0 +-2322 0 +-2323 0 +-2324 0 +-2325 0 +-2326 0 +-2327 0 +2328 0 +-2329 0 +2330 0 +-2331 0 +2332 0 +-2333 0 +-2334 0 +2335 0 +-2336 0 +2337 0 +-2338 0 +-2339 0 +2340 0 +2341 0 +2342 0 +2343 0 +2344 0 +2345 0 +2346 0 +2347 0 +2348 0 +2349 0 +2350 0 +2351 0 +2352 0 +2353 0 +2354 0 +2355 0 +2356 0 +2357 0 +2358 0 +2359 0 +-2360 0 +2361 0 +2362 0 +2363 0 +2364 0 +2365 0 +-2366 0 +2367 0 +2368 0 +-2369 0 +2370 0 +-2371 0 +2372 0 +-2373 0 +2374 0 +-2375 0 +2376 0 +-2377 0 +2378 0 +-2379 0 +-2380 0 +-2381 0 +2382 0 +2383 0 +2384 0 +-2385 0 +-2386 0 +2387 0 +-2388 0 +2389 0 +-2390 0 +-2391 0 +-2392 0 +2393 0 +2394 0 +2395 0 +-2396 0 +2397 0 +-2398 0 +2399 0 +2400 0 +2401 0 +-2402 0 +-2403 0 +2404 0 +2405 0 +-2406 0 +2407 0 +-2408 0 +2409 0 +2410 0 +-2411 0 +2412 0 +2413 0 +2414 0 +-2415 0 +2416 0 +2417 0 +2418 0 +2419 0 +-2420 0 +2421 0 +2422 0 +2423 0 +-2424 0 +-2425 0 +-2426 0 +2427 0 +2428 0 +2429 0 +-2430 0 +-2431 0 +-2432 0 +-2433 0 +-2434 0 +-2435 0 +-2436 0 +-2437 0 +2438 0 +-2439 0 +2440 0 +-2441 0 +-2442 0 +-2443 0 +2444 0 +2445 0 +2446 0 +2447 0 +-2448 0 +-2449 0 +-2450 0 +-2451 0 +-2452 0 +-2453 0 +2454 0 +-2455 0 +-2456 0 +-2457 0 +2458 0 +-2459 0 +2460 0 +-2461 0 +-2462 0 +2463 0 +-2464 0 +2465 0 +2466 0 +-2467 0 +2468 0 +-2469 0 +-2470 0 +2471 0 +2472 0 +-2473 0 +2474 0 +-2475 0 +2476 0 +-2477 0 +2478 0 +2479 0 +2480 0 +-2481 0 +-2482 0 +2483 0 +-2484 0 +2485 0 +2486 0 +-2487 0 +2488 0 +2489 0 +-2490 0 +-2491 0 +2492 0 +2493 0 +-2494 0 +2495 0 +-2496 0 +2497 0 +-2498 0 +2499 0 +-2500 0 +-2501 0 +-2502 0 +2503 0 +2504 0 +-2505 0 +2506 0 +-2507 0 +-2508 0 +2509 0 +-2510 0 +2511 0 +2512 0 +-2513 0 +-2514 0 +2515 0 +2516 0 +-2517 0 +2518 0 +2519 0 +2520 0 +-2521 0 +2522 0 +-2523 0 +2524 0 +2525 0 +2526 0 +2527 0 +2528 0 +2529 0 +-2530 0 +2531 0 +-2532 0 +2533 0 +-2534 0 +2535 0 +2536 0 +2537 0 +2538 0 +2539 0 +-2540 0 +2541 0 +2542 0 +2543 0 +2544 0 +2545 0 +-2546 0 +2547 0 +2548 0 +-2549 0 +-2550 0 +-2551 0 +-2552 0 +2553 0 +-2554 0 +2555 0 +2556 0 +-2557 0 +-2558 0 +-2559 0 +2560 0 +-2561 0 +2562 0 +-2563 0 +2564 0 +-2565 0 +2566 0 +2567 0 +-2568 0 +2569 0 +-2570 0 +2571 0 +2572 0 +2573 0 +-2574 0 +2575 0 +2576 0 +-2577 0 +2578 0 +-2579 0 +2580 0 +-2581 0 +-2582 0 +2583 0 +-2584 0 +2585 0 +-2586 0 +2587 0 +-2588 0 +-2589 0 +-2590 0 +-2591 0 +-2592 0 +2593 0 +2594 0 +2595 0 +2596 0 +-2597 0 +-2598 0 +2599 0 +2600 0 +2601 0 +2602 0 +-2603 0 +-2604 0 +2605 0 +2606 0 +-2607 0 +-2608 0 +-2609 0 +-2610 0 +2611 0 +-2612 0 +2613 0 +2614 0 +-2615 0 +-2616 0 +2617 0 +2618 0 +-2619 0 +2620 0 +2621 0 +2622 0 +-2623 0 +-2624 0 +-2625 0 +2626 0 +2627 0 +-2628 0 +-2629 0 +2630 0 +-2631 0 +2632 0 +-2633 0 +-2634 0 +2635 0 +2636 0 +-2637 0 +2638 0 +2639 0 +-2640 0 +-2641 0 +2642 0 +2643 0 +2644 0 +-2645 0 +2646 0 +2647 0 +2648 0 +2649 0 +2650 0 +2651 0 +-2652 0 +-2653 0 +2654 0 +2655 0 +-2656 0 +-2657 0 +-2658 0 +2659 0 +-2660 0 +2661 0 +2662 0 +2663 0 +2664 0 +2665 0 +2666 0 +2667 0 +2668 0 +-2669 0 +-2670 0 +-2671 0 +-2672 0 +2673 0 +2674 0 +2675 0 +2676 0 +-2677 0 +-2678 0 +2679 0 +2680 0 +-2681 0 +-2682 0 +-2683 0 +-2684 0 +2685 0 +2686 0 +2687 0 +2688 0 +2689 0 +-2690 0 +-2691 0 +2692 0 +2693 0 +2694 0 +-2695 0 +-2696 0 +-2697 0 +2698 0 +-2699 0 +2700 0 +-2701 0 +-2702 0 +2703 0 +2704 0 +2705 0 +2706 0 +2707 0 +2708 0 +2709 0 +-2710 0 +2711 0 +2712 0 +-2713 0 +2714 0 +-2715 0 +2716 0 +-2717 0 +2718 0 +-2719 0 +2720 0 +2721 0 +-2722 0 +-2723 0 +-2724 0 +-2725 0 +2726 0 +-2727 0 +-2728 0 +-2729 0 +-2730 0 +2731 0 +-2732 0 +-2733 0 +2734 0 +-2735 0 +2736 0 +-2737 0 +2738 0 +2739 0 +2740 0 +2741 0 +-2742 0 +2743 0 +2744 0 +2745 0 +2746 0 +-2747 0 +2748 0 +-2749 0 +-2750 0 +-2751 0 +2752 0 +2753 0 +2754 0 +2755 0 +2756 0 +-2757 0 +2758 0 +2759 0 +-2760 0 +-2761 0 +2762 0 +2763 0 +-2764 0 +-2765 0 +2766 0 +-2767 0 +-2768 0 +-2769 0 +2770 0 +2771 0 +2772 0 +2773 0 +-2774 0 +-2775 0 +-2776 0 +2777 0 +-2778 0 +2779 0 +2780 0 +-2781 0 +2782 0 +-2783 0 +2784 0 +-2785 0 +2786 0 +-2787 0 +-2788 0 +2789 0 +-2790 0 +2791 0 +2792 0 +2793 0 +-2794 0 +2795 0 +2796 0 +2797 0 +2798 0 +2799 0 +2800 0 +-2801 0 +-2802 0 +-2803 0 +2804 0 +2805 0 +-2806 0 +2807 0 +-2808 0 +-2809 0 +-2810 0 +-2811 0 +-2812 0 +-2813 0 +-2814 0 +-2815 0 +-2816 0 +-2817 0 +-2818 0 +-2819 0 +-2820 0 +2821 0 +-2822 0 +-2823 0 +2824 0 +2825 0 +-2826 0 +2827 0 +2828 0 +-2829 0 +2830 0 +2831 0 +2832 0 +2833 0 +-2834 0 +-2835 0 +-2836 0 +-2837 0 +-2838 0 +2839 0 +2840 0 +-2841 0 +2842 0 +-2843 0 +2844 0 +2845 0 +2846 0 +-2847 0 +2848 0 +2849 0 +-2850 0 +2851 0 +2852 0 +-2853 0 +-2854 0 +-2855 0 +-2856 0 +-2857 0 +-2858 0 +2859 0 +2860 0 +2861 0 +-2862 0 +-2863 0 +-2864 0 +2865 0 +-2866 0 +-2867 0 +2868 0 +-2869 0 +2870 0 +-2871 0 +-2872 0 +-2873 0 +-2874 0 +-2875 0 +-2876 0 +2877 0 +-2878 0 +2879 0 +2880 0 +2881 0 +2882 0 +-2883 0 +2884 0 +2885 0 +-2886 0 +2887 0 +2888 0 +-2889 0 +-2890 0 +-2891 0 +2892 0 +2893 0 +2894 0 +2895 0 +-2896 0 +2897 0 +2898 0 +2899 0 +-2900 0 +2901 0 +2902 0 +-2903 0 +2904 0 +2905 0 +-2906 0 +2907 0 +-2908 0 +2909 0 +2910 0 +2911 0 +-2912 0 +-2913 0 +2914 0 +2915 0 +2916 0 +-2917 0 +2918 0 +-2919 0 +-2920 0 +2921 0 +2922 0 +-2923 0 +-2924 0 +-2925 0 +2926 0 +-2927 0 +2928 0 +2929 0 +2930 0 +2931 0 +-2932 0 +-2933 0 +-2934 0 +2935 0 +2936 0 +-2937 0 +2938 0 +-2939 0 +2940 0 +-2941 0 +2942 0 +2943 0 +-2944 0 +2945 0 +2946 0 +2947 0 +2948 0 +-2949 0 +2950 0 +2951 0 +2952 0 +-2953 0 +2954 0 +-2955 0 +-2956 0 +2957 0 +-2958 0 +-2959 0 +-2960 0 +-2961 0 +2962 0 +-2963 0 +-2964 0 +2965 0 +2966 0 +-2967 0 +-2968 0 +-2969 0 +-2970 0 +2971 0 +-2972 0 +2973 0 +2974 0 +-2975 0 +-2976 0 +-2977 0 +2978 0 +2979 0 +-2980 0 +2981 0 +2982 0 +2983 0 +2984 0 +-2985 0 +2986 0 +-2987 0 +2988 0 +-2989 0 +-2990 0 +2991 0 +-2992 0 +2993 0 +2994 0 +-2995 0 +2996 0 +2997 0 +-2998 0 +2999 0 +3000 0 +-3001 0 +-3002 0 +-3003 0 +-3004 0 +3005 0 +-3006 0 +-3007 0 +3008 0 +-3009 0 +-3010 0 +3011 0 +3012 0 +3013 0 +3014 0 +-3015 0 +3016 0 +-3017 0 +-3018 0 +3019 0 +-3020 0 +-3021 0 +-3022 0 +-3023 0 +-3024 0 +-3025 0 +3026 0 +3027 0 +3028 0 +3029 0 +-3030 0 +-3031 0 +-3032 0 +-3033 0 +-3034 0 +-3035 0 +-3036 0 +3037 0 +-3038 0 +3039 0 +3040 0 +-3041 0 +3042 0 +-3043 0 +3044 0 +-3045 0 +-3046 0 +3047 0 +-3048 0 +3049 0 +-3050 0 +3051 0 +3052 0 +-3053 0 +3054 0 +3055 0 +-3056 0 +-3057 0 +-3058 0 +3059 0 +-3060 0 +-3061 0 +-3062 0 +-3063 0 +3064 0 +-3065 0 +-3066 0 +3067 0 +3068 0 +-3069 0 +-3070 0 +-3071 0 +3072 0 +3073 0 +-3074 0 +3075 0 +3076 0 +3077 0 +3078 0 +3079 0 +3080 0 +-3081 0 +-3082 0 +-3083 0 +3084 0 +-3085 0 +-3086 0 +3087 0 +3088 0 +3089 0 +3090 0 +3091 0 +3092 0 +-3093 0 +-3094 0 +3095 0 +3096 0 +3097 0 +-3098 0 +-3099 0 +3100 0 +3101 0 +3102 0 +-3103 0 +3104 0 +3105 0 +-3106 0 +-3107 0 +3108 0 +3109 0 +-3110 0 +-3111 0 +3112 0 +-3113 0 +-3114 0 +-3115 0 +3116 0 +-3117 0 +-3118 0 +-3119 0 +-3120 0 +3121 0 +3122 0 +3123 0 +3124 0 +3125 0 +-3126 0 +3127 0 +-3128 0 +3129 0 +3130 0 +-3131 0 +-3132 0 +-3133 0 +-3134 0 +-3135 0 +-3136 0 +-3137 0 +-3138 0 +3139 0 +3140 0 +-3141 0 +3142 0 +-3143 0 +3144 0 +-3145 0 +3146 0 +-3147 0 +-3148 0 +3149 0 +-3150 0 +-3151 0 +-3152 0 +3153 0 +3154 0 +-3155 0 +-3156 0 +-3157 0 +3158 0 +-3159 0 +3160 0 +-3161 0 +-3162 0 +3163 0 +-3164 0 +3165 0 +3166 0 +-3167 0 +3168 0 +-3169 0 +3170 0 +3171 0 +-3172 0 +3173 0 +3174 0 +3175 0 +3176 0 +-3177 0 +3178 0 +3179 0 +3180 0 +3181 0 +-3182 0 +-3183 0 +-3184 0 +3185 0 +-3186 0 +-3187 0 +3188 0 +3189 0 +3190 0 +-3191 0 +3192 0 +3193 0 +-3194 0 +3195 0 +-3196 0 +3197 0 +-3198 0 +-3199 0 +3200 0 +3201 0 +3202 0 +-3203 0 +-3204 0 +-3205 0 +3206 0 +3207 0 +3208 0 +3209 0 +3210 0 +-3211 0 +-3212 0 +3213 0 +-3214 0 +3215 0 +-3216 0 +-3217 0 +3218 0 +-3219 0 +3220 0 +-3221 0 +-3222 0 +-3223 0 +-3224 0 +-3225 0 +-3226 0 +-3227 0 +-3228 0 +-3229 0 +-3230 0 +3231 0 +3232 0 +3233 0 +3234 0 +-3235 0 +-3236 0 +3237 0 +3238 0 +3239 0 +-3240 0 +-3241 0 +3242 0 +-3243 0 +3244 0 +-3245 0 +3246 0 +-3247 0 +-3248 0 +3249 0 +-3250 0 +-3251 0 +3252 0 +-3253 0 +-3254 0 +3255 0 +3256 0 +-3257 0 +-3258 0 +3259 0 +-3260 0 +-3261 0 +-3262 0 +-3263 0 +-3264 0 +-3265 0 +-3266 0 +-3267 0 +3268 0 +3269 0 +3270 0 +3271 0 +-3272 0 +-3273 0 +3274 0 +3275 0 +-3276 0 +3277 0 +3278 0 +3279 0 +-3280 0 +3281 0 +3282 0 +3283 0 +-3284 0 +3285 0 +3286 0 +3287 0 +-3288 0 +3289 0 +-3290 0 +-3291 0 +3292 0 +-3293 0 +-3294 0 +3295 0 +-3296 0 +-3297 0 +3298 0 +3299 0 +-3300 0 +-3301 0 +-3302 0 +-3303 0 +3304 0 +-3305 0 +3306 0 +3307 0 +3308 0 +3309 0 +-3310 0 +3311 0 +-3312 0 +3313 0 +-3314 0 +-3315 0 +3316 0 +3317 0 +3318 0 +3319 0 +-3320 0 +3321 0 +3322 0 +-3323 0 +-3324 0 +-3325 0 +3326 0 +-3327 0 +-3328 0 +3329 0 +-3330 0 +-3331 0 +-3332 0 +3333 0 +3334 0 +-3335 0 +-3336 0 +-3337 0 +3338 0 +-3339 0 +3340 0 +-3341 0 +-3342 0 +3343 0 +3344 0 +3345 0 +3346 0 +-3347 0 +3348 0 +3349 0 +3350 0 +-3351 0 +3352 0 +-3353 0 +-3354 0 +-3355 0 +-3356 0 +3357 0 +-3358 0 +3359 0 +-3360 0 +-3361 0 +-3362 0 +3363 0 +-3364 0 +3365 0 +3366 0 +-3367 0 +-3368 0 +3369 0 +3370 0 +3371 0 +3372 0 +3373 0 +-3374 0 +-3375 0 +-3376 0 +3377 0 +-3378 0 +-3379 0 +-3380 0 +3381 0 +-3382 0 +-3383 0 +-3384 0 +-3385 0 +-3386 0 +-3387 0 +3388 0 +3389 0 +3390 0 +-3391 0 +3392 0 +3393 0 +3394 0 +3395 0 +3396 0 +-3397 0 +-3398 0 +3399 0 +3400 0 +3401 0 +-3402 0 +-3403 0 +-3404 0 +-3405 0 +-3406 0 +-3407 0 +3408 0 +-3409 0 +-3410 0 +3411 0 +-3412 0 +-3413 0 +3414 0 +-3415 0 +-3416 0 +-3417 0 +-3418 0 +-3419 0 +3420 0 +3421 0 +-3422 0 +-3423 0 +3424 0 +3425 0 +-3426 0 +-3427 0 +3428 0 +-3429 0 +3430 0 +3431 0 +3432 0 +3433 0 +3434 0 +3435 0 +3436 0 +-3437 0 +3438 0 +-3439 0 +-3440 0 +-3441 0 +3442 0 +-3443 0 +-3444 0 +3445 0 +-3446 0 +3447 0 +3448 0 +-3449 0 +3450 0 +-3451 0 +-3452 0 +3453 0 +-3454 0 +3455 0 +-3456 0 +-3457 0 +3458 0 +3459 0 +-3460 0 +-3461 0 +-3462 0 +3463 0 +3464 0 +-3465 0 +-3466 0 +-3467 0 +-3468 0 +-3469 0 +-3470 0 +-3471 0 +-3472 0 +3473 0 +3474 0 +-3475 0 +-3476 0 +3477 0 +3478 0 +3479 0 +-3480 0 +-3481 0 +3482 0 +-3483 0 +3484 0 +-3485 0 +3486 0 +3487 0 +-3488 0 +-3489 0 +3490 0 +3491 0 +-3492 0 +3493 0 +-3494 0 +3495 0 +3496 0 +3497 0 +3498 0 +3499 0 +3500 0 +3501 0 +-3502 0 +3503 0 +-3504 0 +3505 0 +3506 0 +3507 0 +-3508 0 +3509 0 +-3510 0 +-3511 0 +3512 0 +-3513 0 +-3514 0 +3515 0 +-3516 0 +3517 0 +-3518 0 +-3519 0 +3520 0 +3521 0 +3522 0 +3523 0 +3524 0 +-3525 0 +-3526 0 +-3527 0 +3528 0 +3529 0 +-3530 0 +-3531 0 +-3532 0 +-3533 0 +3534 0 +3535 0 +3536 0 +-3537 0 +-3538 0 +3539 0 +3540 0 +-3541 0 +-3542 0 +3543 0 +-3544 0 +-3545 0 +-3546 0 +-3547 0 +-3548 0 +-3549 0 +3550 0 +3551 0 +-3552 0 +-3553 0 +3554 0 +3555 0 +-3556 0 +3557 0 +3558 0 +3559 0 +3560 0 +3561 0 +3562 0 +3563 0 +3564 0 +-3565 0 +-3566 0 +-3567 0 +3568 0 +-3569 0 +-3570 0 +-3571 0 +3572 0 +-3573 0 +3574 0 +3575 0 +-3576 0 +3577 0 +-3578 0 +-3579 0 +-3580 0 +3581 0 +-3582 0 +-3583 0 +3584 0 +3585 0 +-3586 0 +-3587 0 +3588 0 +-3589 0 +3590 0 +-3591 0 +3592 0 +3593 0 +3594 0 +3595 0 +3596 0 +-3597 0 +3598 0 +-3599 0 +-3600 0 +3601 0 +3602 0 +3603 0 +3604 0 +3605 0 +-3606 0 +-3607 0 +3608 0 +3609 0 +3610 0 +-3611 0 +-3612 0 +-3613 0 +-3614 0 +3615 0 +3616 0 +3617 0 +3618 0 +3619 0 +3620 0 +-3621 0 +3622 0 +-3623 0 +3624 0 +-3625 0 +-3626 0 +3627 0 +-3628 0 +3629 0 +3630 0 +3631 0 +-3632 0 +-3633 0 +-3634 0 +3635 0 +3636 0 +3637 0 +3638 0 +-3639 0 +-3640 0 +-3641 0 +-3642 0 +-3643 0 +-3644 0 +3645 0 +3646 0 +3647 0 +-3648 0 +-3649 0 +-3650 0 +3651 0 +3652 0 +3653 0 +3654 0 +-3655 0 +-3656 0 +3657 0 +3658 0 +-3659 0 +-3660 0 +3661 0 +3662 0 +-3663 0 +3664 0 +-3665 0 +3666 0 +3667 0 +3668 0 +-3669 0 +3670 0 +3671 0 +-3672 0 +-3673 0 +-3674 0 +-3675 0 +3676 0 +3677 0 +-3678 0 +3679 0 +-3680 0 +-3681 0 +-3682 0 +3683 0 +-3684 0 +3685 0 +3686 0 +-3687 0 +3688 0 +3689 0 +-3690 0 +3691 0 +-3692 0 +-3693 0 +-3694 0 +3695 0 +-3696 0 +3697 0 +-3698 0 +3699 0 +-3700 0 +-3701 0 +-3702 0 +-3703 0 +-3704 0 +-3705 0 +3706 0 +3707 0 +-3708 0 +3709 0 +-3710 0 +-3711 0 +3712 0 +-3713 0 +3714 0 +3715 0 +3716 0 +-3717 0 +3718 0 +-3719 0 +3720 0 +-3721 0 +-3722 0 +3723 0 +-3724 0 +-3725 0 +3726 0 +-3727 0 +3728 0 +3729 0 +3730 0 +3731 0 +3732 0 +3733 0 +-3734 0 +3735 0 +-3736 0 +3737 0 +-3738 0 +-3739 0 +-3740 0 +-3741 0 +-3742 0 +3743 0 +-3744 0 +3745 0 +3746 0 +-3747 0 +3748 0 +-3749 0 +-3750 0 +3751 0 +-3752 0 +-3753 0 +-3754 0 +-3755 0 +-3756 0 +3757 0 +-3758 0 +-3759 0 +3760 0 +3761 0 +3762 0 +-3763 0 +3764 0 +3765 0 +-3766 0 +3767 0 +-3768 0 +-3769 0 +3770 0 +-3771 0 +3772 0 +3773 0 +-3774 0 +3775 0 +-3776 0 +3777 0 +3778 0 +3779 0 +3780 0 +-3781 0 +-3782 0 +-3783 0 +-3784 0 +3785 0 +-3786 0 +3787 0 +-3788 0 +3789 0 +3790 0 +3791 0 +-3792 0 +-3793 0 +-3794 0 +3795 0 +-3796 0 +-3797 0 +-3798 0 +-3799 0 +-3800 0 +3801 0 +3802 0 +3803 0 +-3804 0 +3805 0 +3806 0 +-3807 0 +-3808 0 +-3809 0 +-3810 0 +3811 0 +-3812 0 +-3813 0 +3814 0 +3815 0 +3816 0 +-3817 0 +-3818 0 +-3819 0 +3820 0 +3821 0 +3822 0 +3823 0 +3824 0 +3825 0 +3826 0 +3827 0 +3828 0 +3829 0 +-3830 0 +-3831 0 +3832 0 +3833 0 +3834 0 +3835 0 +-3836 0 +-3837 0 +-3838 0 +-3839 0 +3840 0 +-3841 0 +3842 0 +-3843 0 +-3844 0 +3845 0 +3846 0 +-3847 0 +3848 0 +3849 0 +-3850 0 +-3851 0 +3852 0 +-3853 0 +3854 0 +-3855 0 +-3856 0 +-3857 0 +3858 0 +3859 0 +3860 0 +-3861 0 +-3862 0 +-3863 0 +3864 0 +-3865 0 +-3866 0 +-3867 0 +-3868 0 +-3869 0 +-3870 0 +-3871 0 +-3872 0 +3873 0 +-3874 0 +3875 0 +-3876 0 +3877 0 +3878 0 +-3879 0 +-3880 0 +-3881 0 +-3882 0 +3883 0 +-3884 0 +3885 0 +-3886 0 +-3887 0 +3888 0 +3889 0 +3890 0 +-3891 0 +3892 0 +3893 0 +-3894 0 +-3895 0 +-3896 0 +-3897 0 +3898 0 +-3899 0 +3900 0 +3901 0 +3902 0 +3903 0 +3904 0 +3905 0 +-3906 0 +3907 0 +3908 0 +-3909 0 +3910 0 +3911 0 +-3912 0 +3913 0 +3914 0 +-3915 0 +-3916 0 +3917 0 +-3918 0 +3919 0 +-3920 0 +3921 0 +3922 0 +-3923 0 +3924 0 +3925 0 +-3926 0 +3927 0 +-3928 0 +3929 0 +3930 0 +3931 0 +3932 0 +-3933 0 +-3934 0 +-3935 0 +-3936 0 +3937 0 +3938 0 +3939 0 +3940 0 +3941 0 +-3942 0 +3943 0 +-3944 0 +3945 0 +3946 0 +3947 0 +-3948 0 +3949 0 +-3950 0 +3951 0 +-3952 0 +-3953 0 +3954 0 +3955 0 +3956 0 +3957 0 +-3958 0 +3959 0 +3960 0 +-3961 0 +-3962 0 +-3963 0 +-3964 0 +3965 0 +-3966 0 +-3967 0 +-3968 0 +3969 0 +3970 0 +3971 0 +-3972 0 +-3973 0 +-3974 0 +3975 0 +3976 0 +3977 0 +-3978 0 +-3979 0 +-3980 0 +-3981 0 +3982 0 +-3983 0 +-3984 0 +-3985 0 +-3986 0 +-3987 0 +3988 0 +-3989 0 +3990 0 +-3991 0 +-3992 0 +-3993 0 +-3994 0 +3995 0 +3996 0 +-3997 0 +3998 0 +3999 0 +-4000 0 +4001 0 +-4002 0 +-4003 0 +4004 0 +-4005 0 +4006 0 +-4007 0 +4008 0 +4009 0 +-4010 0 +4011 0 +-4012 0 +4013 0 +4014 0 +-4015 0 +4016 0 +4017 0 +-4018 0 +4019 0 +-4020 0 +-4021 0 +4022 0 +-4023 0 +-4024 0 +-4025 0 +4026 0 +4027 0 +-4028 0 +4029 0 +-4030 0 +-4031 0 +-4032 0 +-4033 0 +4034 0 +4035 0 +-4036 0 +-4037 0 +4038 0 +4039 0 +-4040 0 +-4041 0 +-4042 0 +-4043 0 +4044 0 +4045 0 +-4046 0 +4047 0 +4048 0 +4049 0 +-4050 0 +4051 0 +4052 0 +4053 0 +4054 0 +4055 0 +4056 0 +4057 0 +-4058 0 +-4059 0 +-4060 0 +-4061 0 +-4062 0 +-4063 0 +-4064 0 +4065 0 +4066 0 +-4067 0 +-4068 0 +-4069 0 +4070 0 +-4071 0 +-4072 0 +4073 0 +-4074 0 +-4075 0 +-4076 0 +-4077 0 +4078 0 +4079 0 +4080 0 +4081 0 +-4082 0 +-4083 0 +-4084 0 +-4085 0 +4086 0 +-4087 0 +4088 0 +4089 0 +-4090 0 +4091 0 +4092 0 +-4093 0 +4094 0 +4095 0 +-4096 0 \ No newline at end of file diff --git a/csflocref.c b/csflocref.c new file mode 100644 index 0000000..c3c6a1e --- /dev/null +++ b/csflocref.c @@ -0,0 +1,630 @@ +#include "csflocref.h" +/* +============================================================================ + Name : csfloc.c + Author : Gábor Kusper + Version : 1.0 + Copyright : Gábor Kusper + Description : CSFLOC in C, Ansi-style + ============================================================================ + */ + + +#include +#include +#include + + +char* fileName; +int doSorting = 1; +int doIndexing = 1; // can be true only if doSorting is also true +int addLongTailClauses = 0; // can be greater than 0 only if doIndexing is true +int howManyClausesAddMaximumPerClauses = 0; + +unsigned int MAXINTINDEX; +unsigned int MAXBITINDEX; +unsigned int MAXVALUE; + +unsigned int* counter; +unsigned int* clauses; + +int* numxsAtEnd; +int* indexClausesByNumxsAtEnd; + +int numOfClauses; +int numOfVariables; + +int lentghOfBitArray; + + +void printBitArray(unsigned int* toPrint) +{ + int i; + for(i = numOfVariables-1; i>=0; i--) + { + int intIndex = i / (sizeof(int)*8); + int bitIndex = i % (sizeof(int)*8); + int mask = 1 << bitIndex; + if((toPrint[intIndex] & mask) > 0) printf("%d ", numOfVariables-i); + else printf("-%d ", numOfVariables-i); + } + printf("0 \n"); +} + +void printClause(int clauseIndex) +{ + printf("clauseIndex:%d\n",clauseIndex); + printf("numxsAtEnd[clauseIndex]:%d\n",numxsAtEnd[clauseIndex]); + int index = clauseIndex * lentghOfBitArray * 2; + int i; + for(i = numOfVariables-1; i>=0; i--) + { + int intIndex = i / (sizeof(int)*8); + int bitIndex = i % (sizeof(int)*8); + int mask = 1 << bitIndex; + if((clauses[index + intIndex*2] & mask) > 0) printf("%d ", numOfVariables-i); + else printf("-%d ", numOfVariables-i); + } + printf("0 \n"); + for(i = numOfVariables-1; i>=0; i--) + { + int intIndex = i / (sizeof(int)*8); + int bitIndex = i % (sizeof(int)*8); + int mask = 1 << bitIndex; + if((clauses[index + intIndex*2 + 1] & mask) > 0) printf("%d ", numOfVariables-i); + else printf("-%d ", numOfVariables-i); + } + printf("0 \n"); +} + + +void printClauses() +{ + int clauseIndex; + for(clauseIndex=0; clauseIndex < numOfClauses; clauseIndex++) + { + printClause(clauseIndex); + } +} + +// coin: http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightBinSearch +int countZeroBitsOnTheRight(unsigned int v) +{ + int c; + // NOTE: if 0 == v, then c = 31. + if (v & 0x1) + { + // special case for odd v (assumed to happen half of the time) + c = 0; + } + else + { + c = 1; + if ((v & 0xffff) == 0) + { + v >>= 16; + c += 16; + } + if ((v & 0xff) == 0) + { + v >>= 8; + c += 8; + } + if ((v & 0xf) == 0) + { + v >>= 4; + c += 4; + } + if ((v & 0x3) == 0) + { + v >>= 2; + c += 2; + } + c -= v & 0x1; + } + return c; +} + + +int countZeroBitsOnTheRightInBitArray(int clauseIndex) +{ + int countZeroBits = 0; + int index = clauseIndex * lentghOfBitArray * 2; + int intIndex; + for(intIndex=0; intIndex 0) clauses[index + intIndex * 2 +1] |= setMask; + if (abs(literal) > maxLiteral) maxLiteral = abs(literal); + } + numxsAtEnd[clauseIndex] = numOfVariables - maxLiteral; + clauseIndex++; + if (clauseIndex == numOfClauses) break; + } + fclose(fptr); + + /* + for (uint i = 0; i < numOfClauses; ++i) { + printf("%u ", numxsAtEnd[i]); + } + printf("\n"); + printf("numxsAtEnd\n"); + */ +} + +void sortClausesByNumxsAtEnd() +{ + //printf("Before sorting:\n"); + //printClauses(); + int i; + for(i=1; i=0; i--) + { + if (numxsAtEnd[i] > lastValue) + { + while(lastValue != numxsAtEnd[i]) + { + indexClausesByNumxsAtEnd[lastValue] = i+1; + lastValue++; + } + } + } + + // it might be, that we over index if there is no clause with numxAtEnd == 0 + // this part corrects this if needed + int correctioningIndex = 0; + while (indexClausesByNumxsAtEnd[correctioningIndex] == numOfClauses) + { + correctioningIndex++; + } + if (correctioningIndex!=0) + { + int goodValue = indexClausesByNumxsAtEnd[correctioningIndex]; + do + { + correctioningIndex--; + indexClausesByNumxsAtEnd[correctioningIndex] = goodValue; + } + while(correctioningIndex!=0); + } +} + + +void addClausesByResolution() +{ + int numberOfNewClauses = 0; + int numOfZerosAtEnd = 0; + while (numberOfNewClauses=indexClausesByNumxsAtEnd[numOfZerosAtEnd]; clauseIndexA--) + { + int clauseIndexB; + int newClausesPerClause = 0; + for(clauseIndexB=clauseIndexA-1; clauseIndexB>=indexClausesByNumxsAtEnd[numOfZerosAtEnd]; clauseIndexB--) + { + resolution(numOfClauses+numberOfNewClauses, clauseIndexA, clauseIndexB, + numOfZerosAtEnd/(sizeof(unsigned int)*8), + numOfZerosAtEnd%(sizeof(unsigned int)*8)); + if (numxsAtEnd[numOfClauses+numberOfNewClauses] == -1) continue; + + //printf("numOfZerosAtEnd: %d\n", numOfZerosAtEnd); + //printf("numberOfNewClauses: %d\n", numberOfNewClauses); + //printf("numxsAtEnd[numOfClauses+numberOfNewClauses]: %d\n", numxsAtEnd[numOfClauses+numberOfNewClauses]); + + numberOfNewClauses++; + newClausesPerClause++; + + if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break; + if (numberOfNewClauses==addLongTailClauses) break; + } + if (numberOfNewClauses==addLongTailClauses) break; + + + // +1 m?lys?g eleje + int numOfZerosAtEnd2 = numxsAtEnd[numOfClauses+numberOfNewClauses-1]; + int clauseIndexC = numOfClauses+numberOfNewClauses-1; + int clauseIndexD; + for(clauseIndexD=indexClausesByNumxsAtEnd[numOfZerosAtEnd2-1]-1; + clauseIndexD>=indexClausesByNumxsAtEnd[numOfZerosAtEnd2]; clauseIndexD--) + { + + //printf("before resolution in +1 depth\n"); + //printf("numxsAtEnd[clauseIndexC]: %d\n", numxsAtEnd[clauseIndexC]); + //printf("numxsAtEnd[clauseIndexD]: %d\n", numxsAtEnd[clauseIndexD]); + + + resolution(numOfClauses+numberOfNewClauses, clauseIndexC, clauseIndexD, + numOfZerosAtEnd2/(sizeof(unsigned int)*8), + numOfZerosAtEnd2%(sizeof(unsigned int)*8)); + if (numxsAtEnd[numOfClauses+numberOfNewClauses] == -1) continue; + + //printf("after resolution in +1 depth\n"); + //printf("numOfZerosAtEnd2: %d\n", numOfZerosAtEnd2); + //printf("numberOfNewClauses: %d\n", numberOfNewClauses); + //printf("numxsAtEnd[numOfClauses+numberOfNewClauses]: %d\n", numxsAtEnd[numOfClauses+numberOfNewClauses]); + + numberOfNewClauses++; + newClausesPerClause++; + + if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break; + if (numberOfNewClauses==addLongTailClauses) break; + } + if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break; + if (numberOfNewClauses==addLongTailClauses) break; + if (numberOfNewClauses==addLongTailClauses) break; + //+1 m?lys?g v?ge + + + + } + numOfZerosAtEnd++; + if (numOfZerosAtEnd == numOfVariables) break; + } + + int i; + for(i=numOfClauses; i=0; clauseIndex--) + { + if (numxsAtEnd[clauseIndex]maxNumx) maxNumx = numxsAtEnd[clauseIndex]; + // printf("s %u %u\n", clauseIndex, numxsAtEnd[clauseIndex]); + if (doSorting) { + break; + } + } + clauseIndex++; + } + if(maxNumx >= 0) + { + fprintf(iofile, "j: %d\n",maxNumx); + int intIndex = maxNumx / (sizeof(int)*8); + int bitIndex = maxNumx % (sizeof(int)*8); + + unsigned int oldCounter = counter[intIndex]; + //printf("Counter old = %d : %d\n", intIndex, oldCounter); + + counter[intIndex] += 1 << bitIndex; + //printf("Counter new = %d : %u\n\n", intIndex, counter.array[intIndex]); + + // add carry + while(oldCounter > counter[intIndex]) { + //printf("add carry\n"); + //printf("num of clauses:%d\n",numOfClauses); + //printf("i = %d\n", i); + //printf("Counter old = %d : %u\n", intIndex, oldCounter); + //printf("bitIndex = %d ; 1 << bitIndex = %d\n", bitIndex, 1 << bitIndex); + //printf("Counter new = %d : %u\n", intIndex, counter.array[intIndex]); + intIndex++; + oldCounter = counter[intIndex]; + //printf("Counter old = %d : %u\n", intIndex, oldCounter); + counter[intIndex]++; // carry added here + //printf("Counter new = %d : %u\n\n", intIndex, counter[intIndex]); + } + + if (counter[lentghOfBitArray-1] >= MAXVALUE) return; + changed = 1; + } + + } + + int i; + for (i=0; i\n"); + printf("\t\t is a file name, it is the SAT problem to be solved, " + "it should be in DIMACS format.\n"); + printf("\t\tOUTPUT is written to standard output.\n"); + printf("OPTIONS:\n"); + printf("\t-help\tDisplays this help message.\n"); + printf("\t-dosort\tTurns on clause sorting.\n"); + printf("\t-donotsort\tTurns off clause sorting.\n"); + printf("\t-doindexing\tTurns on clause indexing, and also forces clause sorting to be switched on.\n"); + printf("\t-donotindexing\tTurns off clause indexing.\n"); + printf("\t-addLongTailClauses=N\tAllows to add long tail clauses, "); + printf("max N clauses are allowed, if N is 0 then it switches off long tail clause adding. "); + printf("If N is greater than 0 then it forces clause ordering and indexing.\n"); + printf("\t-addLongTailClausesPerClause=M\tAllows to add maximum M long tail clauses per each input clause, "); + printf("if M is 0 then it switches off long tail clause adding, i.e., it sets N to be 0. "); + printf("It has any effect if and only if long tail clause adding is switched on, "); + printf("i.e., N and M are not 0.\n"); + printf("THE DEFAULT SETTINGS ARE:\n"); + printf("Clause indexing is turned on, clause sorting is turned on, "); + printf("1000 long tail clauses are allowed, 100 per input clauses, i.e., N = 1000, and M = 100.\n"); + printf("EXAMPLE 1:\n"); + printf("\tcsfloc -input=hole6.cnf\n"); + printf("\tReads and solves the SAT problem represented by hole6.cnf. The solution is written to the standard output.\n"); + printf("EXAMPLE 2:\n"); + printf("\tcsfloc -input=uf50-01.cnf -dosort -doindex -addLongTailClauses=1000 -addLongTailClausesPerClause=100\n"); + printf("\tReads and solves the SAT problem represented by uf50-01.cnf. "); + printf("Clause sorting is switched on. "); + printf("Clause indexing is switched on. "); + printf("Adding long tail clauses is switch on. Maximum 1000 new clauses are created, maximum 100 per input clauses. "); + printf("The solution is written to the standard output.\n"); +} + +// read the "value" of a command line argument, where the format of the arguments is = +char* getCommandLineArgValue(char* arg) { + char* s = strchr(arg, '='); + + if (!s) return NULL; + + // close the "name" of the argument, as a string + *s = '\0'; + + // return the "value" of the argument + return s + 1; +} + +// process all the command line argument +int processCommandLineArgs(int argc, char** argv) { + int i=0; + int numberOfSetMandatoryOptions=1; + return numberOfSetMandatoryOptions == 1; +} + +void runcsfloc(char* path, FILE* iofile) { + + long startTime = clock(); + //printf("phase 0\n"); + readDIMACScsfloc(path); + //printf("phase 1\n"); + // printClauses(); + if (doSorting) { + sortClausesByNumxsAtEnd(); + } + //printf("phase 2\n"); + // printClauses(); + if (doIndexing) createIndexClausesByNumxsAtEnd(); + //printf("phase 3\n"); + if (addLongTailClauses>0) { + addClausesByResolution(); + printf("Please don't do this\n"); + } + + + CCCSolver(iofile); + + long endTime = clock(); + + /* + if (counter[lentghOfBitArray-1] >= MAXVALUE) printf("0\n"); + else + { + printf("1\n"); + } + */ + + + + free(numxsAtEnd); + free(counter); + free(clauses); + free(indexClausesByNumxsAtEnd); + + +} diff --git a/csflocref.h b/csflocref.h new file mode 100644 index 0000000..dc59192 --- /dev/null +++ b/csflocref.h @@ -0,0 +1,5 @@ +#pragma once +#include "types.h" +#include + +void runcsfloc(char* path, FILE* iofile); \ No newline at end of file diff --git a/githubtoken b/githubtoken new file mode 100644 index 0000000..7e58af9 --- /dev/null +++ b/githubtoken @@ -0,0 +1 @@ +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 \ No newline at end of file diff --git a/gpusolver.c b/gpusolver.c index 831f89b..57ea871 100644 --- a/gpusolver.c +++ b/gpusolver.c @@ -58,8 +58,8 @@ gpusolver* initSolver() { // TODO: Cleanup return NULL; } - - o->commqueue = clCreateCommandQueueWithProperties(o->ctx, o->deviceid, 0, &res); + cl_queue_properties properties[] = { CL_QUEUE_PROPERTIES, CL_QUEUE_PROFILING_ENABLE, 0 }; + o->commqueue = clCreateCommandQueueWithProperties(o->ctx, o->deviceid, properties, &res); if (res != CL_SUCCESS) { printf("Failed to create OpenCL command queue\n"); // TODO: Cleanup diff --git a/main.c b/main.c index a97c575..cf6b1c5 100644 --- a/main.c +++ b/main.c @@ -85,7 +85,7 @@ int main() { // runuf20lol(); - runTests(); + // runTests(); /* srand( utime()); @@ -116,8 +116,8 @@ int main() { - /* - cnf* c = readDIMACS("/home/lev/Downloads/uf20/uf20-03.cnf"); + + cnf* c = readDIMACS("/home/heka/Downloads/uf20/uf20-03.cnf"); sortlastnum(c); // gpusolve(c); @@ -133,7 +133,7 @@ int main() { freecnf(c); return 0; - */ + // runTests(); // return 0; diff --git a/psatv0.cl b/psatv0.cl new file mode 100644 index 0000000..9a29997 --- /dev/null +++ b/psatv0.cl @@ -0,0 +1,278 @@ + +#pragma OPENCL EXTENSION cl_khr_byte_addressable_store : enable + +#define DEBUG + +#ifdef DEBUG +#define DBG(X) printf("%s\n", (X)) +#else +#define DBG(X) do {} while (0) +#endif + +static inline void printbits(uint a) { + for (uint i = 0; i < 32; ++i) { + uint ind = 31 - i; + printf("%u", (a >> ind) & 1U); + } +} + +static inline void stateaddpow(uint wcnt, uint* state, uint pow) { + uint corpow = pow & 0b11111U; + uint startind = pow >> 5U; + uint tr = 1U << corpow; + uint tval = state[startind] + tr; + bool carry = tval < state[startind]; + state[startind] = tval; + if (carry) { + uint i = startind + 1; + for ( ; i < wcnt; ++i) { + state[i]++; + if (state[i]) break; + } + } +} + +/* +static inline void stateaddpow(uint wcnt, uint* state, uint pow) { + uint corpow = pow & 0b11111U; + uint startind = pow >> 5U; + uint tr = 1U << corpow; + uint tval = state[startind] + tr; + bool carry = tval < state[startind]; + uint i = startind + 1; + for ( ; i < wcnt; ++i) { + state[i] = carry + state[i]; + carry = (state[i] == 0) * carry; + } + + //if (carry) { + //uint i = startind + 1; + //for ( ; i < wcnt; ++i) { + //state[i]++; + //if (state[i]) break; + //} + //} + +} +*/ + + + +__kernel void vectorSAT(__global const uint* cnfheader, __global const uint* lvars, __global const uint* vars, __global const uint* clauses, __global const uchar* pars, __global uint* output, __global uchar* scratchpad, __local uint* maxvals) { + output[0] = 2; + + __local uint setmax; + + uint cnt = cnfheader[0]; + uint vcnt = cnfheader[1]; + uint ccnt = cnfheader[2]; + + uint wcnt = 1 + (vcnt >> 5U); + + uint maxctr = 1U << (vcnt & 0b11111U); + + uint glbid = get_global_id(0); + uint glbsz = get_global_size(0); + + /* + uint locid = get_local_id(0); + uint locsz = get_local_size(0); + uint grpid = get_group_id(0); + uint grpcn = get_num_groups(0); + */ + + // Zero out the counter + for (uint i = 0; i < wcnt; ++i) output[i + 1] = 0; + + // Set all scratchpad clauses to true + for (uint j = 0; j < ccnt; j += glbsz) { + uchar cond = (j + glbid) < ccnt; + // If ptr would go past end of array, set it to last element + j = j * cond + (!cond) * (ccnt - glbid - 1); + scratchpad[j + glbid] = 1; + // if ((j + glbid) < ccnt) + } + + bool done = false; + __local uint iter; + __local uint firstind[1]; + iter = 0; + while (output[0] == 2) { + firstind[0] = ccnt; + if (glbid == 0) { + iter = iter + 1; + } + // if (glbid == 0) printf("%s\n", ":~"); + setmax = 0; + uint maxnumx = 0; + + for (uint j = 0; j < cnt; j += glbsz) { + + uchar cond = (j + glbid) < cnt; + // Last element cap + j = j * cond + (!cond) * (cnt - glbid - 1); + uint varind = vars[j + glbid]; + varind = (vcnt - 1) - varind; + uint iind = varind >> 5U; + uint bind = varind & 0b11111U; + uchar cpar = (output[iind + 1] >> bind) & 1U; + //uchar cond2 = (cpar != pars[j + glbid]); + //uint dirind = cond2 * clauses[j + glbid] + (!cond2) * ccnt; + // scratchpad[dirind] = 0; + + if (cpar != pars[j + glbid]) { + scratchpad[clauses[j + glbid]] = 0; + /* + if (clauses[j + glbid] == 50) { + printf("50 failed on (%u) %u (%u) %u / %u %u\n", pars[j + glbid], vars[j + glbid], cpar, varind, iind, bind); + printbits(output[2]); + printbits(output[1]); + } + */ + } + + /* + if ((j + glbid) < cnt) { + uint varind = vars[j + glbid]; + varind = (vcnt - 1) - varind; + uint iind = varind >> 5U; + uint bind = varind & 0b11111U; + uchar cpar = (output[iind + 1] >> bind) & 1U; + if (cpar != pars[j + glbid]) { + scratchpad[clauses[j + glbid]] = 0; + // printf("z %u %u\n", j + glbid, clauses[j + glbid]); + } + } + */ + + } + + barrier(CLK_LOCAL_MEM_FENCE | CLK_GLOBAL_MEM_FENCE); + + + for (uint j = 0; j < ccnt; j += glbsz) { + /* + if (((j + glbid) < ccnt) && (scratchpad[j + glbid] == 1)) { + setmax = 1; + // printf("%u\n", (~output[1]) & 0b11111); + // printf("%u%u%u%u%u\n", (output[1] >> 4) & 1U, (output[1] >> 3) & 1U, (output[1] >> 2) & 1U, (output[1] >> 1) & 1U, output[1] & 1U); + // printf("%u - %u\n", j + glbid, scratchpad[j + glbid]); + }*/ + + //uchar cond = (j + glbid) < ccnt; + // Last element cap + // j = j * cond + (!cond) * (ccnt - glbid - 1); + if (scratchpad[j + glbid] == 1 && (j + glbid) < ccnt) { + setmax = 1; + // printf("s %u %u %u\n", j + glbid, lvars[j + glbid], iter); + // printf("c %u %u %u\n", j + glbid, scratchpad[j + glbid], lvars[j + glbid]); + } + } + + barrier(CLK_LOCAL_MEM_FENCE); + /* + if (glbid == 0) { + printf(">> %u%u%u%u%u%u%u%u%u%u%u%u%u%u%u%u%u%u%u%u\n", (output[1] >> 19) & 1U,(output[1] >> 18) & 1U, (output[1] >> 17) & 1U, (output[1] >> 16) & 1U, (output[1] >> 15) & 1U, (output[1] >> 14) & 1U, (output[1] >> 13) & 1U, (output[1] >> 12) & 1U, (output[1] >> 11) & 1U, (output[1] >> 10) & 1U, (output[1] >> 9) & 1U, (output[1] >> 8) & 1U, (output[1] >> 7) & 1U, (output[1] >> 6) & 1U, (output[1] >> 5) & 1U, (output[1] >> 4) & 1U, (output[1] >> 3) & 1U, (output[1] >> 2) & 1U, (output[1] >> 1) & 1U, output[1] & 1U); + + } + */ + + + + + if (setmax) { + // Set maxval array to zero + maxvals[glbid] = 0; + + // Accumulate and reduce the maximums + for (uint j = 0; j < ccnt; j += glbsz) { + + uint a = maxvals[glbid]; + uint b = lvars[j + glbid]; + uint c = max(a, b); + + //uchar cond = (j + glbid) < ccnt; + //uint d = glbid * cond + (!cond) * glbsz; + //maxvals[d] = c; + if ((j + glbid) < ccnt && scratchpad[j + glbid] == 1) { + maxvals[glbid] = c; + // printf("min %u\n", j + glbid); + // atomic_min(firstind, (j + glbid)); + } + } + + /* + if (glbid == 0) { + for (uint k = 0; k < ccnt; ++k) { + if (scratchpad[k] == 1) { + printf("s %u %u\n", k, lvars[k]); //, iter); + } + } + + printf("z %u %u\n", scratchpad[50], scratchpad[199]); + } + */ + + barrier(CLK_LOCAL_MEM_FENCE); + + // uint maxj = lvars[firstind[0]]; + + // Set all scratchpad clauses to true + for (uint j = 0; j < ccnt; j += glbsz) { + uchar cond = (j + glbid) < ccnt; + // If ptr would go past end of array, set it to last element + j = j * cond + (!cond) * (ccnt - glbid - 1); + scratchpad[j + glbid] = 1; + // if ((j + glbid) < ccnt) + } + + // Final reduction pass + + uint maxj = maxvals[0]; + for (uint j = 1; j < glbsz; ++j) { + maxj = max(maxj, maxvals[j]); + } + + + // Add to the counter + if (glbid == 0) { + // printf("> %u\n", maxj); + /* + printbits(output[2]); + printbits(output[1]); + printf("%s", "\n"); + */ + // uint temp = ind; + // printf("maxNumx = %u\n", maxj);// firstind[0]); + stateaddpow(wcnt, output + 1, maxj); + /* + printbits(output[2]); + printbits(output[1]); + printf("%s", "\n"); + */ + /* + if (output[2] == 60234U) { + printf("%s\n", "YEEDLEY DEET"); + printbits(output[2]); + printbits(output[1]); + printf("%s", "\n"); + } + */ + + // printf(">> %u%u%u%u%u\n", (output[1] >> 4) & 1U, (output[1] >> 3) & 1U, (output[1] >> 2) & 1U, (output[1] >> 1) & 1U, output[1] & 1U); + } + + // Check counter for overflow + if (output[wcnt] >= maxctr) { + output[0] = 1; + } + } else { + // SAT. Set status and assignment. + output[0] = 0; + if (glbid == 0) { + for (uint i = 0; i < wcnt; ++i) output[i + 1] = ~output[i + 1]; + } + } + barrier(CLK_LOCAL_MEM_FENCE); + } +} \ No newline at end of file