meelgroup/ganak

The first scalable probabilistic exact counter

ganak's Issues

Incorrect count on a specific set of benchmarks

I found Ganak always returned the same count 2^50 or 2^60 or 2^70 on a large set of benchmarks. These benchmarks probably originate from the same question according to the filename. I used default values for all options of Ganak 1.0.0.

For example, check out the instance. ApproxMC can enumerate all 1024 solutions but Ganak gives a count of 2^50.

Check out the entire set of benchmarks here.

Actually, the issue may not be due to Ganak. I checked sharpSAT gives the same problematic count of 2^50. Therefore, it's probably an underlying bug in sharpSAT.

Output strange information and wrong count for the following instance

p cnf 2580 3300
3 -1 0
1 4 0
7 -5 0
41 1840 1601 0
11 -9 0
1604 1601 0
15 -13 0
2354 1601 0
19 -17 0
2278 1601 0
23 -21 0
2202 1601 0
27 -25 0
2126 1601 0
31 -29 0
2050 1601 0
35 -33 0
1974 1601 0
39 -37 0
1898 1601 0
43 -41 0
5 1822 1601 0
47 -45 0
1858 77 1601 0
51 -49 0
73 1856 1601 0
55 -53 0
1854 69 1601 0
59 -57 0
65 1852 1601 0
63 -61 0
61 1850 1601 0
67 -65 0
57 1848 1601 0
71 -69 0
53 1846 1601 0
75 -73 0
49 1844 1601 0
79 -77 0
45 1842 1601 0
83 -81 0
1608 1605 0
87 -85 0
85 88 0
91 -89 0
2242 1605 0
95 -93 0
2166 1605 0
99 -97 0
2090 1605 0
103 -101 0
2014 1605 0
107 -105 0
1938 1605 0
111 -109 0
1894 153 1605 0
115 -113 0
149 1892 1605 0
119 -117 0
1890 145 1605 0
123 -121 0
141 1888 1605 0
127 -125 0
137 1886 1605 0
131 -129 0
133 1884 1605 0
135 -133 0
129 1882 1605 0
139 -137 0
125 1880 1605 0
143 -141 0
121 1878 1605 0
147 -145 0
117 1876 1605 0
151 -149 0
113 1874 1605 0
155 -153 0
109 1872 1605 0
159 -157 0
2394 1605 0
163 -161 0
2282 1609 0
167 -165 0
2206 1609 0
171 -169 0
169 172 0
175 -173 0
2130 1609 0
179 -177 0
2054 1609 0
183 -181 0
1978 1609 0
187 -185 0
233 1932 1609 0
191 -189 0
1930 229 1609 0
195 -193 0
225 1928 1609 0
199 -197 0
1926 221 1609 0
203 -201 0
217 1924 1609 0
207 -205 0
213 1922 1609 0
211 -209 0
209 1920 1609 0
215 -213 0
205 1918 1609 0
219 -217 0
201 1916 1609 0
223 -221 0
197 1914 1609 0
227 -225 0
193 1912 1609 0
231 -229 0
189 1910 1609 0
235 -233 0
185 1908 1609 0
239 -237 0
1612 1609 0
243 -241 0
2246 1613 0
247 -245 0
2170 1613 0
251 -249 0
2094 1613 0
255 -253 0
253 256 0
259 -257 0
2018 1613 0
263 -261 0
1970 313 1613 0
267 -265 0
309 1968 1613 0
271 -269 0
1966 305 1613 0
275 -273 0
301 1964 1613 0
279 -277 0
1962 297 1613 0
283 -281 0
293 1960 1613 0
287 -285 0
289 1958 1613 0
291 -289 0
285 1956 1613 0
295 -293 0
281 1954 1613 0
299 -297 0
277 1952 1613 0
303 -301 0
273 1950 1613 0
307 -305 0
269 1948 1613 0
311 -309 0
265 1946 1613 0
315 -313 0
261 1944 1613 0
319 -317 0
1616 1613 0
323 -321 0
2210 1617 0
327 -325 0
2134 1617 0
331 -329 0
2058 1617 0
335 -333 0
393 2008 1617 0
339 -337 0
337 340 0
343 -341 0
2006 389 1617 0
347 -345 0
385 2004 1617 0
351 -349 0
2002 381 1617 0
355 -353 0
377 2000 1617 0
359 -357 0
1998 373 1617 0
363 -361 0
369 1996 1617 0
367 -365 0
365 1994 1617 0
371 -369 0
361 1992 1617 0
375 -373 0
357 1990 1617 0
379 -377 0
353 1988 1617 0
383 -381 0
349 1986 1617 0
387 -385 0
345 1984 1617 0
391 -389 0
341 1982 1617 0
395 -393 0
1980 333 1617 0
399 -397 0
1620 1617 0
403 -401 0
2174 1621 0
407 -405 0
2098 1621 0
411 -409 0
2046 473 1621 0
415 -413 0
469 2044 1621 0
419 -417 0
2042 465 1621 0
423 -421 0
421 424 0
427 -425 0
461 2040 1621 0
431 -429 0
2038 457 1621 0
435 -433 0
453 2036 1621 0
439 -437 0
2034 449 1621 0
443 -441 0
445 2032 1621 0
447 -445 0
441 2030 1621 0
451 -449 0
437 2028 1621 0
455 -453 0
433 2026 1621 0
459 -457 0
429 2024 1621 0
463 -461 0
425 2022 1621 0
467 -465 0
2020 417 1621 0
471 -469 0
2018 413 1621 0
475 -473 0
2016 409 1621 0
479 -477 0
1624 1621 0
483 -481 0
2138 1625 0
487 -485 0
553 2084 1625 0
491 -489 0
2082 549 1625 0
495 -493 0
545 2080 1625 0
499 -497 0
2078 541 1625 0
503 -501 0
537 2076 1625 0
507 -505 0
505 508 0
511 -509 0
2074 533 1625 0
515 -513 0
529 2072 1625 0
519 -517 0
2070 525 1625 0
523 -521 0
521 2068 1625 0
527 -525 0
517 2066 1625 0
531 -529 0
513 2064 1625 0
535 -533 0
509 2062 1625 0
539 -537 0
2060 501 1625 0
543 -541 0
2058 497 1625 0
547 -545 0
2056 493 1625 0
551 -549 0
2054 489 1625 0
555 -553 0
2052 485 1625 0
559 -557 0
1628 1625 0
563 -561 0
2122 633 1629 0
567 -565 0
629 2120 1629 0
571 -569 0
2118 625 1629 0
575 -573 0
621 2116 1629 0
579 -577 0
2114 617 1629 0
583 -581 0
613 2112 1629 0
587 -585 0
2110 609 1629 0
591 -589 0
589 592 0
595 -593 0
605 2108 1629 0
599 -597 0
2106 601 1629 0
603 -601 0
597 2104 1629 0
607 -605 0
593 2102 1629 0
611 -609 0
2100 585 1629 0
615 -613 0
2098 581 1629 0
619 -617 0
2096 577 1629 0
623 -621 0
2094 573 1629 0
627 -625 0
2092 569 1629 0
631 -629 0
2090 565 1629 0
635 -633 0
2088 561 1629 0
639 -637 0
1632 1629 0
643 -641 0
2158 709 1633 0
647 -645 0
705 2156 1633 0
651 -649 0
2154 701 1633 0
655 -653 0
697 2152 1633 0
659 -657 0
2150 693 1633 0
663 -661 0
689 2148 1633 0
667 -665 0
2146 685 1633 0
671 -669 0
681 2144 1633 0
675 -673 0
673 676 0
679 -677 0
2142 677 1633 0
683 -681 0
2140 669 1633 0
687 -685 0
2138 665 1633 0
691 -689 0
2136 661 1633 0
695 -693 0
2134 657 1633 0
699 -697 0
2132 653 1633 0
703 -701 0
2130 649 1633 0
707 -705 0
2128 645 1633 0
711 -709 0
2126 641 1633 0
715 -713 0
2560 1633 0
719 -717 0
1636 1633 0
723 -721 0
2194 785 1637 0
727 -725 0
781 2192 1637 0
731 -729 0
2190 777 1637 0
735 -733 0
773 2188 1637 0
739 -737 0
2186 769 1637 0
743 -741 0
765 2184 1637 0
747 -745 0
2182 761 1637 0
751 -749 0
2180 753 1637 0
755 -753 0
749 2178 1637 0
759 -757 0
757 760 0
763 -761 0
2176 745 1637 0
767 -765 0
2174 741 1637 0
771 -769 0
2172 737 1637 0
775 -773 0
2170 733 1637 0
779 -777 0
2168 729 1637 0
783 -781 0
2166 725 1637 0
787 -785 0
2164 721 1637 0
791 -789 0
2562 1637 0
795 -793 0
2142 1637 0
799 -797 0
1640 1637 0
803 -801 0
2230 861 1641 0
807 -805 0
857 2228 1641 0
811 -809 0
2226 853 1641 0
815 -813 0
849 2224 1641 0
819 -817 0
2222 845 1641 0
823 -821 0
2220 837 1641 0
827 -825 0
2218 833 1641 0
831 -829 0
2216 829 1641 0
835 -833 0
825 2214 1641 0
839 -837 0
2212 821 1641 0
843 -841 0
841 844 0
847 -845 0
2210 817 1641 0
851 -849 0
2208 813 1641 0
855 -853 0
2206 809 1641 0
859 -857 0
2204 805 1641 0
863 -861 0
2202 801 1641 0
867 -865 0
2564 1641 0
871 -869 0
2182 1641 0
875 -873 0
2106 1641 0
879 -877 0
1644 1641 0
883 -881 0
2266 937 1645 0
887 -885 0
933 2264 1645 0
891 -889 0
2262 929 1645 0
895 -893 0
2260 921 1645 0
899 -897 0
2258 917 1645 0
903 -901 0
2256 913 1645 0
907 -905 0
2254 909 1645 0
911 -909 0
2252 905 1645 0
915 -913 0
901 2250 1645 0
919 -917 0
2248 897 1645 0
923 -921 0
2246 893 1645 0
927 -925 0
925 928 0
931 -929 0
2244 889 1645 0
935 -933 0
2242 885 1645 0
939 -937 0
2240 881 1645 0
943 -941 0
2566 1645 0
947 -945 0
2222 1645 0
951 -949 0
2146 1645 0
955 -953 0
2070 1645 0
959 -957 0
1648 1645 0
963 -961 0
2302 1013 1649 0
967 -965 0
2300 1005 1649 0
971 -969 0
2298 1001 1649 0
975 -973 0
2296 997 1649 0
979 -977 0
2294 993 1649 0
983 -981 0
2292 989 1649 0
987 -985 0
2290 985 1649 0
991 -989 0
2288 981 1649 0
995 -993 0
977 2286 1649 0
999 -997 0
2284 973 1649 0
1003 -1001 0
2282 969 1649 0
1007 -1005 0
2280 965 1649 0
1011 -1009 0
1009 1012 0
1015 -1013 0
2278 961 1649 0
1019 -1017 0
2568 1649 0
1023 -1021 0
2262 1649 0
1027 -1025 0
2186 1649 0
1031 -1029 0
2110 1649 0
1035 -1033 0
2034 1649 0
1039 -1037 0
1652 1649 0
1043 -1041 0
2338 1085 1653 0
1047 -1045 0
2336 1081 1653 0
1051 -1049 0
2334 1077 1653 0
1055 -1053 0
2332 1073 1653 0
1059 -1057 0
2330 1069 1653 0
1063 -1061 0
2328 1065 1653 0
1067 -1065 0
2326 1061 1653 0
1071 -1069 0
2324 1057 1653 0
1075 -1073 0
1053 2322 1653 0
1079 -1077 0
2320 1049 1653 0
1083 -1081 0
1045 2318 1653 0
1087 -1085 0
2316 1041 1653 0
1091 -1089 0
2570 1653 0
1095 -1093 0
1093 1096 0
1099 -1097 0
2302 1653 0
1103 -1101 0
2226 1653 0
1107 -1105 0
2150 1653 0
1111 -1109 0
2074 1653 0
1115 -1113 0
1998 1653 0
1119 -1117 0
1656 1653 0
1123 -1121 0
2374 1161 1657 0
1127 -1125 0
2372 1157 1657 0
1131 -1129 0
2370 1153 1657 0
1135 -1133 0
2368 1149 1657 0
1139 -1137 0
2366 1145 1657 0
1143 -1141 0
2364 1141 1657 0
1147 -1145 0
2362 1137 1657 0
1151 -1149 0
2360 1133 1657 0
1155 -1153 0
1129 2358 1657 0
1159 -1157 0
2356 1125 1657 0
1163 -1161 0
2354 1121 1657 0
1167 -1165 0
2572 1657 0
1171 -1169 0
2342 1657 0
1175 -1173 0
2266 1657 0
1179 -1177 0
1177 1180 0
1183 -1181 0
2190 1657 0
1187 -1185 0
2114 1657 0
1191 -1189 0
2038 1657 0
1195 -1193 0
1962 1657 0
1199 -1197 0
1660 1657 0
1203 -1201 0
2410 1237 1661 0
1207 -1205 0
2408 1233 1661 0
1211 -1209 0
2406 1229 1661 0
1215 -1213 0
2404 1225 1661 0
1219 -1217 0
2402 1221 1661 0
1223 -1221 0
2400 1217 1661 0
1227 -1225 0
2398 1213 1661 0
1231 -1229 0
2396 1209 1661 0
1235 -1233 0
2394 1205 1661 0
1239 -1237 0
2392 1201 1661 0
1243 -1241 0
2574 1661 0
1247 -1245 0
2382 1661 0
1251 -1249 0
2306 1661 0
1255 -1253 0
2230 1661 0
1259 -1257 0
2154 1661 0
1263 -1261 0
1261 1264 0
1267 -1265 0
2078 1661 0
1271 -1269 0
2002 1661 0
1275 -1273 0
1926 1661 0
1279 -1277 0
1664 1661 0
1283 -1281 0
2446 1313 1665 0
1287 -1285 0
2444 1309 1665 0
1291 -1289 0
2442 1305 1665 0
1295 -1293 0
2440 1301 1665 0
1299 -1297 0
2438 1297 1665 0
1303 -1301 0
2436 1293 1665 0
1307 -1305 0
2434 1289 1665 0
1311 -1309 0
2432 1285 1665 0
1315 -1313 0
1281 2430 1665 0
1319 -1317 0
2576 1665 0
1323 -1321 0
2422 1665 0
1327 -1325 0
2346 1665 0
1331 -1329 0
2270 1665 0
1335 -1333 0
2194 1665 0
1339 -1337 0
2118 1665 0
1343 -1341 0
2042 1665 0
1347 -1345 0
1345 1348 0
1351 -1349 0
1966 1665 0
1355 -1353 0
1890 1665 0
1359 -1357 0
1668 1665 0
1363 -1361 0
2482 1389 1669 0
1367 -1365 0
2480 1385 1669 0
1371 -1369 0
2478 1381 1669 0
1375 -1373 0
2476 1377 1669 0
1379 -1377 0
2474 1373 1669 0
1383 -1381 0
2472 1369 1669 0
1387 -1385 0
2470 1365 1669 0
1391 -1389 0
2468 1361 1669 0
1395 -1393 0
2578 1669 0
1399 -1397 0
2462 1669 0
1403 -1401 0
2386 1669 0
1407 -1405 0
2310 1669 0
1411 -1409 0
2234 1669 0
1415 -1413 0
2158 1669 0
1419 -1417 0
2082 1669 0
1423 -1421 0
2006 1669 0
1427 -1425 0
1930 1669 0
1431 -1429 0
1429 1432 0
1435 -1433 0
1854 1669 0
1439 -1437 0
1672 1669 0
1443 -1441 0
2518 1465 1673 0
1447 -1445 0
2516 1461 1673 0
1451 -1449 0
2514 1457 1673 0
1455 -1453 0
2512 1453 1673 0
1459 -1457 0
2510 1449 1673 0
1463 -1461 0
2508 1445 1673 0
1467 -1465 0
2506 1441 1673 0
1471 -1469 0
2580 1673 0
1475 -1473 0
2502 1673 0
1479 -1477 0
2426 1673 0
1483 -1481 0
2350 1673 0
1487 -1485 0
2274 1673 0
1491 -1489 0
2198 1673 0
1495 -1493 0
2122 1673 0
1499 -1497 0
2046 1673 0
1503 -1501 0
1970 1673 0
1507 -1505 0
1894 1673 0
1511 -1509 0
1817 -1753 1673 0
1515 -1513 0
1513 1516 0
1519 -1517 0
1676 1673 0
1523 -1521 0
2554 1541 1677 0
1527 -1525 0
2552 1537 1677 0
1531 -1529 0
2550 1533 1677 0
1535 -1533 0
2548 1529 1677 0
1539 -1537 0
2546 1525 1677 0
1543 -1541 0
2544 1521 1677 0
1547 -1545 0
2578 1589 1677 0
1551 -1549 0
2542 1677 0
1555 -1553 0
2466 1677 0
1559 -1557 0
2390 1677 0
1563 -1561 0
2314 1677 0
1567 -1565 0
2238 1677 0
1571 -1569 0
2162 1677 0
1575 -1573 0
2086 1677 0
1579 -1577 0
2010 1677 0
1583 -1581 0
1934 1677 0
1587 -1585 0
1858 1677 0
1591 -1589 0
2556 1545 1677 0
1595 -1593 0
1680 1677 0
1599 -1597 0
1597 1600 0
1603 -1601 0
9 1824 1601 0
1607 -1605 0
1860 81 1605 0
1611 -1609 0
1934 237 1609 0
1615 -1613 0
317 1613 1972 0
1619 -1617 0
2010 397 1617 0
1623 -1621 0
477 1621 2048 0
1627 -1625 0
2086 557 1625 0
1631 -1629 0
637 1629 2124 0
1635 -1633 0
2162 717 1633 0
1639 -1637 0
797 1637 2200 0
1643 -1641 0
2238 877 1641 0
1647 -1645 0
957 1645 2276 0
1651 -1649 0
2314 1037 1649 0
1655 -1653 0
1117 2352 1653 0
1659 -1657 0
2390 1197 1657 0
1663 -1661 0
1277 2428 1661 0
1667 -1665 0
2466 1357 1665 0
1671 -1669 0
1437 2504 1669 0
1675 -1673 0
2542 1517 1673 0
1679 -1677 0
1677 2580 1593 0
1683 -1681 0
1782 1681 0
1687 -1685 0
1784 1685 0
1691 -1689 0
1786 1689 0
1695 -1693 0
1788 1693 0
1699 -1697 0
1790 1697 0
1703 -1701 0
1792 1701 0
1707 -1705 0
1794 1705 0
1711 -1709 0
1796 1709 0
1715 -1713 0
1798 1713 0
1719 -1717 0
1800 1717 0
1723 -1721 0
1802 1721 0
1727 -1725 0
1804 1725 0
1731 -1729 0
1806 1729 0
1735 -1733 0
1808 1733 0
1739 -1737 0
1810 1737 0
1743 -1741 0
1812 1741 0
1747 -1745 0
1814 1745 0
1751 -1749 0
1816 1749 0
1755 -1753 0
1818 1753 0
1759 -1757 0
1820 1757 0
2506 1601 0
1782 -1601 0
1684 1681 0
2508 1605 0
1784 -1605 0
1688 1685 0
2510 1609 0
1786 -1609 0
1692 1689 0
2512 1613 0
1788 -1613 0
1696 1693 0
2514 1617 0
1790 -1617 0
1700 1697 0
2516 1621 0
1792 -1621 0
1704 1701 0
2518 1625 0
1794 -1625 0
1708 1705 0
1629 2520 0
1796 -1629 0
1712 1709 0
2522 1633 0
1798 -1633 0
1716 1713 0
2524 1637 0
1800 -1637 0
1720 1717 0
2526 1641 0
1802 -1641 0
1724 1721 0
2528 1645 0
1804 -1645 0
1728 1725 0
2530 1649 0
1806 -1649 0
1732 1729 0
2532 1653 0
1808 -1653 0
1736 1733 0
2534 1657 0
1810 -1657 0
1740 1737 0
2536 1661 0
1812 -1661 0
1744 1741 0
2538 1665 0
1814 -1665 0
1748 1745 0
2540 1669 0
1816 -1669 0
1752 1749 0
2540 1509 1673 0
1818 -1673 0
1756 1753 0
2579 1677 -1593 -1673 0
1820 -1677 0
1760 1757 0
2468 1601 0
5 1821 -1601 -1605 0
-5 1822 -1601 0
8 5 0
2470 1605 0
2392 1601 0
9 1823 -1601 -1609 0
-9 1824 -1601 0
12 9 0
2472 1609 0
2316 1601 0
1825 13 -1601 -1613 0
-13 1826 -1601 0
16 13 0
2474 1613 0
2240 1601 0
1827 17 -1601 -1617 0
-17 1828 -1601 0
20 17 0
2476 1617 0
2164 1601 0
1829 21 -1601 -1621 0
-21 1830 -1601 0
24 21 0
2478 1621 0
2088 1601 0
1831 25 -1601 -1625 0
-25 1832 -1601 0
28 25 0
2480 1625 0
2012 1601 0
1833 29 -1601 -1629 0
-29 1834 -1601 0
32 29 0
2482 1629 0
1936 1601 0
1835 33 -1601 -1633 0
-33 1836 -1601 0
36 33 0
1633 2484 0
1860 1601 0
1837 37 -1601 -1637 0
-37 1838 -1601 0
40 37 0
2486 1637 0
1857 -77 1601 -1677 0
41 1839 -1601 -1641 0
-41 1840 -1601 0
44 41 0
2488 1641 0
1855 -73 1601 -1673 0
45 1841 -1601 -1645 0
-45 1842 -1601 0
48 45 0
2490 1645 0
1853 -69 1601 -1669 0
49 1843 -1601 -1649 0
-49 1844 -1601 0
52 49 0
2492 1649 0
1851 -65 1601 -1665 0
53 1845 -1601 -1653 0
-53 1846 -1601 0
56 53 0
2494 1653 0
1849 -61 1601 -1661 0
1847 57 -1601 -1657 0
-57 1848 -1601 0
60 57 0
2496 1657 0
1847 -57 1601 -1657 0
1849 61 -1601 -1661 0
-61 1850 -1601 0
64 61 0
2498 1661 0
1845 -53 1601 -1653 0
1851 65 -1601 -1665 0
-65 1852 -1601 0
68 65 0
2500 1665 0
1843 -49 1601 -1649 0
1853 69 -1601 -1669 0
1854 -69 -1601 0
72 69 0
2502 1433 1669 0
1841 -45 1601 -1645 0
1855 73 -1601 -1673 0
-73 1856 -1601 0
76 73 0
2541 -1517 1673 -1677 0
1839 -41 1601 -1641 0
1857 77 -1601 -1677 0
1858 -77 -1601 0
80 77 0
2576 1585 1677 0
2432 1605 0
81 1859 -1605 -1601 0
1860 -81 -1605 0
84 81 0
1837 -37 1601 -1637 0
2356 1605 0
89 1861 -1605 -1609 0
-89 1862 -1605 0
92 89 0
2434 1609 0
2280 1605 0
93 1863 -1605 -1613 0
-93 1864 -1605 0
96 93 0
2436 1613 0
2204 1605 0
97 1865 -1605 -1617 0
-97 1866 -1605 0
100 97 0
2438 1617 0
2128 1605 0
101 1867 -1605 -1621 0
-101 1868 -1605 0
104 101 0
2440 1621 0
2052 1605 0
105 1869 -1605 -1625 0
-105 1870 -1605 0
108 105 0
2442 1625 0
1976 1605 0
109 1871 -1605 -1629 0
-109 1872 -1605 0
112 109 0
2444 1629 0
1900 1605 0
113 1873 -1605 -1633 0
-113 1874 -1605 0
116 113 0
2446 1633 0
1895 -157 -1677 1605 0
117 1875 -1605 -1637 0
-117 1876 -1605 0
120 117 0
1637 2448 0
1893 -153 1605 -1673 0
121 1877 -1605 -1641 0
-121 1878 -1605 0
124 121 0
2450 1641 0
1891 1605 -1669 -149 0
125 1879 -1605 -1645 0
-125 1880 -1605 0
128 125 0
2452 1645 0
1889 -145 1605 -1665 0
129 1881 -1605 -1649 0
-129 1882 -1605 0
132 129 0
2454 1649 0
1887 1605 -1661 -141 0
133 1883 -1605 -1653 0
-133 1884 -1605 0
136 133 0
2456 1653 0
1885 -137 1605 -1657 0
1885 137 -1605 -1657 0
-137 1886 -1605 0
140 137 0
2458 1657 0
1883 1605 -1653 -133 0
1887 141 -1605 -1661 0
-141 1888 -1605 0
144 141 0
2460 1661 0
1881 -129 1605 -1649 0
1889 145 -1605 -1665 0
1890 -145 -1605 0
148 145 0
1353 2464 1665 0
1879 1605 -1645 -125 0
1891 149 -1605 -1669 0
-149 1892 -1605 0
152 149 0
2503 1669 -1677 -1437 0
1877 -121 1605 -1641 0
1893 153 -1605 -1673 0
1894 -153 -1605 0
156 153 0
2538 1505 1673 0
1875 -117 1605 -1637 0
1895 157 -1605 -1677 0
-157 -1605 1896 0
160 157 0
2577 -1669 1677 -1589 0
2396 1609 0
161 1897 -1609 -1601 0
1898 -161 -1609 0
164 161 0
37 1838 1601 0
2320 1609 0
165 1899 -1609 -1605 0
1900 -165 -1609 0
168 165 0
1873 -113 1605 -1633 0
2244 1609 0
173 1901 -1609 -1613 0
-173 1902 -1609 0
176 173 0
2398 1613 0
2168 1609 0
177 1903 -1609 -1617 0
-177 1904 -1609 0
180 177 0
2400 1617 0
2092 1609 0
181 1905 -1609 -1621 0
-181 1906 -1609 0
184 181 0
2402 1621 0
2016 1609 0
185 1907 -1609 -1625 0
-185 1908 -1609 0
188 185 0
2404 1625 0
1940 1609 0
189 1909 -1609 -1629 0
-189 1910 -1609 0
192 189 0
2406 1629 0
1933 -237 1609 -1677 0
193 1911 -1609 -1633 0
-193 1912 -1609 0
196 193 0
2408 1633 0
1931 -233 1609 -1673 0
197 1913 -1609 -1637 0
-197 1914 -1609 0
200 197 0
2410 1637 0
1929 -229 1609 -1669 0
201 1915 -1609 -1641 0
-201 1916 -1609 0
204 201 0
1641 2412 0
1927 -225 1609 -1665 0
205 1917 -1609 -1645 0
-205 1918 -1609 0
208 205 0
2414 1645 0
1925 -221 1609 -1661 0
209 1919 -1609 -1649 0
-209 1920 -1609 0
212 209 0
2416 1649 0
1923 -217 1609 -1657 0
1921 213 -1609 -1653 0
-213 1922 -1609 0
216 213 0
2418 1653 0
1921 -213 1609 -1653 0
1923 217 -1609 -1657 0
-217 1924 -1609 0
220 217 0
2420 1657 0
1919 -209 1609 -1649 0
1925 221 -1609 -1661 0
1926 -221 -1609 0
224 221 0
2426 1273 1661 0
1917 -205 1609 -1645 0
1927 225 -1609 -1665 0
-225 1928 -1609 0
228 225 0
2465 -1357 1665 -1677 0
1915 -201 1609 -1641 0
1929 229 -1609 -1669 0
1930 -229 -1609 0
232 229 0
2500 1425 1669 0
1913 -197 1609 -1637 0
1931 233 -1609 -1673 0
-233 1932 -1609 0
236 233 0
2539 -1509 1673 -1669 0
1911 -193 1609 -1633 0
1933 237 -1609 -1677 0
1934 -237 -1609 0
240 237 0
2574 1581 1677 0
2360 1613 0
241 1935 -1613 -1601 0
1936 -241 -1613 0
244 241 0
1835 -33 1601 -1633 0
2284 1613 0
245 1937 -1613 -1605 0
1938 -245 -1613 0
248 245 0
105 1870 1605 0
2208 1613 0
249 1939 -1613 -1609 0
1940 -249 -1613 0
252 249 0
1909 -189 1609 -1629 0
2132 1613 0
257 1941 -1613 -1617 0
-257 1942 -1613 0
260 257 0
2362 1617 0
2056 1613 0
261 1943 -1613 -1621 0
-261 1944 -1613 0
264 261 0
2364 1621 0
1980 1613 0
265 1945 -1613 -1625 0
-265 1946 -1613 0
268 265 0
2366 1625 0
1971 -317 1613 -1677 0
269 1947 -1613 -1629 0
-269 1948 -1613 0
272 269 0
2368 1629 0
1969 1613 -1673 -313 0
273 1949 -1613 -1633 0
-273 1950 -1613 0
276 273 0
2370 1633 0
1967 -309 1613 -1669 0
277 1951 -1613 -1637 0
-277 1952 -1613 0
280 277 0
2372 1637 0
1965 1613 -1665 -305 0
281 1953 -1613 -1641 0
-281 1954 -1613 0
284 281 0
2374 1641 0
1963 -301 1613 -1661 0
285 1955 -1613 -1645 0
-285 1956 -1613 0
288 285 0
1645 2376 0
1961 1613 -1657 -297 0
289 1957 -1613 -1649 0
-289 1958 -1613 0
292 289 0
2378 1649 0
1959 -293 1613 -1653 0
1959 293 -1613 -1653 0
-293 1960 -1613 0
296 293 0
2380 1653 0
1957 1613 -1649 -289 0
1961 297 -1613 -1657 0
1962 -297 -1613 0
300 297 0
1193 2388 1657 0
1955 -285 1613 -1645 0
1963 301 -1613 -1661 0
-301 1964 -1613 0
304 301 0
2427 -1277 1661 -1677 0
1953 1613 -1641 -281 0
1965 305 -1613 -1665 0
1966 -305 -1613 0
308 305 0
2462 1349 1665 0
1951 -277 1613 -1637 0
1967 309 -1613 -1669 0
-309 1968 -1613 0
312 309 0
2501 -1433 1669 -1673 0
1949 -273 1613 -1633 0
1969 313 -1613 -1673 0
1970 -313 -1613 0
316 313 0
2536 1501 1673 0
1947 -269 1613 -1629 0
1971 317 -1613 -1677 0
-317 -1613 1972 0
320 317 0
2575 -1585 1677 -1665 0
2324 1617 0
321 1973 -1617 -1601 0
1974 -321 -1617 0
324 321 0
33 1836 1601 0
2248 1617 0
325 1975 -1617 -1605 0
1976 -325 -1617 0
328 325 0
1871 -109 1605 -1629 0
2172 1617 0
329 1977 -1617 -1609 0
1978 -329 -1617 0
332 329 0
181 1906 1609 0
2096 1617 0
333 1979 -1617 -1613 0
1980 -333 -1617 0
336 333 0
1945 -265 1613 -1625 0
2020 1617 0
341 1981 -1617 -1621 0
-341 1982 -1617 0
344 341 0
2326 1621 0
2009 -397 1617 -1677 0
345 1983 -1617 -1625 0
-345 1984 -1617 0
348 345 0
2328 1625 0
2007 -393 1617 -1673 0
349 1985 -1617 -1629 0
-349 1986 -1617 0
352 349 0
2330 1629 0
2005 -389 1617 -1669 0
353 1987 -1617 -1633 0
-353 1988 -1617 0
356 353 0
2332 1633 0
2003 -385 1617 -1665 0
357 1989 -1617 -1637 0
-357 1990 -1617 0
360 357 0
2334 1637 0
2001 -381 1617 -1661 0
361 1991 -1617 -1641 0
-361 1992 -1617 0
364 361 0
2336 1641 0
1999 -377 1617 -1657 0
365 1993 -1617 -1645 0
-365 1994 -1617 0
368 365 0
2338 1645 0
1997 -373 1617 -1653 0
1995 369 -1617 -1649 0
-369 1996 -1617 0
372 369 0
1649 2340 0
1995 -369 1617 -1649 0
1997 373 -1617 -1653 0
1998 -373 -1617 0
376 373 0
2350 1113 1653 0
1993 -365 1617 -1645 0
1999 377 -1617 -1657 0
-377 2000 -1617 0
380 377 0
2389 -1197 1657 -1677 0
1991 -361 1617 -1641 0
2001 381 -1617 -1661 0
2002 -381 -1617 0
384 381 0
1269 2424 1661 0
1989 -357 1617 -1637 0
2003 385 -1617 -1665 0
-385 2004 -1617 0
388 385 0
2463 -1353 1665 -1673 0
1987 -353 1617 -1633 0
2005 389 -1617 -1669 0
2006 -389 -1617 0
392 389 0
2498 1421 1669 0
1985 -349 1617 -1629 0
2007 393 -1617 -1673 0
-393 2008 -1617 0
396 393 0
2537 -1505 1673 -1665 0
1983 -345 1617 -1625 0
2009 397 -1617 -1677 0
2010 -397 -1617 0
400 397 0
2572 1577 1677 0
2288 1621 0
401 2011 -1621 -1601 0
2012 -401 -1621 0
404 401 0
1833 -29 1601 -1629 0
2212 1621 0
405 2013 -1621 -1605 0
2014 -405 -1621 0
408 405 0
101 1868 1605 0
2136 1621 0
409 2015 -1621 -1609 0
2016 -409 -1621 0
412 409 0
1907 -185 1609 -1625 0
2060 1621 0
413 2017 -1621 -1613 0
2018 -413 -1621 0
416 413 0
257 1942 1613 0
2047 1621 -1677 -477 0
417 2019 -1621 -1617 0
2020 -417 -1621 0
420 417 0
1981 -341 1617 -1621 0
2045 -473 1621 -1673 0
425 2021 -1621 -1625 0
-425 2022 -1621 0
428 425 0
2290 1625 0
2043 1621 -1669 -469 0
429 2023 -1621 -1629 0
-429 2024 -1621 0
432 429 0
2292 1629 0
2041 -465 1621 -1665 0
433 2025 -1621 -1633 0
-433 2026 -1621 0
436 433 0
2294 1633 0
2039 1621 -1661 -461 0
437 2027 -1621 -1637 0
-437 2028 -1621 0
440 437 0
2296 1637 0
2037 -457 1621 -1657 0
441 2029 -1621 -1641 0
-441 2030 -1621 0
444 441 0
2298 1641 0
2035 1621 -1653 -453 0
445 2031 -1621 -1645 0
-445 2032 -1621 0
448 445 0
2300 1645 0
2033 -449 1621 -1649 0
2033 449 -1621 -1649 0
2034 -449 -1621 0
452 449 0
1033 2312 1649 0
2031 1621 -1645 -445 0
2035 453 -1621 -1653 0
-453 2036 -1621 0
456 453 0
2351 1653 -1677 -1117 0
2029 -441 1621 -1641 0
2037 457 -1621 -1657 0
2038 -457 -1621 0
460 457 0
2386 1189 1657 0
2027 1621 -1637 -437 0
2039 461 -1621 -1661 0
-461 2040 -1621 0
464 461 0
2425 1661 -1673 -1273 0
2025 -433 1621 -1633 0
2041 465 -1621 -1665 0
2042 -465 -1621 0
468 465 0
2460 1341 1665 0
2023 -429 1621 -1629 0
2043 469 -1621 -1669 0
-469 2044 -1621 0
472 469 0
2499 -1665 1669 -1425 0
2021 -425 1621 -1625 0
2045 473 -1621 -1673 0
2046 -473 -1621 0
476 473 0
2534 1497 1673 0
2019 -417 1621 -1617 0
2047 477 -1621 -1677 0
-477 -1621 2048 0
480 477 0
2573 -1661 1677 -1581 0
2252 1625 0
481 2049 -1625 -1601 0
2050 -481 -1625 0
484 481 0
29 1834 1601 0
2176 1625 0
485 2051 -1625 -1605 0
2052 -485 -1625 0
488 485 0
1869 -105 1605 -1625 0
2100 1625 0
489 2053 -1625 -1609 0
2054 -489 -1625 0
492 489 0
177 1904 1609 0
2085 -557 1625 -1677 0
493 2055 -1625 -1613 0
2056 -493 -1625 0
496 493 0
1943 -261 1613 -1621 0
2083 -553 1625 -1673 0
497 2057 -1625 -1617 0
2058 -497 -1625 0
500 497 0
1978 329 1617 0
2081 -549 1625 -1669 0
501 2059 -1625 -1621 0
2060 -501 -1625 0
504 501 0
2017 -413 1621 -1613 0
2079 -545 1625 -1665 0
509 2061 -1625 -1629 0
-509 2062 -1625 0
512 509 0
2254 1629 0
2077 -541 1625 -1661 0
513 2063 -1625 -1633 0
-513 2064 -1625 0
516 513 0
2256 1633 0
2075 -537 1625 -1657 0
517 2065 -1625 -1637 0
-517 2066 -1625 0
520 517 0
2258 1637 0
2073 -533 1625 -1653 0
521 2067 -1625 -1641 0
-521 2068 -1625 0
524 521 0
2260 1641 0
2071 -529 1625 -1649 0
2069 525 -1625 -1645 0
2070 -525 -1625 0
528 525 0
2274 953 1645 0
2069 -525 1625 -1645 0
2071 529 -1625 -1649 0
-529 2072 -1625 0
532 529 0
2313 -1037 1649 -1677 0
2067 -521 1625 -1641 0
2073 533 -1625 -1653 0
2074 -533 -1625 0
536 533 0
1109 2348 1653 0
2065 -517 1625 -1637 0
2075 537 -1625 -1657 0
-537 2076 -1625 0
540 537 0
2387 -1193 1657 -1673 0
2063 -513 1625 -1633 0
2077 541 -1625 -1661 0
2078 -541 -1625 0
544 541 0
2422 1265 1661 0
2061 -509 1625 -1629 0
2079 545 -1625 -1665 0
-545 2080 -1625 0
548 545 0
2461 -1349 1665 -1669 0
2059 -501 1625 -1621 0
2081 549 -1625 -1669 0
2082 -549 -1625 0
552 549 0
2496 1417 1669 0
2057 -497 1625 -1617 0
2083 553 -1625 -1673 0
-553 2084 -1625 0
556 553 0
2535 -1501 1673 -1661 0
2055 -493 1625 -1613 0
2085 557 -1625 -1677 0
2086 -557 -1625 0
560 557 0
2570 1573 1677 0
2216 1629 0
561 2087 -1629 -1601 0
2088 -561 -1629 0
564 561 0
1831 -25 1601 -1625 0
2140 1629 0
565 2089 -1629 -1605 0
2090 -565 -1629 0
568 565 0
97 1866 1605 0
2123 -637 1629 -1677 0
569 2091 -1629 -1609 0
2092 -569 -1629 0
572 569 0
1905 -181 1609 -1621 0
2121 1629 -1673 -633 0
573 2093 -1629 -1613 0
2094 -573 -1629 0
576 573 0
1940 249 1613 0
2119 -629 1629 -1669 0
577 2095 -1629 -1617 0
2096 -577 -1629 0
580 577 0
1979 -333 1617 -1613 0
2117 1629 -1665 -625 0
581 2097 -1629 -1621 0
2098 -581 -1629 0
584 581 0
2014 405 1621 0
2115 -621 1629 -1661 0
585 2099 -1629 -1625 0
2100 -585 -1629 0
588 585 0
2053 -489 1625 -1609 0
2113 1629 -1657 -617 0
593 2101 -1629 -1633 0
-593 2102 -1629 0
596 593 0
2218 1633 0
2111 -613 1629 -1653 0
597 2103 -1629 -1637 0
-597 2104 -1629 0
600 597 0
2220 1637 0
2109 1629 -1649 -609 0
601 2105 -1629 -1641 0
2106 -601 -1629 0
604 601 0
873 2236 1641 0
2107 -605 1629 -1645 0
2107 605 -1629 -1645 0
-605 2108 -1629 0
608 605 0
2275 -957 1645 -1677 0
2105 -601 1629 -1641 0
2109 609 -1629 -1649 0
2110 -609 -1629 0
612 609 0
2310 1029 1649 0
2103 -597 1629 -1637 0
2111 613 -1629 -1653 0
-613 2112 -1629 0
616 613 0
2349 -1113 1653 -1673 0
2101 1629 -1633 -593 0
2113 617 -1629 -1657 0
2114 -617 -1629 0
620 617 0
1185 2384 1657 0
2099 -585 1629 -1625 0
2115 621 -1629 -1661 0
-621 2116 -1629 0
624 621 0
2423 -1269 1661 -1669 0
2097 -1621 1629 -581 0
2117 625 -1629 -1665 0
2118 -625 -1629 0
628 625 0
2458 1337 1665 0
2095 -577 1629 -1617 0
2119 629 -1629 -1669 0
-629 2120 -1629 0
632 629 0
2497 -1421 1669 -1661 0
2093 -1613 1629 -573 0
2121 633 -1629 -1673 0
2122 -633 -1629 0
636 633 0
2532 1493 1673 0
2091 -569 1629 -1609 0
2123 637 -1629 -1677 0
-637 2124 -1629 0
640 637 0
2571 -1577 1677 -1657 0
2180 1633 0
641 2125 -1633 -1601 0
2126 -641 -1633 0
644 641 0
25 1832 1601 0
2161 -717 1633 -1677 0
645 2127 -1633 -1605 0
2128 -645 -1633 0
648 645 0
1867 -101 -1621 1605 0
2159 -713 1633 -1673 0
649 2129 -1633 -1609 0
2130 -649 -1633 0
652 649 0
173 1902 1609 0
2157 -709 1633 -1669 0
653 2131 -1633 -1613 0
2132 -653 -1633 0
656 653 0
1941 -257 -1617 1613 0
2155 -705 1633 -1665 0
657 2133 -1633 -1617 0
2134 -657 -1633 0
660 657 0
1976 325 1617 0
2153 -701 1633 -1661 0
661 2135 -1633 -1621 0
2136 -661 -1633 0
664 661 0
2015 -409 1621 -1609 0
2151 -697 1633 -1657 0
665 2137 -1633 -1625 0
2138 -665 -1633 0
668 665 0
2050 481 1625 0
2149 -693 1633 -1653 0
669 2139 -1633 -1629 0
2140 -669 -1633 0
672 669 0
2089 -1605 1629 -565 0
2147 -689 1633 -1649 0
677 2141 -1633 -1637 0
2142 -677 -1633 0
680 677 0
2198 793 1637 0
2145 -685 1633 -1645 0
2143 681 -1633 -1641 0
-681 2144 -1633 0
684 681 0
2237 -877 1641 -1677 0
2143 -681 1633 -1641 0
2145 685 -1633 -1645 0
2146 -685 -1633 0
688 685 0
949 2272 1645 0
2141 -677 1633 -1637 0
2147 689 -1633 -1649 0
-689 2148 -1633 0
692 689 0
2311 -1033 1649 -1673 0
2139 -669 1633 -1629 0
2149 693 -1633 -1653 0
2150 -693 -1633 0
696 693 0
2346 1105 1653 0
2137 -665 1633 -1625 0
2151 697 -1633 -1657 0
-697 2152 -1633 0
700 697 0
2385 -1189 1657 -1669 0
2135 -661 1633 -1621 0
2153 701 -1633 -1661 0
2154 -701 -1633 0
704 701 0
2420 1257 1661 0
2133 -657 1633 -1617 0
2155 705 -1633 -1665 0
-705 2156 -1633 0
708 705 0
2459 -1341 1665 -1661 0
2131 -653 1633 -1613 0
2157 709 -1633 -1669 0
2158 -709 -1633 0
712 709 0
2494 1413 1669 0
2129 -649 1633 -1609 0
2159 713 -1633 -1673 0
-713 2160 -1633 0
716 713 0
2533 -1497 1673 -1657 0
2127 -645 1633 -1605 0
2161 717 -1633 -1677 0
2162 -717 -1633 0
720 717 0
2568 1569 1677 0
2199 1637 -1677 -797 0
721 2163 -1637 -1601 0
2164 -721 -1637 0
724 721 0
1829 -21 1601 -1621 0
2197 -793 1637 -1673 0
725 2165 -1637 -1605 0
2166 -725 -1637 0
728 725 0
93 1864 1605 0
2195 -789 -1669 1637 0
729 2167 -1637 -1609 0
2168 -729 -1637 0
732 729 0
1903 -177 1609 -1617 0
2193 -785 1637 -1665 0
733 2169 -1637 -1613 0
2170 -733 -1637 0
736 733 0
1938 245 1613 0
2191 1637 -1661 -781 0
737 2171 -1637 -1617 0
2172 -737 -1637 0
740 737 0
1977 -329 1617 -1609 0
2189 -777 1637 -1657 0
741 2173 -1637 -1621 0
2174 -741 -1637 0
744 741 0
2012 401 1621 0
2187 1637 -1653 -773 0
745 2175 -1637 -1625 0
2176 -745 -1637 0
748 745 0
2051 -485 1625 -1605 0
2185 -769 1637 -1649 0
749 2177 -1637 -1629 0
-749 2178 -1637 0
752 749 0
2558 1629 0
2183 1637 -1645 -765 0
753 2179 -1637 -1633 0
2180 -753 -1637 0
756 753 0
2125 -641 1633 -1601 0
2181 -761 1637 -1641 0
2181 761 -1637 -1641 0
2182 -761 -1637 0
764 761 0
2234 869 1641 0
2179 -753 1637 -1633 0
2183 765 -1637 -1645 0
-765 2184 -1637 0
768 765 0
2273 1645 -1673 -953 0
2177 -749 1637 -1629 0
2185 769 -1637 -1649 0
2186 -769 -1637 0
772 769 0
1025 2308 1649 0
2175 -745 1637 -1625 0
2187 773 -1637 -1653 0
-773 2188 -1637 0
776 773 0
2347 1653 -1669 -1109 0
2173 -741 1637 -1621 0
2189 777 -1637 -1657 0
2190 -777 -1637 0
780 777 0
2382 1181 1657 0
2171 -737 1637 -1617 0
2191 781 -1637 -1661 0
-781 2192 -1637 0
784 781 0
2421 1661 -1665 -1265 0
2169 -733 1637 -1613 0
2193 785 -1637 -1665 0
2194 -785 -1637 0
788 785 0
2456 1333 1665 0
2167 -729 1637 -1609 0
2195 789 -1637 -1669 0
-789 2196 -1637 0
792 789 0
2495 -1657 1669 -1417 0
2165 -725 1637 -1605 0
2197 793 -1637 -1673 0
2198 -793 -1637 0
796 793 0
2530 1489 1673 0
2163 -721 1637 -1601 0
2199 797 -1637 -1677 0
-797 2200 -1637 0
800 797 0
2569 -1653 1677 -1573 0
2235 -873 1641 -1673 0
801 2201 -1641 -1601 0
2202 -801 -1641 0
804 801 0
21 1830 1601 0
2233 -869 1641 -1669 0
805 2203 -1641 -1605 0
2204 -805 -1641 0
808 805 0
1865 -97 1605 -1617 0
2231 -865 1641 -1665 0
809 2205 -1641 -1609 0
2206 -809 -1641 0
812 809 0
1900 165 1609 0
2229 -861 1641 -1661 0
813 2207 -1641 -1613 0
2208 -813 -1641 0
816 813 0
1939 -249 1613 -1609 0
2227 -857 1641 -1657 0
817 2209 -1641 -1617 0
2210 -817 -1641 0
820 817 0
1974 321 1617 0
2225 -853 1641 -1653 0
821 2211 -1641 -1621 0
2212 -821 -1641 0
824 821 0
2013 -405 1621 -1605 0
2223 -849 1641 -1649 0
825 2213 -1641 -1625 0
-825 2214 -1641 0
828 825 0
2556 1625 0
2221 -845 1641 -1645 0
829 2215 -1641 -1629 0
2216 -829 -1641 0
832 829 0
2087 -561 1629 -1601 0
2219 -837 1641 -1637 0
2217 833 -1641 -1633 0
2218 -833 -1641 0
836 833 0
2102 1633 0
2217 -833 1641 -1633 0
2219 837 -1641 -1637 0
2220 -837 -1641 0
840 837 0
2104 1637 0
2215 -829 1641 -1629 0
2221 845 -1641 -1645 0
2222 -845 -1641 0
848 845 0
2270 945 1645 0
2213 -825 1641 -1625 0
2223 849 -1641 -1649 0
-849 2224 -1641 0
852 849 0
2309 -1029 1649 -1669 0
2211 -821 1641 -1621 0
2225 853 -1641 -1653 0
2226 -853 -1641 0
856 853 0
1101 2344 1653 0
2209 -817 1641 -1617 0
2227 857 -1641 -1657 0
-857 2228 -1641 0
860 857 0
2383 -1185 1657 -1665 0
2207 -813 1641 -1613 0
2229 861 -1641 -1661 0
2230 -861 -1641 0
864 861 0
2418 1253 1661 0
2205 -809 1641 -1609 0
2231 865 -1641 -1665 0
-865 2232 -1641 0
868 865 0
2457 -1337 1665 -1657 0
2203 -805 1641 -1605 0
2233 869 -1641 -1669 0
2234 -869 -1641 0
872 869 0
2492 1409 1669 0
2201 -801 1641 -1601 0
2235 873 -1641 -1673 0
-873 2236 -1641 0
876 873 0
2531 -1493 1673 -1653 0
2144 1641 0
2237 877 -1641 -1677 0
2238 -877 -1641 0
880 877 0
2566 1565 1677 0
2271 -949 1645 -1669 0
881 2239 -1645 -1601 0
2240 -881 -1645 0
884 881 0
1827 -17 1601 -1617 0
2269 1645 -1665 -945 0
885 2241 -1645 -1605 0
2242 -885 -1645 0
888 885 0
89 1862 1605 0
2267 -941 1645 -1661 0
889 2243 -1645 -1609 0
2244 -889 -1645 0
892 889 0
1901 -173 1609 -1613 0
2265 1645 -1657 -937 0
893 2245 -1645 -1613 0
2246 -893 -1645 0
896 893 0
1936 241 1613 0
2263 -933 1645 -1653 0
897 2247 -1645 -1617 0
2248 -897 -1645 0
900 897 0
1975 -325 1617 -1605 0
2261 1645 -1649 -929 0
901 2249 -1645 -1621 0
-901 2250 -1645 0
904 901 0
2554 1621 0
2259 -921 1645 -1641 0
905 2251 -1645 -1625 0
2252 -905 -1645 0
908 905 0
2049 -481 1625 -1601 0
2257 1645 -1637 -917 0
909 2253 -1645 -1629 0
2254 -909 -1645 0
912 909 0
2062 1629 0
2255 -913 1645 -1633 0
2255 913 -1645 -1633 0
2256 -913 -1645 0
916 913 0
2064 1633 0
2253 -909 1645 -1629 0
2257 917 -1645 -1637 0
2258 -917 -1645 0
920 917 0
2066 1637 0
2251 -905 1645 -1625 0
2259 921 -1645 -1641 0
2260 -921 -1645 0
924 921 0
2068 1641 0
2249 -1621 1645 -901 0
2261 929 -1645 -1649 0
2262 -929 -1645 0
932 929 0
2306 1021 1649 0
2247 -897 1645 -1617 0
2263 933 -1645 -1653 0
-933 2264 -1645 0
936 933 0
2345 -1105 1653 -1665 0
2245 -1613 1645 -893 0
2265 937 -1645 -1657 0
2266 -937 -1645 0
940 937 0
2380 1173 1657 0
2243 -889 1645 -1609 0
2267 941 -1645 -1661 0
-941 2268 -1645 0
944 941 0
2419 -1257 1661 -1657 0
2241 -1605 1645 -885 0
2269 945 -1645 -1665 0
2270 -945 -1645 0
948 945 0
2454 1329 1665 0
2239 -881 1645 -1601 0
2271 949 -1645 -1669 0
-949 2272 -1645 0
952 949 0
2493 -1413 1669 -1653 0
2184 1645 0
2273 953 -1645 -1673 0
2274 -953 -1645 0
956 953 0
2528 1485 1673 0
2108 1645 0
2275 957 -1645 -1677 0
-957 2276 -1645 0
960 957 0
2567 -1569 1677 -1649 0
2307 -1025 1649 -1665 0
961 2277 -1649 -1601 0
2278 -961 -1649 0
964 961 0
17 1828 1601 0
2305 -1021 1649 -1661 0
965 2279 -1649 -1605 0
2280 -965 -1649 0
968 965 0
1863 -93 -1613 1605 0
2303 -1017 1649 -1657 0
969 2281 -1649 -1609 0
2282 -969 -1649 0
972 969 0
1898 161 1609 0
2301 -1013 1649 -1653 0
973 2283 -1649 -1613 0
2284 -973 -1649 0
976 973 0
1937 -245 -1605 1613 0
2299 -1005 1649 -1645 0
977 2285 -1649 -1617 0
-977 2286 -1649 0
980 977 0
2552 1617 0
2297 -1001 1649 -1641 0
981 2287 -1649 -1621 0
2288 -981 -1649 0
984 981 0
2011 -401 1621 -1601 0
2295 -997 1649 -1637 0
985 2289 -1649 -1625 0
2290 -985 -1649 0
988 985 0
2022 1625 0
2293 -993 1649 -1633 0
2291 989 -1649 -1629 0
2292 -989 -1649 0
992 989 0
2024 1629 0
2291 -989 1649 -1629 0
2293 993 -1649 -1633 0
2294 -993 -1649 0
996 993 0
2026 1633 0
2289 -985 1649 -1625 0
2295 997 -1649 -1637 0
2296 -997 -1649 0
1000 997 0
2028 1637 0
2287 -981 1649 -1621 0
2297 1001 -1649 -1641 0
2298 -1001 -1649 0
1004 1001 0
2030 1641 0
2285 -977 1649 -1617 0
2299 1005 -1649 -1645 0
2300 -1005 -1649 0
1008 1005 0
2032 1645 0
2283 -973 1649 -1613 0
2301 1013 -1649 -1653 0
2302 -1013 -1649 0
1016 1013 0
2342 1097 1653 0
2281 -969 1649 -1609 0
2303 1017 -1649 -1657 0
-1017 2304 -1649 0
1020 1017 0
2381 -1181 1657 -1661 0
2279 -965 1649 -1605 0
2305 1021 -1649 -1661 0
2306 -1021 -1649 0
1024 1021 0
2416 1249 1661 0
2277 -961 1649 -1601 0
2307 1025 -1649 -1665 0
-1025 2308 -1649 0
1028 1025 0
2455 -1333 1665 -1653 0
2224 1649 0
2309 1029 -1649 -1669 0
2310 -1029 -1649 0
1032 1029 0
2490 1405 1669 0
2148 1649 0
2311 1033 -1649 -1673 0
-1033 2312 -1649 0
1036 1033 0
2529 -1489 1673 -1649 0
2072 1649 0
2313 1037 -1649 -1677 0
2314 -1037 -1649 0
1040 1037 0
2564 1561 1677 0
2343 1653 -1661 -1101 0
1041 2315 -1653 -1601 0
2316 -1041 -1653 0
1044 1041 0
1825 -13 1601 -1613 0
2341 -1097 1653 -1657 0
1045 2317 -1653 -1605 0
-1045 2318 -1653 0
1048 1045 0
2546 1605 0
2339 -1089 -1649 1653 0
1049 2319 -1653 -1609 0
2320 -1049 -1653 0
1052 1049 0
1899 -165 1609 -1605 0
2337 -1085 1653 -1645 0
1053 2321 -1653 -1613 0
-1053 2322 -1653 0
1056 1053 0
2550 1613 0
2335 1653 -1641 -1081 0
1057 2323 -1653 -1617 0
2324 -1057 -1653 0
1060 1057 0
1973 -321 1617 -1601 0
2333 -1077 1653 -1637 0
1061 2325 -1653 -1621 0
2326 -1061 -1653 0
1064 1061 0
1982 1621 0
2331 1653 -1633 -1073 0
1065 2327 -1653 -1625 0
2328 -1065 -1653 0
1068 1065 0
1984 1625 0
2329 -1069 1653 -1629 0
2329 1069 -1653 -1629 0
2330 -1069 -1653 0
1072 1069 0
1986 1629 0
2327 -1065 1653 -1625 0
2331 1073 -1653 -1633 0
2332 -1073 -1653 0
1076 1073 0
1988 1633 0
2325 -1061 1653 -1621 0
2333 1077 -1653 -1637 0
2334 -1077 -1653 0
1080 1077 0
1990 1637 0
2323 -1057 1653 -1617 0
2335 1081 -1653 -1641 0
2336 -1081 -1653 0
1084 1081 0
1992 1641 0
2321 -1053 1653 -1613 0
2337 1085 -1653 -1645 0
2338 -1085 -1653 0
1088 1085 0
1994 1645 0
2319 -1049 1653 -1609 0
2339 -1653 1089 -1649 0
-1089 -1653 2340 0
1092 1089 0
1996 1649 0
2317 -1045 1653 -1605 0
2341 1097 -1653 -1657 0
2342 -1097 -1653 0
1100 1097 0
2378 1169 1657 0
2315 -1041 1653 -1601 0
2343 1101 -1653 -1661 0
-1101 2344 -1653 0
1104 1101 0
2417 -1653 1661 -1253 0
2264 1653 0
2345 1105 -1653 -1665 0
2346 -1105 -1653 0
1108 1105 0
2452 1325 1665 0
2188 1653 0
2347 1109 -1653 -1669 0
-1109 2348 -1653 0
1112 1109 0
2491 -1649 1669 -1409 0
2112 1653 0
2349 1113 -1653 -1673 0
2350 -1113 -1653 0
1116 1113 0
2526 1481 1673 0
2036 1653 0
2351 1117 -1653 -1677 0
-1117 2352 -1653 0
1120 1117 0
2565 -1645 1677 -1565 0
2379 -1173 1657 -1653 0
1121 2353 -1657 -1601 0
2354 -1121 -1657 0
1124 1121 0
13 1826 1601 0
2377 -1169 1657 -1649 0
1125 2355 -1657 -1605 0
2356 -1125 -1657 0
1128 1125 0
1861 -89 1605 -1609 0
2375 -1165 1657 -1645 0
1129 2357 -1657 -1609 0
-1129 2358 -1657 0
1132 1129 0
2548 1609 0
2373 -1161 1657 -1641 0
1133 2359 -1657 -1613 0
2360 -1133 -1657 0
1136 1133 0
1935 -241 1613 -1601 0
2371 -1157 1657 -1637 0
1137 2361 -1657 -1617 0
2362 -1137 -1657 0
1140 1137 0
1942 1617 0
2369 -1153 1657 -1633 0
1141 2363 -1657 -1621 0
2364 -1141 -1657 0
1144 1141 0
1944 1621 0
2367 -1149 1657 -1629 0
2365 1145 -1657 -1625 0
2366 -1145 -1657 0
1148 1145 0
1946 1625 0
2365 -1145 1657 -1625 0
2367 1149 -1657 -1629 0
2368 -1149 -1657 0
1152 1149 0
1948 1629 0
2363 -1141 1657 -1621 0
2369 1153 -1657 -1633 0
2370 -1153 -1657 0
1156 1153 0
1950 1633 0
2361 -1137 1657 -1617 0
2371 1157 -1657 -1637 0
2372 -1157 -1657 0
1160 1157 0
1952 1637 0
2359 -1133 1657 -1613 0
2373 1161 -1657 -1641 0
2374 -1161 -1657 0
1164 1161 0
1954 1641 0
2357 -1129 1657 -1609 0
2375 -1657 1165 -1645 0
-1165 -1657 2376 0
1168 1165 0
1956 1645 0
2355 -1125 1657 -1605 0
2377 1169 -1657 -1649 0
2378 -1169 -1657 0
1172 1169 0
1958 1649 0
2353 -1121 1657 -1601 0
2379 1173 -1657 -1653 0
2380 -1173 -1657 0
1176 1173 0
1960 1653 0
2304 1657 0
2381 1181 -1657 -1661 0
2382 -1181 -1657 0
1184 1181 0
2414 1245 1661 0
2228 1657 0
2383 1185 -1657 -1665 0
-1185 2384 -1657 0
1188 1185 0
2453 -1329 1665 -1649 0
2152 1657 0
2385 1189 -1657 -1669 0
2386 -1189 -1657 0
1192 1189 0
2488 1401 1669 0
2076 1657 0
2387 1193 -1657 -1673 0
-1193 2388 -1657 0
1196 1193 0
2527 -1485 1673 -1645 0
2000 1657 0
2389 1197 -1657 -1677 0
2390 -1197 -1657 0
1200 1197 0
2562 1557 1677 0
2415 -1249 1661 -1649 0
1201 2391 -1661 -1601 0
2392 -1201 -1661 0
1204 1201 0
1823 -9 1601 -1609 0
2413 -1645 1661 -1245 0
1205 2393 -1661 -1605 0
2394 -1205 -1661 0
1208 1205 0
157 1605 1896 0
2411 -1241 1661 -1641 0
1209 2395 -1661 -1609 0
2396 -1209 -1661 0
1212 1209 0
1897 -161 1609 -1601 0
2409 1661 -1637 -1237 0
1213 2397 -1661 -1613 0
2398 -1213 -1661 0
1216 1213 0
1902 1613 0
2407 -1233 1661 -1633 0
1217 2399 -1661 -1617 0
2400 -1217 -1661 0
1220 1217 0
1904 1617 0
2405 1661 -1629 -1229 0
1221 2401 -1661 -1621 0
2402 -1221 -1661 0
1224 1221 0
1906 1621 0
2403 -1225 1661 -1625 0
2403 1225 -1661 -1625 0
2404 -1225 -1661 0
1228 1225 0
1908 1625 0
2401 -1221 1661 -1621 0
2405 1229 -1661 -1629 0
2406 -1229 -1661 0
1232 1229 0
1910 1629 0
2399 -1217 1661 -1617 0
2407 1233 -1661 -1633 0
2408 -1233 -1661 0
1236 1233 0
1912 1633 0
2397 -1213 1661 -1613 0
2409 1237 -1661 -1637 0
2410 -1237 -1661 0
1240 1237 0
1914 1637 0
2395 -1209 1661 -1609 0
2411 -1661 1241 -1641 0
-1241 -1661 2412 0
1244 1241 0
1916 1641 0
2393 -1605 1661 -1205 0
2413 1245 -1661 -1645 0
2414 -1245 -1661 0
1248 1245 0
1918 1645 0
2391 -1201 1661 -1601 0
2415 1249 -1661 -1649 0
2416 -1249 -1661 0
1252 1249 0
1920 1649 0
2344 1661 0
2417 1253 -1661 -1653 0
2418 -1253 -1661 0
1256 1253 0
1922 1653 0
2268 1661 0
2419 1257 -1661 -1657 0
2420 -1257 -1661 0
1260 1257 0
1924 1657 0
2192 1661 0
2421 1265 -1661 -1665 0
2422 -1265 -1661 0
1268 1265 0
2450 1321 1665 0
2116 1661 0
2423 1269 -1661 -1669 0
-1269 2424 -1661 0
1272 1269 0
2489 -1405 1669 -1645 0
2040 1661 0
2425 1273 -1661 -1673 0
2426 -1273 -1661 0
1276 1273 0
2524 1477 1673 0
1964 1661 0
2427 1277 -1661 -1677 0
-1277 2428 -1661 0
1280 1277 0
2563 -1561 1677 -1641 0
2451 -1325 1665 -1645 0
1281 2429 -1665 -1601 0
-1281 2430 -1665 0
1284 1281 0
2544 1601 0
2449 -1321 1665 -1641 0
1285 2431 -1665 -1605 0
2432 -1285 -1665 0
1288 1285 0
1859 -81 1605 -1601 0
2447 -1317 1665 -1637 0
1289 2433 -1665 -1609 0
2434 -1289 -1665 0
1292 1289 0
1862 1609 0
2445 -1313 1665 -1633 0
1293 2435 -1665 -1613 0
2436 -1293 -1665 0
1296 1293 0
1864 1613 0
2443 -1309 1665 -1629 0
1297 2437 -1665 -1617 0
2438 -1297 -1665 0
1300 1297 0
1866 1617 0
2441 -1305 1665 -1625 0
2439 1301 -1665 -1621 0
2440 -1301 -1665 0
1304 1301 0
1868 1621 0
2439 -1301 1665 -1621 0
2441 1305 -1665 -1625 0
2442 -1305 -1665 0
1308 1305 0
1870 1625 0
2437 -1297 1665 -1617 0
2443 1309 -1665 -1629 0
2444 -1309 -1665 0
1312 1309 0
1872 1629 0
2435 -1293 1665 -1613 0
2445 1313 -1665 -1633 0
2446 -1313 -1665 0
1316 1313 0
1874 1633 0
2433 -1289 1665 -1609 0
2447 -1665 1317 -1637 0
-1317 -1665 2448 0
1320 1317 0
1876 1637 0
2431 -1285 1665 -1605 0
2449 1321 -1665 -1641 0
2450 -1321 -1665 0
1324 1321 0
1878 1641 0
2429 -1281 1665 -1601 0
2451 1325 -1665 -1645 0
2452 -1325 -1665 0
1328 1325 0
1880 1645 0
2384 1665 0
2453 1329 -1665 -1649 0
2454 -1329 -1665 0
1332 1329 0
1882 1649 0
2308 1665 0
2455 1333 -1665 -1653 0
2456 -1333 -1665 0
1336 1333 0
1884 1653 0
2232 1665 0
2457 1337 -1665 -1657 0
2458 -1337 -1665 0
1340 1337 0
1886 1657 0
2156 1665 0
2459 1341 -1665 -1661 0
2460 -1341 -1665 0
1344 1341 0
1888 1661 0
2080 1665 0
2461 1349 -1665 -1669 0
2462 -1349 -1665 0
1352 1349 0
2486 1397 1669 0
2004 1665 0
2463 1353 -1665 -1673 0
-1353 2464 -1665 0
1356 1353 0
2525 -1481 1673 -1641 0
1928 1665 0
2465 1357 -1665 -1677 0
2466 -1357 -1665 0
1360 1357 0
2560 1553 1677 0
2487 -1641 1669 -1401 0
1361 2467 -1669 -1601 0
2468 -1361 -1669 0
1364 1361 0
1821 -5 1601 -1605 0
2485 -1397 1669 -1637 0
1365 2469 -1669 -1605 0
2470 -1365 -1669 0
1368 1365 0
1822 1605 0
2483 -1393 -1633 1669 0
1369 2471 -1669 -1609 0
2472 -1369 -1669 0
1372 1369 0
1824 1609 0
2481 -1389 1669 -1629 0
1373 2473 -1669 -1613 0
2474 -1373 -1669 0
1376 1373 0
1826 1613 0
2479 -1625 1669 -1385 0
1377 2475 -1669 -1617 0
2476 -1377 -1669 0
1380 1377 0
1828 1617 0
2477 -1381 1669 -1621 0
2477 1381 -1669 -1621 0
2478 -1381 -1669 0
1384 1381 0
1830 1621 0
2475 -1377 1669 -1617 0
2479 1385 -1669 -1625 0
2480 -1385 -1669 0
1388 1385 0
1832 1625 0
2473 -1373 1669 -1613 0
2481 1389 -1669 -1629 0
2482 -1389 -1669 0
1392 1389 0
1834 1629 0
2471 -1369 1669 -1609 0
2483 -1669 1393 -1633 0
-1393 -1669 2484 0
1396 1393 0
1836 1633 0
2469 -1365 1669 -1605 0
2485 1397 -1669 -1637 0
2486 -1397 -1669 0
1400 1397 0
1838 1637 0
2467 -1361 1669 -1601 0
2487 1401 -1669 -1641 0
2488 -1401 -1669 0
1404 1401 0
1840 1641 0
2424 1669 0
2489 1405 -1669 -1645 0
2490 -1405 -1669 0
1408 1405 0
1842 1645 0
2348 1669 0
2491 1409 -1669 -1649 0
2492 -1409 -1669 0
1412 1409 0
1844 1649 0
2272 1669 0
2493 1413 -1669 -1653 0
2494 -1413 -1669 0
1416 1413 0
1846 1653 0
2196 1669 0
2495 1417 -1669 -1657 0
2496 -1417 -1669 0
1420 1417 0
1848 1657 0
2120 1669 0
2497 1421 -1669 -1661 0
2498 -1421 -1669 0
1424 1421 0
1850 1661 0
2044 1669 0
2499 1425 -1669 -1665 0
2500 -1425 -1669 0
1428 1425 0
1852 1665 0
1968 1669 0
2501 1433 -1669 -1673 0
2502 -1433 -1669 0
1436 1433 0
2522 1473 1673 0
1892 1669 0
2503 1437 -1669 -1677 0
-1437 2504 -1669 0
1440 1437 0
2561 -1637 1677 -1557 0
2523 -1477 1673 -1637 0
1441 2505 -1673 -1601 0
2506 -1441 -1673 0
1444 1441 0
1781 -1681 1601 0
2521 -1473 1673 -1633 0
1445 2507 -1673 -1605 0
2508 -1445 -1673 0
1448 1445 0
1783 -1685 1605 0
2519 -1469 1673 -1629 0
1449 2509 -1673 -1609 0
2510 -1449 -1673 0
1452 1449 0
1785 -1689 1609 0
2517 -1465 1673 -1625 0
1453 2511 -1673 -1613 0
2512 -1453 -1673 0
1456 1453 0
1787 -1693 1613 0
2515 -1461 1673 -1621 0
2513 1457 -1673 -1617 0
2514 -1457 -1673 0
1460 1457 0
1789 -1697 1617 0
2513 -1457 1673 -1617 0
2515 1461 -1673 -1621 0
2516 -1461 -1673 0
1464 1461 0
1791 -1701 1621 0
2511 -1453 1673 -1613 0
2517 1465 -1673 -1625 0
2518 -1465 -1673 0
1468 1465 0
1793 -1705 1625 0
2509 -1449 1673 -1609 0
2519 -1673 1469 -1629 0
-1469 -1673 2520 0
1472 1469 0
1795 -1709 1629 0
2507 -1445 1673 -1605 0
2521 1473 -1673 -1633 0
2522 -1473 -1673 0
1476 1473 0
1797 -1713 1633 0
2505 -1441 1673 -1601 0
2523 1477 -1673 -1637 0
2524 -1477 -1673 0
1480 1477 0
1799 -1717 1637 0
2464 1673 0
2525 1481 -1673 -1641 0
2526 -1481 -1673 0
1484 1481 0
1801 -1721 1641 0
2388 1673 0
2527 1485 -1673 -1645 0
2528 -1485 -1673 0
1488 1485 0
1803 -1725 1645 0
2312 1673 0
2529 1489 -1673 -1649 0
2530 -1489 -1673 0
1492 1489 0
1805 -1729 1649 0
2236 1673 0
2531 1493 -1673 -1653 0
2532 -1493 -1673 0
1496 1493 0
1807 -1733 1653 0
2160 1673 0
2533 1497 -1673 -1657 0
2534 -1497 -1673 0
1500 1497 0
1809 -1737 1657 0
2084 1673 0
2535 1501 -1673 -1661 0
2536 -1501 -1673 0
1504 1501 0
1811 -1741 1661 0
2008 1673 0
2537 1505 -1673 -1665 0
2538 -1505 -1673 0
1508 1505 0
1813 -1745 1665 0
1932 1673 0
2539 1509 -1673 -1669 0
2540 -1509 -1673 0
1512 1509 0
1815 -1749 1669 0
1856 1673 0
2541 1517 -1673 -1677 0
2542 -1517 -1673 0
1520 1517 0
2558 1549 1677 0
2559 -1553 1677 -1633 0
1521 2543 -1677 -1601 0
2544 -1521 -1677 0
1524 1521 0
2430 1601 0
2557 1677 -1629 -1549 0
1525 2545 -1677 -1605 0
2546 -1525 -1677 0
1528 1525 0
2318 1605 0
2555 -1545 1677 -1625 0
1529 2547 -1677 -1609 0
2548 -1529 -1677 0
1532 1529 0
2358 1609 0
2553 -1621 1677 -1541 0
1533 2549 -1677 -1613 0
2550 -1533 -1677 0
1536 1533 0
2322 1613 0
2551 -1537 1677 -1617 0
2551 1537 -1677 -1617 0
2552 -1537 -1677 0
1540 1537 0
2286 1617 0
2549 -1533 1677 -1613 0
2553 1541 -1677 -1621 0
2554 -1541 -1677 0
1544 1541 0
2250 1621 0
2547 -1529 1677 -1609 0
2555 1545 -1677 -1625 0
2556 -1545 -1677 0
1548 1545 0
2214 1625 0
2545 -1525 1677 -1605 0
2557 1549 -1677 -1629 0
2558 -1549 -1677 0
1552 1549 0
2178 1629 0
2543 -1521 1677 -1601 0
2559 1553 -1677 -1633 0
2560 -1553 -1677 0
1556 1553 0
713 1633 2160 0
2504 1677 0
2561 1557 -1677 -1637 0
2562 -1557 -1677 0
1560 1557 0
789 2196 1637 0
2428 1677 0
2563 1561 -1677 -1641 0
2564 -1561 -1677 0
1564 1561 0
865 2232 1641 0
2352 1677 0
2565 1565 -1677 -1645 0
2566 -1565 -1677 0
1568 1565 0
941 2268 1645 0
2276 1677 0
2567 1569 -1677 -1649 0
2568 -1569 -1677 0
1572 1569 0
1017 2304 1649 0
2200 1677 0
2569 1573 -1677 -1653 0
2570 -1573 -1677 0
1576 1573 0
2340 1089 1653 0
2124 1677 0
2571 1577 -1677 -1657 0
2572 -1577 -1677 0
1580 1577 0
2376 1165 1657 0
2048 1677 0
2573 1581 -1677 -1661 0
2574 -1581 -1677 0
1584 1581 0
2412 1241 1661 0
1972 1677 0
2575 1585 -1677 -1665 0
2576 -1585 -1677 0
1588 1585 0
2448 1317 1665 0
1896 1677 0
2577 1589 -1677 -1669 0
2578 -1589 -1677 0
1592 1589 0
2484 1393 1669 0
1819 -1757 1677 0
2579 -1677 1593 -1673 0
2580 -1593 -1677 0
1596 1593 0
2520 1469 1673 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
c The variables forgot
1598 0
1514 0
1430 0
1346 0
1262 0
1178 0
1094 0
1010 0
926 0
842 0
758 0
674 0
590 0
506 0
422 0
338 0
254 0
170 0
86 0
2 0
1758 0
1754 0
1750 0
1746 0
1742 0
1738 0
1734 0
1730 0
1726 0
1722 0
1718 0
1714 0
1710 0
1706 0
1702 0
1698 0
1694 0
1690 0
1686 0
1682 0
6 0
90 0
94 0
98 0
102 0
106 0
110 0
114 0
118 0
122 0
126 0
130 0
134 0
138 0
142 0
146 0
150 0
154 0
158 0
162 0
166 0
174 0
178 0
182 0
186 0
190 0
194 0
198 0
202 0
206 0
210 0
214 0
218 0
222 0
226 0
230 0
234 0
238 0
242 0
246 0
250 0
258 0
262 0
266 0
270 0
274 0
278 0
282 0
286 0
290 0
294 0
298 0
302 0
306 0
310 0
314 0
318 0
322 0
326 0
330 0
334 0
342 0
346 0
350 0
354 0
358 0
362 0
366 0
370 0
374 0
378 0
382 0
386 0
390 0
394 0
398 0
402 0
406 0
410 0
414 0
418 0
426 0
430 0
434 0
438 0
442 0
446 0
450 0
454 0
458 0
462 0
466 0
470 0
474 0
478 0
482 0
486 0
490 0
494 0
498 0
502 0
510 0
514 0
518 0
522 0
526 0
530 0
534 0
538 0
542 0
546 0
550 0
554 0
558 0
562 0
566 0
570 0
574 0
578 0
582 0
586 0
594 0
598 0
602 0
606 0
610 0
614 0
618 0
622 0
626 0
630 0
634 0
638 0
642 0
646 0
650 0
654 0
658 0
662 0
666 0
670 0
678 0
682 0
686 0
690 0
694 0
698 0
702 0
706 0
710 0
714 0
718 0
722 0
726 0
730 0
734 0
738 0
742 0
746 0
750 0
754 0
762 0
766 0
770 0
774 0
778 0
782 0
786 0
790 0
794 0
798 0
802 0
806 0
810 0
814 0
818 0
822 0
826 0
830 0
834 0
838 0
846 0
850 0
854 0
858 0
862 0
866 0
870 0
874 0
878 0
882 0
886 0
890 0
894 0
898 0
902 0
906 0
910 0
914 0
918 0
922 0
930 0
934 0
938 0
942 0
946 0
950 0
954 0
958 0
962 0
966 0
970 0
974 0
978 0
982 0
986 0
990 0
994 0
998 0
1002 0
1006 0
1014 0
1018 0
1022 0
1026 0
1030 0
1034 0
1038 0
1042 0
1046 0
1050 0
1054 0
1058 0
1062 0
1066 0
1070 0
1074 0
1078 0
1082 0
1086 0
1090 0
1098 0
1102 0
1106 0
1110 0
1114 0
1118 0
1122 0
1126 0
1130 0
1134 0
1138 0
1142 0
1146 0
1150 0
1154 0
1158 0
1162 0
1166 0
1170 0
1174 0
1182 0
1186 0
1190 0
1194 0
1198 0
1202 0
1206 0
1210 0
1214 0
1218 0
1222 0
1226 0
1230 0
1234 0
1238 0
1242 0
1246 0
1250 0
1254 0
1258 0
1266 0
1270 0
1274 0
1278 0
1282 0
1286 0
1290 0
1294 0
1298 0
1302 0
1306 0
1310 0
1314 0
1318 0
1322 0
1326 0
1330 0
1334 0
1338 0
1342 0
1350 0
1354 0
1358 0
1362 0
1366 0
1370 0
1374 0
1378 0
1382 0
1386 0
1390 0
1394 0
1398 0
1402 0
1406 0
1410 0
1414 0
1418 0
1422 0
1426 0
1434 0
1438 0
1442 0
1446 0
1450 0
1454 0
1458 0
1462 0
1466 0
1470 0
1474 0
1478 0
1482 0
1486 0
1490 0
1494 0
1498 0
1502 0
1506 0
1510 0
1518 0
1522 0
1526 0
1530 0
1534 0
1538 0
1542 0
1546 0
1550 0
1554 0
1558 0
1562 0
1566 0
1570 0
1574 0
1578 0
1582 0
1586 0
1590 0
1594 0
82 0
78 0
74 0
70 0
66 0
62 0
58 0
54 0
50 0
46 0
42 0
38 0
34 0
30 0
26 0
22 0
18 0
14 0
10 0
1602 0
1678 0
1674 0
1670 0
1666 0
1662 0
1658 0
1654 0
1650 0
1646 0
1642 0
1638 0
1634 0
1630 0
1626 0
1622 0
1618 0
1614 0
1610 0
1606 0

Segmentation fault when running Ganak

Ganak ends up with a segmentation fault when running on the attached .cnf file
(executed as ./ganak buggy.cnf). I had to zip the .cnf file for upload so unzip it.

buggy.zip

The following is the report produced by valgrind:
==25159== Invalid read of size 8
==25159== at 0x485561B: Instance::deleteConflictClauses() (instance.cpp:247)
==25159== by 0x485C2C7: Solver::resolveConflict() (solver.cpp:627)
==25159== by 0x485E6D7: Solver::countSAT() (solver.cpp:251)
==25159== by 0x4861210: Solver::solve(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&) (solver.cpp:207)
==25159== by 0x10A426: main (main.cpp:168)
==25159== Address 0x0 is not stack'd, malloc'd or (recently) free'd
==25159==
==25159==
==25159== Process terminating with default action of signal 11 (SIGSEGV)
==25159== Access not within mapped region at address 0x0
==25159== at 0x485561B: Instance::deleteConflictClauses() (instance.cpp:247)
==25159== by 0x485C2C7: Solver::resolveConflict() (solver.cpp:627)
==25159== by 0x485E6D7: Solver::countSAT() (solver.cpp:251)
==25159== by 0x4861210: Solver::solve(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&) (solver.cpp:207)
==25159== by 0x10A426: main (main.cpp:168)

Based on my inspection of the code, the vector tmp_ratiosB (in function deleteConflictClauses (instance.cpp)) is empty when calling tmp_ratiosB[tmp_ratiosB.size()/2].
A possible fix is to check whether the vector is empty and if yes, then terminate the function (returning True). However, I do not know if this fix is sound (I do not know how exactly Ganak works).

Please, check the issue.
Thanks, Jaroslav

This line keeps being printed non-stop

Here:

ganak/src/instance.cpp

Line 305 in 66d056e

cout << "c invalid weight format" << endl;

Even though all it's paring is a valid weight, right? I have lines like:

w 37 0.500000
w 38 0.610000
w 39 0.390000
w 40 0.090000

See issue #16 for the CNF

@smsharma1 I think this is incorrect printing? Also, this parsing is incredibly fragile, I'm super afraid this will not be warning of incorrect weights. Yep, this gets parsed with exactly the same number of useless warnings:

w 38 0.610000.5

Incorrect model count in Ganak and SharpSAT

I have found an instance with 87 variables and 25 clauses in which both Ganak and SharpSAT disagree with MiniCD2 (http://reasoning.cs.ucla.edu/c2d/), Cachet (https://www.cs.rochester.edu/u/kautz/Cachet/index.htm), and a model counter which I'm implementing from scratch. The instance is available in https://www.cs.helsinki.fi/u/tukotu/bug.cnf.

The output of Ganak and SharpSAT is
9674458629986262485827584
and the output of MiniCD2, Cachet, and my model counter is
9674458629986261412085760

I don't know if MiniCD2 and Cachet are independent implementations, but my implementation is independent from both of them and currently very simple, so therefore I believe that the bug is originating from SharpSAT, and Ganak has inherited it. I'm posting the issue here instead of SharpSAT repo because it seems that Ganak is being maintained unlike SharpSAT.

I have spend some time on trying to minify the bug instance, in particular, it is currently minimal in terms of removal of clauses.

Edit: Should be noted that I have also found instances in which Ganak and SharpSAT agree with my model counter, but MiniCD2 and Cachet disagree with them but agree with each other. So I'm not 100% confident that this is SharpSAT/Ganak bug.

Compilation problems on mac

Build fails on Linux

Hi,
I failed to build this with the following log. Can you check this out?

`
/ganak-master/build$ cmake
-- LIB directory is ''
-- BIN directory is ''
-- Doing a RelWithDebInfo build
-- Compiling for dynamic library use
-- build type is RelWithDebInfo
-- Performing Test HAVE_FLAG_-mtune=native
-- Performing Test HAVE_FLAG_-mtune=native - Success
'--'
-- Performing Test HAVE_FLAG_-std=c99
-- Performing Test HAVE_FLAG_-std=c99 - Success
CMake Error at build/CMakeFiles/git-data/grabRef.cmake:36 (file):
file failed to open for reading (No such file or directory):

''xxxxx''/ganak-master/build/CMakeFiles/git-data/head-ref
Call Stack (most recent call first):
cmake/GetGitRevisionDescription.cmake:70 (include)
CMakeLists.txt:309 (get_git_head_revision)

-- GIT hash found:
-- PROJECT_VERSION: 1.0.1
-- PROJECT_VERSION_MAJOR: 1
-- PROJECT_VERSION_MINOR: 0
-- PROJECT_VERSION_PATCH: 1
-- Configuring incomplete, errors occurred!`

A potential bug with CNF Examples while using Ganak

Hi!
I recently encountered an issue while utilizing Ganak. I attempted to process two CNF files using Ganak. I set the timeout of running the model counter to 600 seconds.
The origin.cnf file can be processed soon while the new.cnf file cannot stop withing 600 seconds. The two files differ by only one clause (origin.cnf is "64 -92 -5 -62 38 0" while new.cnf is "64 -92 -92 -5 -62 38 0") and produce completely opposite results. To assist the diagnosis, I conducted further tests: the critical clause "64 -92 -92 -5 -62 38 0" and the key variable "92" in new.cnf, which seem to be causing the timeout.
I think Ganak may have a potential bug, and I hope this information can assist you to address the potential bugs. The two example files are attached here for your reference.
Best regards,

Haiyan and Jifeng
CSTAR group

Model Count for full counting benchmarks

Hello,

Would it be possible to post a list of all the instances in the counting benchmarks (zip linked in the description) alongside with the exact model count? (for example in a csv file)

Thank you

Incorrect weighted model count because of learn-and-start-over?

Dear ganak developers and maintainers,

I'm running some experiments on the wmc branch and there is one instance for which the weighted model count returned by ganak is twice that of the weighted model count returned by Cachet, ace (it's an encoding of a Bayesian Network), and my own version of weighted sharpSAT.
To be specific: ganak returns 1.20932839536671822778, while the other solvers return 0.604664197683359113891.

I have always had the -noPMC and -noPCC flags, but I have played with different branching heuristics, with always the same result.

However: when I turn LSO off, the weighted model count returned by ganak matches the model count returned by the other solvers.

I'm guessing I can for now just work around this problem by disabling LSO for my experiments, but it would be nice to fix this, if it is indeed buggy behaviour, or otherwise just understand it better. Could you maybe help with this? Am I missing or misunderstanding something?

---

A few more thoughts on this problem:

I noticed that any variables for which the weight is unspecified, are interpreted by ganak as having weight 1 for each literal.
I also noticed that free variables still contribute to the model count, such that for each free variable for which both literals have weight 1, the model count is multiplied with 2.

As far as I can tell, there are 4 free variables in the instance below:

Variable 259 with weight 0.12 is free
Variable 261 with weight 0.45 is free
Variable 263 with weight 0.28 is free
Variable 265 with weight 0.63 is free

Since none of them has weight 1, I'm guessing that maybe they are not the cause of the factor 2 discrepancy with the model count returned by the other solvers, but it must be one of the variables with no specified weight?
I haven't seen this discrepancy in any of the other 50 instances that I generated.

Thanks for reading, and kind regards,
anna

---

The problematic instance: input2.cnf.gz

ERROR: We need to change the hash range (-1)

Hi,
I met some problem when the ganak solved cnf. Can you help me check out?

'''
./ganak chain21_4_mdad.cnf

c Setting the timout to: 100000
c Outputting solution to console
c GANAK version 1.0.0
c ganak GIT revision: GIT-notfound
c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES = | STATICCOMPILE = OFF | ONLY_SIMPLE = | Boost_FOUND = | ZLIB_FOUND = | ENABLE_TESTING = | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = May 10 2021 11:16:22
c Setting the timout to: 100000
c Solving chain21_4_mdad.cnf
c variables (all/used/free): 416/416/0
c clauses (all/long/binary/unit): 1347/977/366/4
c Sampling set not present! So doing total model counting.
c
c Preprocessing ..
c DONE
c variables (all/used/free): 398/398/0
c clauses (all/long/binary/unit): 1272/922/350/0
c Maximum cache size: 9376 MB
c
c We have solved halfed
c We have solved halfed
c We have solved halfed
c We have solved halfed
c We have solved halfed
c Max decision level :25
c Max decision level :50
c Cache full!!
ERROR: We need to change the hash range (-1)
''''

Waiting for your reply. Thanks

Solver segfaulting while running benchmarks

I tried to run your solver on dimacs files of ISCAS85 benchmarks, it segfaulted. Then, I tried on benchmarks in the benchmarks directory. The solver still segfaulted. I believe some change in your code base, left it in some vague state.

Please remove dependence on MIS and instead use B+E

It is perhaps better to just distribute the binary for B+E, and remove dependence on MIS.

Master branch fails to build

Steps to reproduce:

git clone https://github.com/meelgroup/ganak
mkdir ganak/build
cd ganak/build
cmake ..
make

Result:

/tmp/ganak/src/component_types/../clhash/clhash.h:68:63: error: invalid application of 'sizeof' to an incomplete type 'void'
        return clhash(random_data_, (const char *)data, len * sizeof(T));
                                                              ^~~~~~~~~
/tmp/ganak/src/component_types/difference_packed_component.h:254:22: note: in instantiation of function template specialization 'clhasher::operator()<void>' requested here
    clhashkey_[i] = h((void*)data_, sizeof(unsigned)*data_size);

This makes sense, given the clhasher::operator() prototype is

template<typename T>
uint64_t operator()(const T *data, const size_t len) const

and hence T in this case is void.

Disable probabilistic solving in Ganak

Hi,

I was wondering wether it is possible to use Ganak for exact counting as well. If that's the case, how can I configure it that way?

Regards,

Valentin

When timeout set: > 100000 sec, ganak stopped at 100000 sec

Hi, @smsharma1
I changed the timeout from 5000 secs to 1000000 secs ( tout_ganak=1000000) in the run_ganak.sh script.
But ganak stopped again after almost 27 hours( 100000 secs), and the output is:

./run_ganak.sh chain21_4_mdad.cnf
c Trying to run Ganak on chain21_4_mdad.cnf with timeout: 1000000
c Trying to run Ganak on chain21_4_mdad.cnf with timeout: 1000000
c Ganak did NOT work

Before it stopped, the hashrange changed to 2 . In the output file:

c Setting the timout to: 100000
c Outputting solution to console
c GANAK version 1.0.0
c The value of hashrange is 64x2
c ganak GIT revision: 8744032
c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES = | STATICCOMPILE = OFF | ONLY_SIMPLE = | Boost_FOUND = | ZLIB_FOUND = | ENABLE_TESTING = | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = May 11 2021 05:01:09
c Setting the timout to: 100000
c Solving chain21_4_mdad.cnf
c variables (all/used/free): 416/416/0
c clauses (all/long/binary/unit): 1347/977/366/4
c Sampling set not present! So doing total model counting.
c
c Preprocessing ..
c DONE
c variables (all/used/free): 398/398/0
c clauses (all/long/binary/unit): 1272/921/351/0
c Maximum cache size: 2000 MB

It may take several days to find the exact solution number for ganak, and before that what should I do to keep ganak running ?

Can I set a large hashrange before I run ganak? Will it help to shorten the solution time?

Originally posted by @Heawen in #12 (comment)

Bug Report

We observed two kinds of failures in Ganak: 1) crashes and 2) faulty
output for projected model counting. Included below are some example
CNF formulas that illustrate the failures. A more comprehensive suite
of (1) formulas that we generated using our bounded-exhaustive test
input generator that creates CNF files; and (2) CNF files derived from
Alloy models in the standard Alloy distribution
(http://alloy.lcs.mit.edu/alloy/download.html) is available at:
https://github.com/testmodelcounter/testmc
Ganak fails on many of these examples, possibly due to the same
bugs. Some of these CNF files also show failures in other model
counters, which we are separately submitting as bugs reports.

Console Output that shows crash; the formula is unsatisfiable so the
count should be 0 but Ganak produces an assertion failure:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat exampleb.cnf
c ind 1 0
p cnf 1 2
1 0
-1 0
musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py exampleb.cnf
rm: cannot remove 'mis.out': No such file or directory
rm: cannot remove 'mis.timeout': No such file or directory
c Outputting solution to console
c GANAK version 1.0.0
The value of delta is 0.05
The value of hashrange is 64x1
ganak: /home/musman/Desktop/ganak/src/instance.h:215: ClauseIndex Instance::addClause(std::vector<LiteralID>&): Assertion !isUnitClause(literals[0].neg())' failed. The total user time taken by ganak is: 0.0`

================================================================

Console Output that shows incorrect count for projected model counting
-- running the tool as specified in ReadMe; count should be 2, but
Ganak reports 3:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat examplea.cnf
c ind 1 0
p cnf 2 1
1 2 0
musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py examplea.cnf
rm: cannot remove 'mis.out': No such file or directory
rm: cannot remove 'mis.timeout': No such file or directory
c Outputting solution to console
c GANAK version 1.0.0
The value of delta is 0.05
The value of hashrange is 64x1
Solving examplea.cnf
variables (all/used/free): 2/2/0
clauses (all/long/binary/unit): 1/0/1/0
Warning! Sampling set is present but projected model counting is turned off by the user
Sampling set size: 1
Sampling set: 1

Preprocessing ..
DONE
variables (all/used/free): 2/2/0
clauses (all/long/binary/unit): 1/0/1/0
Maximum cache size: 2000 MB

We have solved halfed
We have solved halfed

variables (total / active / free) 2/2/0
clauses (removed) 1 (0)
decisions 1
Max. decision level 1
conflicts 0
conflict clauses (all/bin/unit) 0/0/0

failed literals found by implicit BCP 0
implicit BCP miss rate 0%
bytes cache size 20234600
bytes cache (overall) 20234600
bytes cache components (overall) 192
bytes cache (infra / comps) 20234408/192
bytes pure comp data (curr) 8
bytes pure comp data (overall) 8
bytes cache with sysoverh (curr) 320
bytes cache with sysoverh (overall) 320
cache (lookup / stores / hits) 1/2/0
cache miss rate 100%
avg. variable count (stores / hits) 2/0

# solutions
3
# END

time: 0.001563s

The total user time taken by ganak is: 0.0

================================================================

Console Output that shows incorrect count for projected model counting
-- using the new “-p” option; count should be 2 but Ganak reports 3:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat examplea.cnf
c ind 1 0
p cnf 2 1
1 2 0
musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py -p examplea.cnf
rm: cannot remove 'mis.out': No such file or directory
rm: cannot remove 'mis.timeout': No such file or directory
c Outputting solution to console
c GANAK version 1.0.0
The value of delta is 0.05
The value of hashrange is 64x1
Solving examplea.cnf
variables (all/used/free): 2/2/0
clauses (all/long/binary/unit): 1/0/1/0
Sampling set is present, performing projected model counting
Sampling set size: 1
Sampling set: 1

Preprocessing ..
DONE
variables (all/used/free): 2/2/0
clauses (all/long/binary/unit): 1/0/1/0
Maximum cache size: 2000 MB

We have solved halfed
We have solved halfed

variables (total / active / free) 2/2/0
clauses (removed) 1 (0)
decisions 1
Max. decision level 1
conflicts 0
conflict clauses (all/bin/unit) 0/0/0

failed literals found by implicit BCP 0
implicit BCP miss rate 0%
bytes cache size 20234600
bytes cache (overall) 20234600
bytes cache components (overall) 192
bytes cache (infra / comps) 20234408/192
bytes pure comp data (curr) 8
bytes pure comp data (overall) 8
bytes cache with sysoverh (curr) 320
bytes cache with sysoverh (overall) 320
cache (lookup / stores / hits) 1/2/0
cache miss rate 100%
avg. variable count (stores / hits) 2/0

# solutions
3
# END

time: 0.001452s

The total user time taken by ganak is: 0.0

Reconstruct Ganak Failed

Hello!
I reconstructed Ganak failed.
During the reconstruction process, there is no error in the command before running "cp ganak ../bin/" according to the Readme. But running "cp ganak ../bin/" found the following problems:
(1) running "cp ganak ../bin/" appeared "cp: cannot create regular file '../bin/': Not a directory";
(2 ) running"./run_ganak.sh <myfile.cnf>" fails with "bash: syntax error near unexpected token `newline'".
Please help to check whether the source code of the master is synchronized with the Readme that the reason I guessed the failed. Or is there a more detailed installation commands that I haven't noticed？

Build fails

Hi,
I failed to build this with the following log. Can you check this out?

[ 12%] Linking C static library libclhash.a
[ 12%] Built target clhash
[ 18%] Building CXX object src/component_types/CMakeFiles/component_types.dir/base_packed_component.cpp.o
In file included from /home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.cpp:7:0:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:51:3: warning: identifier ‘nullptr’ is a keyword in C++11 [-Wc++0x-compat]
   T *data_start_ = nullptr;
   ^
In file included from /home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.cpp:7:0:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:51:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   T *data_start_ = nullptr;
                    ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:52:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   T *p = nullptr;
          ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:55:27: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned end_of_bits_ = 0;
                           ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:51:20: error: ‘nullptr’ was not declared in this scope
   T *data_start_ = nullptr;
                    ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:52:10: error: ‘nullptr’ was not declared in this scope
   T *p = nullptr;
          ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:66:25: error: ‘uint64_t’ does not name a type
   void set_hacked(const uint64_t _old_size, const uint64_t _old_num_vars) {
                         ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:66:51: error: ‘uint64_t’ does not name a type
   void set_hacked(const uint64_t _old_size, const uint64_t _old_num_vars) {
                                                   ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:207:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned* data_ = nullptr;
                     ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:209:3: error: ‘uint64_t’ does not name a type
   uint64_t* clhashkey_ = nullptr;
   ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:212:23: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned hashkey_ = 0;
                       ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:216:29: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned creation_time_ = 1;
                             ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:217:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned hack_ = 0;
                    ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:218:23: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned old_size = 0;
                       ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:219:27: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned old_num_vars = 0;
                           ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:225:48: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
   unsigned length_solution_period_and_flags_ = 0;
                                                ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:207:21: error: ‘nullptr’ was not declared in this scope
   unsigned* data_ = nullptr;
                     ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h: In member function ‘void BasePackedComponent::set_hacked(int, int)’:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:70:13: error: ‘nullptr’ was not declared in this scope
     data_ = nullptr;
             ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h: In destructor ‘BasePackedComponent::~BasePackedComponent()’:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:106:9: error: ‘clhashkey_’ was not declared in this scope
     if (clhashkey_){
         ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:107:17: error: type ‘<type error>’ argument given to ‘delete’, expected pointer
       delete [] clhashkey_;
                 ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h: In static member function ‘static void BasePackedComponent::outbit(unsigned int)’:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:111:8: warning: ‘auto’ changes meaning in C++11; please remove it [-Wc++0x-compat]
    for(auto i=0; i<32;i++){
        ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:111:13: error: ‘i’ does not name a type
    for(auto i=0; i<32;i++){
             ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:111:18: error: expected ‘;’ before ‘i’
    for(auto i=0; i<32;i++){
                  ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:111:18: error: ‘i’ was not declared in this scope
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h: In member function ‘void BasePackedComponent::clear()’:
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:192:13: error: ‘nullptr’ was not declared in this scope
     data_ = nullptr;
             ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:193:9: error: ‘clhashkey_’ was not declared in this scope
     if (clhashkey_){
         ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:194:17: error: type ‘<type error>’ argument given to ‘delete’, expected pointer
       delete [] clhashkey_;
                 ^
/home/smkim/Desktop/tools/ganak/src/component_types/base_packed_component.h:196:5: error: ‘clhashkey_’ was not declared in this scope
     clhashkey_ = nullptr;
     ^
src/component_types/CMakeFiles/component_types.dir/build.make:62: recipe for target 'src/component_types/CMakeFiles/component_types.dir/base_packed_component.cpp.o' failed
make[2]: *** [src/component_types/CMakeFiles/component_types.dir/base_packed_component.cpp.o] Error 1
CMakeFiles/Makefile2:185: recipe for target 'src/component_types/CMakeFiles/component_types.dir/all' failed
make[1]: *** [src/component_types/CMakeFiles/component_types.dir/all] Error 2
Makefile:84: recipe for target 'all' failed
make: *** [all] Error 2

Dependence on Header.

Hi Shubham,

Just an observation:

For a toy example

p cnf 2 1 
1 2 0
-1 -2 0

Output of GANAK is:

c # solutions 
s mc 3
c # END

Whereas with the correct header, as expected, output is 2.

Thanks,
Priyanka

WMC ganak fails on the given examples

Hello,

After compiling (edit: on linux) ganak on the wmc branch, for weighted model counting, it fails on the file benchmarks/toy.cnf with the following error message

c Outputting solution to console
c GANAK version 1.0.0
c ganak GIT revision: 66d056ed46bede6a9440b0d75887d2717640c147
c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = OFF | ONLY_SIMPLE =  | Boost_FOUND =  | ZLIB_FOUND =  | ENABLE_TESTING =  | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Oct 18 2022 16:17:37
The sum of positive and negative literal is not equal to 1 for variable 4 pos weight 0.5 neg weight 0.5

Which is strange given that 0.5+0.5 = 1

Sampling set with Sym Ganak

Pardon me if this is an intended behavior, but I was exploring the branch symganak and found that the sampling sets written in a cnf file didn't work as I would expect. More precisely, if a sampling set is written using the notation c ind V1 V2 ... Vn 0, more than 2^n solutions can be returned.

Here is a small example:

p cnf 46 64
c ind 1 2 3 4 5 6 7 8 9 10 0
-6 -39 0
-7 -39 0
-6 -7 40 0
-38 -40 0
-8 -38 39 0
-8 -40 0
-9 38 0
-7 -44 0

Using the solver crytominisat, I obtain a total of 704 solutions, which is the same number indicated by ganak. However, symganak indicates a total of 7971459301376 solutions, which is largely over 2^10.

Since the Readme.md for the symganak branch does not feature information about Projected Model Counting, I expect that this behavior is already known. I'm still writing this issue since symganak clearly reads the sampling set and output informations about it while being executed.