Paul Purdom

The satisfiability (SAT) problem is a core problem in mathematical logic and computing theory. In practice, SAT is fundamental in solving many problems in automated reasoning, computer aided design, computer aided manufacturing, machine vision, database, robotics, integrated circuit design, computer architecture design, and computer network design. Traditional methods treat SAT as a discrete, constrained decision problem. In recent years, many optimization methods, parallel algorithms, and practical techniques have been developed for solving SAT. In this survey, we present a general framework (an algorithm space) that integrates existing SAT algorithms into a unified perspective. We describe sequential and parallel SAT algorithms including variable splitting, resolution, local search, global optimization, mathematical programming, and practical SAT algorithms. We give performance evaluation of some existing SAT algorithms. Finally, we provide a set of practical applications of the satisfiability problems.Descriptors:* MATHEMATICAL LOGIC,* MATHEMATICAL PROGRAMMING, ALGORITHMS, REPRINTS, ROBOTICS, OPTIMIZATION, DECISION MAKING, COMPUTER AIDED DESIGN, EXPERIMENTAL DESIGN, COMPUTER ARCHITECTURE, PARALLEL PROCESSING, SEARCHING, COMPUTER VISION, COMPUTER AIDED MANUFACTURING, COMPUTER NETWORKS.

The average time required for simple search rearrangement backtracking is compared with that for ordinary backtracking when each algorithm is used to find all solutions for random conjunctive normal form predicates. The sets of random predicates are characterized by v: the number of variables, t(v): the number of clauses, and p(v): the probability that a literal appears in clause. For large v if vp(v)<-1n2 both backtracking methods require exponential time if and only if the average number of solutions per problem is exponential. Any backtracking method which finds all solutions to problems has this limitation. For vp(v)>1n 2, there is a difficult region where the average number of solutions per problem is exponentially small, but backtracking requires an exponentially large time. The difficult region for search rearrangement backtracking is only slightly smaller than the difficult region for ordinary backtracking. It is …

A fast algorithm is given to produce a small set of short sentences from a context free grammar such that each production of the grammar is used at least once. The sentences are useful for testing parsing programs and for debugging grammars (finding errors in a grammar which causes it to specify some language other than the one intended). Some experimental results from using the sentences to test some automatically generated simpleLR(1) parsers are also given.

1–1. You should use the polynomial time algorithm because it is faster.(Normally the polynomial algorithm will be better even for moderate values of n, but if the constants associated with the polynomial time algorithm are particularly large and the constants associated with the exponential algorithm are particular small, then the exponential algorithm may be faster for moderate n.) 1.1–2. The time is likely to be too small to measure. Thus if the algorithm needs 20 microseconds and the computer has a clock that ticks each millisecond, it will be difficult or impossible to measure the time. This can sometimes be overcome by putting the straight-line code in a loop and doing it 10,000 times (one needs to compare the time for the loop with no code inside to the time for the loop with the code inside). On time sharing systems, several runs of the same program are likely to lead to different measured times.1.1-3. Hopefully the …

The Davis-Putnam procedure [4] is a powerful method fol* solving the satisfiabiity problem. Satisfiabilitly is NP-complete and the worst-case time of the procedure is exponential 191. In this paper we study the average time. Since the Davis-Putnam procedure is difficult to analyze, we consider simplified versions of it. We show that for certain probability distributions, a version of the procedure which includes the splitting rule and a simplif&! l pure literal rule has polynomial average behavior. The degree of the polynomial is given in terms of a parameter of the assumed distribution. Exclusion of the pure literal rule results in exponential behavior. The Davis-Putnam procedure, which is used to determine whether a conjunctive normal form (CNF) predicate is satisfiable, may be stated as follows.

An algorithm is given for computing the transitive closure of a directed graph in a time no greater thana ₁ N ₁ n+a ₂ n ² for largen wherea ₁ anda ₂ are constants depending on the computer used to execute the algorithm,n is the number of nodes in the graph andN ₁ is the number of arcs (not counting those arcs which are part of a cycle and not counting those arcs which can be removed without changing the transitive closure). For graphs where each arc is selected at random with probabilityp, the average time to compute the transitive closure is no greater than min{a ₁ pn ³+a ₂ n ², 1/2a ₁ n ² p ⁻²+a ₂ n ²} for largen. The algorithm will compute the transitive closure of an undirected graph in a time no greater thana ₂ n ² for largen. The method uses aboutn ²+n bits and 5n words of storage (where each word can holdn+2 values).

Formulas are given for the expected number of nodes in the backtrack tree that is generated while searching for all the solutions of a random predicate. The most general formulas apply to selection from any set of predicates that obeys the following conditions. Each predicate is the conjunction of t terms selected from a set of terms T. For any subset <svg aria-label="T' \leqq T" class="gs_fsvg" height="13px" style="vertical-align:-2px;" width="42px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.55869)"><g><path d="M 94 27 Q 95 32 98 45 T 107 65 T 123 72 Q 299 72 356 82 Q 411 96 422 141 L 702 1266 Q 711 1291 711 1311 Q 711 1327 639 1327 H 520 Q 383 1327 308 1285 T 199 1174 T 109 948 Q 102 930 88 930 H 70 Q 49 930 49 956 L 195 1380 Q 199 1399 215 1399 H 1425 Q 1446 1399 1446 1372 L 1378 948 Q 1378 942 1371 936 T 1358 930 H 1339 Q 1319 930 1319 956 Q 1341 1101 1341 1161 Q 1341 1233 1311 1270 T 1233 1317 T 1108 1327 H 987 Q 932 1327 913 1317 T 881 1257 L 600 133 Q 599 129 598 125 T 596 115 Q 596 89 627 82 Q 680 72 854 72 Q 874 72 874 45 Q 867 16 863 8 T 840 0 H 115 Q 94 0 94 27 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(584.39001, -362.89200)"><path d="M 117 106 Q 98 115 98 131 Q 98 133 100 137 L 375 1059 Q 389 1099 418 1122 T 487 1145 Q 537 1145 574 1111 T 612 1028 Q 612 1002 602 979 L 207 94 Q 204 82 186 82 Q 182 82 178 84 L 117 106 Z " transform="scale(0.34180, -0.34180)"></path></g></g><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 190 915 Q 170 922 170 950 Q 170 977 197 987 L 1366 1540 Q 1370 1542 1380 1542 Q 1398 1542 1409 1531 T 1421 1501 Q 1421 1474 1397 1464 L 307 950 L 1403 432 Q 1421 423 1421 397 Q 1421 380 1409 368 T 1380 356 Q 1370 356 1366 360 L 190 915 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1231.63159, 0.00000)"></path><path d="M 94 27 Q 95 32 98 45 T 107 65 T 123 72 Q 299 72 356 82 Q 411 96 422 141 L 702 1266 Q 711 1291 711 1311 Q 711 1327 639 1327 H 520 Q 383 1327 308 1285 T 199 1174 T 109 948 Q 102 930 88 930 H 70 Q 49 930 49 956 L 195 1380 Q 199 1399 215 1399 H 1425 Q 1446 1399 1446 1372 L 1378 948 Q 1378 942 1371 936 T 1358 930 H 1339 Q 1319 930 1319 956 Q 1341 1101 1341 1161 Q 1341 1233 1311 1270 T 1233 1317 T 1108 1327 H 987 Q 932 1327 913 1317 T 881 1257 L 600 133 Q 599 129 598 125 T 596 115 Q 596 89 627 82 Q 680 72 854 72 Q 874 72 874 45 Q 867 16 863 8 T 840 0 H 115 Q 94 0 94 27 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2287.19019, 0.00000)"></path></g></svg>, the probability that the predicate contains only terms from <svg aria-label="T'" class="gs_fsvg" height="11px" style="vertical-align:0px;" width="13px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.55869)"><g><path d="M 94 27 Q 95 32 98 45 T 107 65 T 123 72 Q 299 72 356 82 Q 411 96 422 141 L 702 1266 Q 711 1291 711 1311 Q 711 1327 639 1327 H 520 Q 383 1327 308 1285 T 199 1174 T 109 948 Q 102 930 88 930 H 70 Q 49 930 49 956 L 195 1380 Q 199 1399 215 1399 H 1425 Q 1446 1399 1446 1372 L 1378 948 Q 1378 942 1371 936 T 1358 930 H 1339 Q 1319 930 1319 956 Q 1341 1101 1341 1161 Q 1341 1233 1311 1270 T 1233 1317 T 1108 1327 H 987 Q 932 1327 913 1317 T 881 1257 L 600 133 Q 599 129 598 125 T 596 115 Q 596 89 627 82 Q 680 72 854 72 Q 874 72 874 45 Q 867 16 863 8 T 840 0 H 115 Q 94 0 94 27 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(584.39001, -362.89200)"><path d="M 117 106 Q 98 115 98 131 Q 98 133 100 137 L 375 1059 Q 389 1099 418 1122 T 487 1145 Q 537 1145 574 1111 T 612 1028 Q 612 1002 602 979 L 207 94 Q 204 82 186 82 Q 182 82 178 84 L 117 106 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg> depends only on the size of <svg aria-label="T'" class="gs_fsvg" height="11px" style="vertical-align:0px;" width="13px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.55869)"><g><path d="M 94 27 Q 95 32 98 45 T 107 65 T 123 72 Q 299 72 356 82 Q 411 96 422 141 L 702 1266 Q 711 1291 711 1311 Q 711 1327 639 1327 H 520 Q 383 1327 308 1285 T 199 1174 T 109 948 Q 102 930 88 930 H 70 Q 49 930 49 956 L 195 1380 Q 199 1399 215 1399 H 1425 Q 1446 1399 1446 1372 L 1378 948 Q 1378 942 1371 936 T 1358 930 H 1339 Q 1319 930 1319 956 Q 1341 1101 1341 1161 Q 1341 1233 1311 1270 T 1233 1317 T 1108 1327 H 987 Q 932 1327 913 1317 T 881 1257 L 600 133 Q 599 129 598 125 T 596 115 Q 596 89 627 82 Q 680 72 854 72 Q 874 72 874 45 Q 867 16 863 8 T 840 0 H 115 Q 94 0 94 27 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(584.39001, -362.89200)"><path d="M 117 106 Q 98 115 98 131 Q 98 133 100 137 L 375 1059 Q 389 1099 418 1122 T 487 1145 Q 537 1145 574 1111 T 612 1028 Q 612 1002 602 979 L 207 94 Q 204 82 186 82 Q 182 82 178 84 L 117 106 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg>. The set T must remain unchanged if each variable <svg aria-label="x_i " class="gs_fsvg" height="8px" style="vertical-align:-2px;" width="13px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 6.18800)"><g><path d="M 160 59 Q 196 31 262 31 Q 326 31 375 92 T 442 227 L 535 590 Q 557 689 557 725 Q 557 776 528 814 T 449 852 Q 384 852 327 811 T 231 708 T 176 582 Q 172 569 160 569 H 135 Q 119 569 119 588 V 594 Q 139 670 187 742 T 304 860 T 453 905 Q 528 905 588 865 T 674 756 Q 709 819 763 862 T 883 905 Q 927 905 973 889 T 1048 842 T 1077 762 Q 1077 710 1043 672 T 958 635 Q 925 635 903 656 T 881 709 Q 881 752 910 784 T 981 823 Q 944 852 879 852 Q 813 852 764 791 T 696 655 L 606 293 Q 584 211 584 158 Q 584 106 613 68 T 692 31 Q 788 31 863 115 T 963 301 Q 967 313 979 313 H 1004 Q 1012 313 1017 307 T 1022 295 Q 1022 293 1020 289 Q 991 167 898 72 T 688 -23 Q 613 -23 552 17 T 467 127 Q 435 67 378 22 T 258 -23 Q 214 -23 167 -8 T 92 40 T 63 121 Q 63 169 96 208 T 180 248 Q 214 248 237 227 T 260 174 Q 260 131 231 99 T 160 59 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(571.56000, 150.00000)"><path d="M 225 154 Q 225 197 240 227 L 412 670 Q 434 729 434 770 Q 434 838 387 838 Q 305 838 249 758 T 168 582 Q 165 563 147 563 H 115 Q 106 563 99 572 T 92 588 V 596 Q 112 672 153 741 T 255 857 T 391 903 Q 444 903 489 882 T 562 821 T 590 729 Q 590 686 575 655 L 403 213 Q 381 164 381 113 Q 381 45 428 45 Q 509 45 565 126 T 645 301 Q 652 319 668 319 H 700 Q 710 319 716 311 T 723 295 Q 723 291 721 287 Q 703 214 662 143 T 559 26 T 424 -20 Q 343 -20 284 27 T 225 154 Z M 463 1241 Q 463 1286 500 1322 T 584 1358 Q 617 1358 641 1334 T 666 1276 Q 666 1230 628 1194 T 545 1159 Q 512 1159 487 1182 T 463 1241 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg> is replaced by <svg aria-label="p_i (x_i )" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="35px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.50000)"><g><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(503.10999, 150.00000)"><path d="M 225 154 Q 225 197 240 227 L 412 670 Q 434 729 434 770 Q 434 838 387 838 Q 305 838 249 758 T 168 582 Q 165 563 147 563 H 115 Q 106 563 99 572 T 92 588 V 596 Q 112 672 153 741 T 255 857 T 391 903 Q 444 903 489 882 T 562 821 T 590 729 Q 590 686 575 655 L 403 213 Q 381 164 381 113 Q 381 45 428 45 Q 509 45 565 126 T 645 301 Q 652 319 668 319 H 700 Q 710 319 716 311 T 723 295 Q 723 291 721 287 Q 703 214 662 143 T 559 26 T 424 -20 Q 343 -20 284 27 T 225 154 Z M 463 1241 Q 463 1286 500 1322 T 584 1358 Q 617 1358 641 1334 T 666 1276 Q 666 1230 628 1194 T 545 1159 Q 512 1159 487 1182 T 463 1241 Z " transform="scale(0.34180, -0.34180)"></path></g></g><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 836.02899, 0.00000)"></path><g transform="translate(1224.91895, 0.00000)"><path d="M 160 59 Q 196 31 262 31 Q 326 31 375 92 T 442 227 L 535 590 Q 557 689 557 725 Q 557 776 528 814 T 449 852 Q 384 852 327 811 T 231 708 T 176 582 Q 172 569 160 569 H 135 Q 119 569 119 588 V 594 Q 139 670 187 742 T 304 860 T 453 905 Q 528 905 588 865 T 674 756 Q 709 819 763 862 T 883 905 Q 927 905 973 889 T 1048 842 T 1077 762 Q 1077 710 1043 672 T 958 635 Q 925 635 903 656 T 881 709 Q 881 752 910 784 T 981 823 Q 944 852 879 852 Q 813 852 764 791 T 696 655 L 606 293 Q 584 211 584 158 Q 584 106 613 68 T 692 31 Q 788 31 863 115 T 963 301 Q 967 313 979 313 H 1004 Q 1012 313 1017 307 T 1022 295 Q 1022 293 1020 289 Q 991 167 898 72 T 688 -23 Q 613 -23 552 17 T 467 127 Q 435 67 378 22 T 258 -23 Q 214 -23 167 -8 T 92 40 T 63 121 Q 63 169 96 208 T 180 248 Q 214 248 237 227 T 260 174 Q 260 131 231 99 T 160 59 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(571.56000, 150.00000)"><path d="M 225 154 Q 225 197 240 227 L 412 670 Q 434 729 434 770 Q 434 838 387 838 Q 305 838 249 758 T 168 582 Q 165 563 147 563 H 115 Q 106 563 99 572 T 92 588 V 596 Q 112 672 153 741 T 255 857 T 391 903 Q 444 903 489 882 T 562 821 T 590 729 Q 590 686 575 655 L 403 213 Q 381 164 381 113 Q 381 45 428 45 Q 509 45 565 126 T 645 301 Q 652 319 668 319 H 700 Q 710 319 716 311 T 723 295 Q 723 291 721 287 Q 703 214 662 143 T 559 26 T 424 -20 Q 343 -20 284 27 T 225 154 Z M 463 1241 Q 463 1286 500 1322 T 584 1358 Q 617 1358 641 1334 T 666 1276 Q 666 1230 628 1194 T 545 1159 Q 512 1159 487 1182 T 463 1241 Z " transform="scale(0.34180, -0.34180)"></path></g></g><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2129.39795, 0.00000)"></path></g></svg>, where <svg aria-label="p_i " class="gs_fsvg" height="9px" style="vertical-align:-3px;" width="12px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 6.18800)"><g><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(503.10999, 150.00000)"><path d="M 225 154 Q 225 197 240 227 L 412 670 Q 434 729 434 770 Q 434 838 387 838 Q 305 838 249 758 T 168 582 Q 165 563 147 563 H 115 Q 106 563 99 572 T 92 588 V 596 Q 112 672 153 741 T 255 857 T 391 903 Q 444 903 489 882 T 562 821 T 590 729 Q 590 686 575 655 L 403 213 Q 381 164 381 113 Q 381 45 428 45 Q 509 45 565 126 T 645 301 Q 652 319 668 319 H 700 Q 710 319 716 311 T 723 295 Q 723 291 721 287 Q 703 214 662 143 T 559 26 T 424 -20 Q 343 -20 284 27 T 225 154 Z M 463 1241 Q 463 1286 500 1322 T 584 1358 Q 617 1358 641 1334 T 666 1276 Q 666 1230 628 1194 T 545 1159 Q 512 1159 487 1182 T 463 1241 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg> is a permutation function. The time needed to evaluate the general formulas is proportional to v, the number of variables in the predicate. More detailed consideration is given to predicates whose terms are random disjunctive clauses with s literals, <svg aria-label="t = v^\alpha " class="gs_fsvg" height="10px" style="vertical-align:0px;" width="38px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 9.40229)"><path d="M 127 166 Q 127 196 133 223 L 281 811 H 66 Q 45 811 45 838 Q 53 883 72 883 H 299 L 381 1217 Q 389 1244 413 1263 T 467 1282 Q 493 1282 510 1266 T 528 1225 Q 528 1219 527 1215 T 526 1208 L 444 883 H 655 Q 676 883 676 856 Q 675 851 672 839 T 664 819 T 649 811 H 426 L 279 219 Q 264 161 264 119 Q 264 31 324 31 Q 414 31 483 115 T 590 301 Q 598 313 606 313 H 631 Q 639 313 644 307 T 649 295 Q 649 291 647 289 Q 602 165 516 71 T 319 -23 Q 238 -23 182 30 T 127 166 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 154 272 Q 137 272 126 285 T 115 313 Q 115 330 126 342 T 154 354 H 1440 Q 1455 354 1466 342 T 1477 313 Q 1477 298 1466 285 T 1440 272 H 154 Z M 154 670 Q 137 670 126 682 T 115 711 Q 115 726 126 739 T 154 752 H 1440 Q 1455 752 1466 739 T 1477 711 Q 1477 694 1466 682 T 1440 670 H 154 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 638.88855, 0.00000)"></path><g transform="translate(1694.44714, 0.00000)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 123 338 Q 123 483 210 614 T 435 824 T 717 903 Q 800 903 872 874 T 999 792 T 1083 668 T 1114 514 L 1118 399 Q 1255 578 1307 788 Q 1311 805 1327 805 H 1360 Q 1371 805 1376 798 T 1382 780 V 774 Q 1359 684 1322 601 T 1236 441 T 1124 293 Q 1124 245 1128 193 T 1148 93 T 1194 45 Q 1235 45 1259 64 T 1301 115 T 1329 147 H 1362 Q 1371 147 1377 140 T 1384 123 Q 1384 85 1352 52 T 1273 0 T 1190 -20 Q 1110 -20 1054 27 T 973 154 Q 867 72 746 26 T 498 -20 Q 394 -20 308 25 T 172 151 T 123 338 Z M 504 45 Q 624 45 741 94 T 956 227 Q 956 239 955 246 T 954 262 L 944 477 Q 944 559 922 642 T 848 781 T 713 838 Q 616 838 538 784 T 408 642 T 328 453 T 301 264 Q 301 170 356 107 T 504 45 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 484.72000, -362.89200)"></path></g></g></svg> for some <svg aria-label="1 &lt; \alpha &lt; s" class="gs_fsvg" height="10px" style="vertical-align:-1px;" width="60px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 9.32400)"><path d="M 190 0 V 72 Q 446 72 446 137 V 1212 Q 340 1161 178 1161 V 1233 Q 429 1233 557 1364 H 586 Q 593 1364 599 1358 T 606 1346 V 137 Q 606 72 862 72 V 0 H 190 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 190 477 Q 170 486 170 512 Q 170 538 197 551 L 1366 1102 Q 1374 1106 1380 1106 Q 1398 1106 1409 1093 T 1421 1065 Q 1421 1040 1397 1026 L 307 512 L 1403 -6 Q 1421 -12 1421 -41 Q 1421 -57 1409 -70 T 1380 -82 Q 1374 -82 1366 -78 L 190 477 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 777.77856, 0.00000)"></path><path d="M 412 -23 Q 315 -23 239 23 T 123 147 T 82 324 Q 82 463 159 599 T 365 820 T 635 905 Q 739 905 818 850 T 938 705 T 979 512 L 981 375 Q 1051 472 1099 576 T 1174 793 Q 1178 805 1190 805 H 1214 Q 1233 805 1233 786 Q 1233 784 1231 780 Q 1207 686 1171 599 T 1086 432 T 981 285 Q 981 31 1040 31 Q 1078 31 1102 53 T 1145 109 T 1169 143 H 1194 Q 1210 143 1210 123 Q 1210 72 1151 24 T 1036 -23 Q 962 -23 913 25 T 846 150 Q 750 68 638 22 T 412 -23 Z M 416 31 Q 635 31 836 211 Q 835 223 833 240 T 831 260 V 481 Q 831 852 631 852 Q 511 852 421 749 T 285 504 T 240 244 Q 240 155 285 93 T 416 31 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1833.33716, 0.00000)"></path><path d="M 190 477 Q 170 486 170 512 Q 170 538 197 551 L 1366 1102 Q 1374 1106 1380 1106 Q 1398 1106 1409 1093 T 1421 1065 Q 1421 1040 1397 1026 L 307 512 L 1403 -6 Q 1421 -12 1421 -41 Q 1421 -57 1409 -70 T 1380 -82 Q 1374 -82 1366 -78 L 190 477 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2754.53760, 0.00000)"></path><path d="M 178 125 Q 233 31 399 31 Q 471 31 536 55 T 643 129 T 686 248 Q 686 301 648 335 T 555 381 L 444 403 Q 368 422 319 474 T 270 600 Q 270 691 319 761 T 450 868 T 618 905 Q 711 905 784 860 T 858 729 Q 858 682 831 646 T 758 610 Q 731 610 711 627 T 692 672 Q 692 696 705 718 T 741 754 T 788 768 Q 770 812 720 832 T 614 852 Q 562 852 510 831 T 426 769 T 395 674 Q 395 637 421 609 T 485 569 L 604 545 Q 661 533 708 502 T 783 425 T 811 319 Q 811 243 768 169 T 664 51 Q 555 -23 397 -23 Q 288 -23 197 27 T 106 176 Q 106 232 138 273 T 227 315 Q 260 315 282 295 T 305 242 Q 305 195 270 160 T 188 125 H 178 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 3810.09619, 0.00000)"></path></g></svg>, and the random selections are done with repetition. For this case the expected number of nodes is <svg aria-label="\exp [O(v^{(s - \alpha )/(s - 1)} )]" class="gs_fsvg" height="16px" style="vertical-align:-4px;" width="122px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 12.43049)"><g><path d="M 510 -23 Q 385 -23 280 42 T 116 217 T 57 449 Q 57 569 111 677 T 263 851 T 481 918 Q 575 918 644 886 T 759 799 T 827 667 T 850 500 Q 850 473 829 473 H 236 V 451 Q 236 281 304 159 T 528 37 Q 591 37 644 65 T 737 143 T 791 250 Q 793 257 798 262 T 811 268 H 829 Q 850 268 850 242 Q 821 126 725 51 T 510 -23 Z M 238 524 H 705 Q 705 601 683 680 T 612 811 T 481 864 Q 365 864 301 755 T 238 524 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 25 0 V 72 Q 103 72 172 102 T 289 193 L 475 430 L 233 745 Q 197 790 154 800 T 35 811 V 883 H 461 V 811 Q 434 811 410 799 T 387 764 Q 387 756 393 745 L 557 532 L 680 690 Q 705 720 705 750 Q 705 775 688 793 T 645 811 V 883 H 1022 V 811 Q 943 811 873 780 T 756 690 L 594 483 L 856 137 Q 895 92 937 82 T 1057 72 V 0 H 631 V 72 Q 656 72 679 84 T 702 119 Q 702 128 696 137 L 512 381 L 365 193 Q 342 167 342 133 Q 342 108 359 90 T 399 72 V 0 H 25 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 444.44000, 0.00000)"></path><path d="M 53 -397 V -326 Q 123 -326 168 -314 T 213 -260 V 727 Q 213 783 173 797 T 53 811 V 883 L 356 905 V 778 Q 412 840 486 872 T 645 905 Q 766 905 863 839 T 1014 667 T 1069 442 Q 1069 318 1008 211 T 843 40 T 614 -23 Q 465 -23 362 98 V -260 Q 362 -302 407 -314 T 522 -326 V -397 H 53 Z M 362 199 Q 398 126 462 78 T 602 31 Q 673 31 727 69 T 819 171 T 873 305 T 891 442 Q 891 524 861 619 T 771 780 T 625 846 Q 542 846 472 803 T 362 688 V 199 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 972.22003, 0.00000)"></path></g><path d="M 242 -512 V 1536 H 522 V 1454 H 324 V -430 H 522 V -512 H 242 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1527.78003, 0.00000)"></path><path d="M 623 -45 Q 469 -45 350 25 T 166 221 T 102 500 Q 102 723 228 944 T 562 1304 T 995 1444 Q 1112 1444 1209 1402 T 1373 1285 T 1476 1111 T 1513 893 Q 1513 724 1441 556 T 1241 251 T 955 34 T 623 -45 Z M 639 16 Q 788 16 917 110 T 1137 354 T 1276 668 T 1325 975 Q 1325 1086 1287 1178 T 1170 1327 T 981 1384 Q 873 1384 771 1332 T 586 1194 Q 501 1107 435 978 T 335 708 T 301 442 Q 301 268 386 142 T 639 16 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1805.56006, 0.00000)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2596.11914, 0.00000)"></path><g transform="translate(2985.00928, 0.00000)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(484.72000, -362.89200)"><path d="M 715 -512 Q 554 -395 445 -233 T 284 119 T 231 512 Q 231 662 260 807 T 350 1084 T 501 1330 T 715 1534 Q 718 1535 720 1535 T 725 1536 H 745 Q 755 1536 761 1529 T 768 1511 Q 768 1498 760 1493 Q 658 1405 584 1292 T 465 1051 T 400 788 T 379 512 Q 379 219 469 -41 T 760 -471 Q 768 -476 768 -489 Q 768 -500 761 -507 T 745 -514 H 725 Q 723 -513 720 -513 T 715 -512 Z " transform="scale(0.34180, -0.34180)"></path><path d="M 244 123 Q 300 45 477 45 Q 544 45 615 65 T 734 131 T 782 248 Q 782 299 738 330 T 637 373 L 504 397 Q 425 413 370 468 T 315 598 Q 315 693 369 762 T 511 867 T 692 903 Q 752 903 815 885 T 919 828 T 961 727 Q 961 678 933 641 T 858 604 Q 829 604 807 623 T 786 672 Q 786 707 810 735 T 868 770 Q 822 838 688 838 Q 601 838 528 796 T 455 672 Q 455 597 561 573 L 696 549 Q 788 531 855 470 T 922 319 Q 922 242 876 168 T 762 51 Q 647 -20 475 -20 Q 350 -20 247 25 T 145 178 Q 145 235 179 277 T 270 319 Q 305 319 328 298 T 352 242 Q 352 196 321 162 T 244 123 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 312.50800, 0.00000)"></path><path d="M 268 461 Q 248 464 234 477 T 221 512 Q 221 554 268 561 H 1559 Q 1606 554 1606 512 Q 1606 491 1592 477 T 1559 461 H 268 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 689.92700, 0.00000)"></path><path d="M 123 338 Q 123 483 210 614 T 435 824 T 717 903 Q 800 903 872 874 T 999 792 T 1083 668 T 1114 514 L 1118 399 Q 1255 578 1307 788 Q 1311 805 1327 805 H 1360 Q 1371 805 1376 798 T 1382 780 V 774 Q 1359 684 1322 601 T 1236 441 T 1124 293 Q 1124 245 1128 193 T 1148 93 T 1194 45 Q 1235 45 1259 64 T 1301 115 T 1329 147 H 1362 Q 1371 147 1377 140 T 1384 123 Q 1384 85 1352 52 T 1273 0 T 1190 -20 Q 1110 -20 1054 27 T 973 154 Q 867 72 746 26 T 498 -20 Q 394 -20 308 25 T 172 151 T 123 338 Z M 504 45 Q 624 45 741 94 T 956 227 Q 956 239 955 246 T 954 262 L 944 477 Q 944 559 922 642 T 848 781 T 713 838 Q 616 838 538 784 T 408 642 T 328 453 T 301 264 Q 301 170 356 107 T 504 45 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 1314.90796, 0.00000)"></path><path d="M 166 -514 Q 156 -514 149 -507 T 143 -489 Q 143 -476 152 -471 Q 256 -382 329 -268 T 446 -28 T 511 236 T 532 512 Q 532 652 511 788 T 446 1052 T 327 1293 T 152 1493 Q 143 1498 143 1511 Q 143 1521 149 1528 T 166 1536 H 186 Q 189 1536 191 1535 T 197 1534 Q 356 1417 465 1255 T 627 904 T 680 512 Q 680 307 627 117 T 464 -234 T 197 -512 Q 194 -512 191 -513 T 186 -514 H 166 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 1834.77686, 0.00000)"></path><path d="M 143 -463 Q 143 -458 147 -444 L 924 1505 Q 940 1536 971 1536 Q 990 1536 1005 1521 T 1020 1487 Q 1020 1480 1019 1476 T 1018 1468 L 242 -481 Q 221 -512 195 -512 Q 175 -512 159 -497 T 143 -463 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 2147.28491, 0.00000)"></path><path d="M 715 -512 Q 554 -395 445 -233 T 284 119 T 231 512 Q 231 662 260 807 T 350 1084 T 501 1330 T 715 1534 Q 718 1535 720 1535 T 725 1536 H 745 Q 755 1536 761 1529 T 768 1511 Q 768 1498 760 1493 Q 658 1405 584 1292 T 465 1051 T 400 788 T 379 512 Q 379 219 469 -41 T 760 -471 Q 768 -476 768 -489 Q 768 -500 761 -507 T 745 -514 H 725 Q 723 -513 720 -513 T 715 -512 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 2545.89282, 0.00000)"></path><path d="M 244 123 Q 300 45 477 45 Q 544 45 615 65 T 734 131 T 782 248 Q 782 299 738 330 T 637 373 L 504 397 Q 425 413 370 468 T 315 598 Q 315 693 369 762 T 511 867 T 692 903 Q 752 903 815 885 T 919 828 T 961 727 Q 961 678 933 641 T 858 604 Q 829 604 807 623 T 786 672 Q 786 707 810 735 T 868 770 Q 822 838 688 838 Q 601 838 528 796 T 455 672 Q 455 597 561 573 L 696 549 Q 788 531 855 470 T 922 319 Q 922 242 876 168 T 762 51 Q 647 -20 475 -20 Q 350 -20 247 25 T 145 178 Q 145 235 179 277 T 270 319 Q 305 319 328 298 T 352 242 Q 352 196 321 162 T 244 123 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 2858.40088, 0.00000)"></path><path d="M 268 461 Q 248 464 234 477 T 221 512 Q 221 554 268 561 H 1559 Q 1606 554 1606 512 Q 1606 491 1592 477 T 1559 461 H 268 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 3235.81982, 0.00000)"></path><path d="M 233 0 V 82 Q 516 82 516 143 V 1202 Q 401 1147 219 1147 V 1229 Q 341 1229 447 1258 T 629 1360 H 666 Q 685 1355 690 1335 V 143 Q 690 82 973 82 V 0 H 233 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 3860.80078, 0.00000)"></path><path d="M 166 -514 Q 156 -514 149 -507 T 143 -489 Q 143 -476 152 -471 Q 256 -382 329 -268 T 446 -28 T 511 236 T 532 512 Q 532 652 511 788 T 446 1052 T 327 1293 T 152 1493 Q 143 1498 143 1511 Q 143 1521 149 1528 T 166 1536 H 186 Q 189 1536 191 1535 T 197 1534 Q 356 1417 465 1255 T 627 904 T 680 512 Q 680 307 627 117 T 464 -234 T 197 -512 Q 194 -512 191 -513 T 186 -514 H 166 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 4259.40869, 0.00000)"></path></g></g><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 8041.64600, 0.00000)"></path><path d="M 45 -512 V -430 H 244 V 1454 H 45 V 1536 H 326 V -512 H 45 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 8430.53613, 0.00000)"></path></g></svg> …

Methods from computational group theory are used to improve the speed of backtrack searching on problems with symmetry. The symmetry testing algorithm, which is similar to a color automorphism algorithm, takes the symmetry group as input and uses it to avoid searching equivalent portions of the search space. The algorithm permits dynamic search rearrangement in conjunction with symmetry testing. Experimental results confirm that the algorithm saves a considerable amount of time on some search problems.

For a simple parameterized model of conjunctive normal form predicates, we show that a simplified version of the Davis–Putnam procedure can, for many values of the parameters, solve the satisfiability problem in polynomial average time. Let v be the number of variables, <svg aria-label="t(v)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="23px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.50000)"><path d="M 127 166 Q 127 196 133 223 L 281 811 H 66 Q 45 811 45 838 Q 53 883 72 883 H 299 L 381 1217 Q 389 1244 413 1263 T 467 1282 Q 493 1282 510 1266 T 528 1225 Q 528 1219 527 1215 T 526 1208 L 444 883 H 655 Q 676 883 676 856 Q 675 851 672 839 T 664 819 T 649 811 H 426 L 279 219 Q 264 161 264 119 Q 264 31 324 31 Q 414 31 483 115 T 590 301 Q 598 313 606 313 H 631 Q 639 313 644 307 T 649 295 Q 649 291 647 289 Q 602 165 516 71 T 319 -23 Q 238 -23 182 30 T 127 166 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 361.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 750.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1270.59900, 0.00000)"></path></g></svg> the number of clauses in a predicate, and <svg aria-label="p(v)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="25px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.50000)"><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 503.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 892.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1412.59900, 0.00000)"></path></g></svg> the probability that a given literal appears in a clause (<svg aria-label="p(v)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="25px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.50000)"><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 503.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 892.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1412.59900, 0.00000)"></path></g></svg> is the same for all literals). Let <svg aria-label="\varepsilon " class="gs_fsvg" height="7px" style="vertical-align:0px;" width="7px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 6.34200)"><path d="M 55 213 Q 55 269 79 322 T 143 417 T 236 492 Q 158 546 158 631 Q 158 722 234 790 T 420 893 T 618 928 Q 655 928 717 911 T 827 868 T 874 809 Q 874 785 855 766 T 815 748 Q 806 748 769 769 T 692 808 T 602 825 Q 528 825 439 807 T 284 746 T 217 633 Q 217 566 293 520 Q 379 559 469 559 Q 629 559 629 502 Q 629 457 574 444 T 449 432 Q 353 432 291 461 Q 223 425 170 360 T 117 225 Q 117 159 161 122 T 271 71 T 401 57 Q 514 57 601 81 T 727 184 Q 733 197 750 197 Q 772 190 772 170 Q 772 168 766 150 Q 733 85 672 41 T 537 -24 T 385 -45 Q 258 -45 156 23 T 55 213 Z M 371 492 Q 407 485 453 485 Q 543 485 565 498 Q 537 506 467 506 Q 416 506 371 492 Z " transform="scale(0.48828, -0.48828)"></path></g></svg> be any small positive constant and n any large positive integer. Then a version of the Davis–Putnam procedure that uses only backtracking and the pure literal rule uses average time that is polynomial in the problem size when any of the following conditions are true for large v. (1) <svg aria-label="t(v) \leqq n\ln v" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="74px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.54200)"><path d="M 127 166 Q 127 196 133 223 L 281 811 H 66 Q 45 811 45 838 Q 53 883 72 883 H 299 L 381 1217 Q 389 1244 413 1263 T 467 1282 Q 493 1282 510 1266 T 528 1225 Q 528 1219 527 1215 T 526 1208 L 444 883 H 655 Q 676 883 676 856 Q 675 851 672 839 T 664 819 T 649 811 H 426 L 279 219 Q 264 161 264 119 Q 264 31 324 31 Q 414 31 483 115 T 590 301 Q 598 313 606 313 H 631 Q 639 313 644 307 T 649 295 Q 649 291 647 289 Q 602 165 516 71 T 319 -23 Q 238 -23 182 30 T 127 166 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 361.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 750.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1270.59900, 0.00000)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 190 915 Q 170 922 170 950 Q 170 977 197 987 L 1366 1540 Q 1370 1542 1380 1542 Q 1398 1542 1409 1531 T 1421 1501 Q 1421 1474 1397 1464 L 307 950 L 1403 432 Q 1421 423 1421 397 Q 1421 380 1409 368 T 1380 356 Q 1370 356 1366 360 L 190 915 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1937.26758, 0.00000)"></path><path d="M 158 35 Q 158 47 160 53 L 313 664 Q 328 721 328 764 Q 328 852 268 852 Q 204 852 173 775 T 113 582 Q 113 576 107 572 T 96 569 H 72 Q 65 569 60 576 T 55 590 Q 77 679 97 741 T 161 854 T 270 905 Q 347 905 406 856 T 465 733 Q 526 813 608 859 T 782 905 Q 855 905 908 880 T 990 804 T 1020 684 Q 1020 600 982 481 T 889 215 Q 860 148 860 92 Q 860 31 907 31 Q 987 31 1040 117 T 1116 301 Q 1120 313 1133 313 H 1157 Q 1165 313 1170 308 T 1176 295 Q 1176 293 1174 289 Q 1146 173 1076 75 T 903 -23 Q 831 -23 780 26 T 729 147 Q 729 185 745 227 Q 771 294 804 387 T 859 565 T 881 715 Q 881 772 857 812 T 778 852 Q 703 852 640 819 T 530 731 T 444 602 L 305 45 Q 298 17 273 -3 T 219 -23 Q 194 -23 176 -7 T 158 35 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2992.82617, 0.00000)"></path><g transform="translate(3759.71338, 0.00000)"><path d="M 63 0 V 72 Q 133 72 178 83 T 223 137 V 1212 Q 223 1267 206 1291 T 159 1321 T 63 1327 V 1399 L 367 1421 V 137 Q 367 94 412 83 T 526 72 V 0 H 63 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 61 0 V 72 Q 131 72 176 83 T 221 137 V 696 Q 221 751 204 775 T 157 805 T 61 811 V 883 L 358 905 V 705 Q 399 793 479 849 T 655 905 Q 797 905 868 837 T 940 629 V 137 Q 940 94 985 83 T 1100 72 V 0 H 631 V 72 Q 701 72 746 83 T 791 137 V 623 Q 791 723 762 787 T 643 852 Q 524 852 447 757 T 371 541 V 137 Q 371 94 416 83 T 530 72 V 0 H 61 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 277.78000, 0.00000)"></path></g><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 4759.72021, 0.00000)"></path></g></svg>; (2) <svg aria-label="t(v) \geqq \exp (\varepsilon v)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="88px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.54200)"><path d="M 127 166 Q 127 196 133 223 L 281 811 H 66 Q 45 811 45 838 Q 53 883 72 883 H 299 L 381 1217 Q 389 1244 413 1263 T 467 1282 Q 493 1282 510 1266 T 528 1225 Q 528 1219 527 1215 T 526 1208 L 444 883 H 655 Q 676 883 676 856 Q 675 851 672 839 T 664 819 T 649 811 H 426 L 279 219 Q 264 161 264 119 Q 264 31 324 31 Q 414 31 483 115 T 590 301 Q 598 313 606 313 H 631 Q 639 313 644 307 T 649 295 Q 649 291 647 289 Q 602 165 516 71 T 319 -23 Q 238 -23 182 30 T 127 166 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 361.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 750.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1270.59900, 0.00000)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 170 397 Q 170 423 197 436 L 1284 950 L 190 1466 Q 170 1476 170 1501 Q 170 1518 181 1530 T 211 1542 Q 221 1542 227 1540 L 1403 985 Q 1421 976 1421 950 Q 1421 926 1397 911 L 227 360 Q 221 356 211 356 Q 194 356 182 369 T 170 397 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1937.26758, 0.00000)"></path><g transform="translate(2992.82617, 0.00000)"><path d="M 510 -23 Q 385 -23 280 42 T 116 217 T 57 449 Q 57 569 111 677 T 263 851 T 481 918 Q 575 918 644 886 T 759 799 T 827 667 T 850 500 Q 850 473 829 473 H 236 V 451 Q 236 281 304 159 T 528 37 Q 591 37 644 65 T 737 143 T 791 250 Q 793 257 798 262 T 811 268 H 829 Q 850 268 850 242 Q 821 126 725 51 T 510 -23 Z M 238 524 H 705 Q 705 601 683 680 T 612 811 T 481 864 Q 365 864 301 755 T 238 524 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 25 0 V 72 Q 103 72 172 102 T 289 193 L 475 430 L 233 745 Q 197 790 154 800 T 35 811 V 883 H 461 V 811 Q 434 811 410 799 T 387 764 Q 387 756 393 745 L 557 532 L 680 690 Q 705 720 705 750 Q 705 775 688 793 T 645 811 V 883 H 1022 V 811 Q 943 811 873 780 T 756 690 L 594 483 L 856 137 Q 895 92 937 82 T 1057 72 V 0 H 631 V 72 Q 656 72 679 84 T 702 119 Q 702 128 696 137 L 512 381 L 365 193 Q 342 167 342 133 Q 342 108 359 90 T 399 72 V 0 H 25 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 444.44000, 0.00000)"></path><path d="M 53 -397 V -326 Q 123 -326 168 -314 T 213 -260 V 727 Q 213 783 173 797 T 53 811 V 883 L 356 905 V 778 Q 412 840 486 872 T 645 905 Q 766 905 863 839 T 1014 667 T 1069 442 Q 1069 318 1008 211 T 843 40 T 614 -23 Q 465 -23 362 98 V -260 Q 362 -302 407 -314 T 522 -326 V -397 H 53 Z M 362 199 Q 398 126 462 78 T 602 31 Q 673 31 727 69 T 819 171 T 873 305 T 891 442 Q 891 524 861 619 T 771 780 T 625 846 Q 542 846 472 803 T 362 688 V 199 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 972.22003, 0.00000)"></path></g><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 4520.60645, 0.00000)"></path><path d="M 55 213 Q 55 269 79 322 T 143 417 T 236 492 Q 158 546 158 631 Q 158 722 234 790 T 420 893 T 618 928 Q 655 928 717 911 T 827 868 T 874 809 Q 874 785 855 766 T 815 748 Q 806 748 769 769 T 692 808 T 602 825 Q 528 825 439 807 T 284 746 T 217 633 Q 217 566 293 520 Q 379 559 469 559 Q 629 559 629 502 Q 629 457 574 444 T 449 432 Q 353 432 291 461 Q 223 425 170 360 T 117 225 Q 117 159 161 122 T 271 71 T 401 57 Q 514 57 601 81 T 727 184 Q 733 197 750 197 Q 772 190 772 170 Q 772 168 766 150 Q 733 85 672 41 T 537 -24 T 385 -45 Q 258 -45 156 23 T 55 213 Z M 371 492 Q 407 485 453 485 Q 543 485 565 498 Q 537 506 467 506 Q 416 506 371 492 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 4909.49658, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 5375.82666, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 5896.42578, 0.00000)"></path></g></svg>; (3) <svg aria-label="p(v) \geqq \varepsilon " class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="50px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.54200)"><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 503.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 892.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1412.59900, 0.00000)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 170 397 Q 170 423 197 436 L 1284 950 L 190 1466 Q 170 1476 170 1501 Q 170 1518 181 1530 T 211 1542 Q 221 1542 227 1540 L 1403 985 Q 1421 976 1421 950 Q 1421 926 1397 911 L 227 360 Q 221 356 211 356 Q 194 356 182 369 T 170 397 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2079.26758, 0.00000)"></path><path d="M 55 213 Q 55 269 79 322 T 143 417 T 236 492 Q 158 546 158 631 Q 158 722 234 790 T 420 893 T 618 928 Q 655 928 717 911 T 827 868 T 874 809 Q 874 785 855 766 T 815 748 Q 806 748 769 769 T 692 808 T 602 825 Q 528 825 439 807 T 284 746 T 217 633 Q 217 566 293 520 Q 379 559 469 559 Q 629 559 629 502 Q 629 457 574 444 T 449 432 Q 353 432 291 461 Q 223 425 170 360 T 117 225 Q 117 159 161 122 T 271 71 T 401 57 Q 514 57 601 81 T 727 184 Q 733 197 750 197 Q 772 190 772 170 Q 772 168 766 150 Q 733 85 672 41 T 537 -24 T 385 -45 Q 258 -45 156 23 T 55 213 Z M 371 492 Q 407 485 453 485 Q 543 485 565 498 Q 537 506 467 506 Q 416 506 371 492 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 3134.82617, 0.00000)"></path></g></svg>; or (4) <svg aria-label="p(v) \leqq n (\ln v/ v)^{3/2} " class="gs_fsvg" height="16px" style="vertical-align:-4px;" width="115px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 12.43049)"><path d="M -51 -397 Q -70 -397 -70 -371 Q -63 -326 -43 -326 Q 21 -326 46 -315 T 86 -256 L 317 666 Q 332 704 332 764 Q 332 852 272 852 Q 208 852 177 775 T 117 582 Q 117 569 100 569 H 76 Q 71 569 65 576 T 59 590 Q 81 679 101 741 T 165 854 T 274 905 Q 344 905 397 865 T 465 758 Q 521 823 589 864 T 729 905 Q 815 905 878 859 T 974 738 T 1006 578 Q 1006 446 938 305 T 755 70 T 508 -23 Q 448 -23 399 11 T 324 100 L 231 -264 Q 226 -294 225 -299 Q 225 -326 360 -326 Q 381 -326 381 -352 Q 374 -379 369 -388 T 346 -397 H -51 Z M 510 31 Q 581 31 642 89 T 741 221 Q 769 276 793 355 T 836 525 T 854 668 Q 854 715 841 756 T 800 824 T 725 852 Q 650 852 583 798 T 463 666 V 659 L 350 207 Q 364 134 404 82 T 510 31 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 503.10999, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 892.00000, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1412.59900, 0.00000)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 190 915 Q 170 922 170 950 Q 170 977 197 987 L 1366 1540 Q 1370 1542 1380 1542 Q 1398 1542 1409 1531 T 1421 1501 Q 1421 1474 1397 1464 L 307 950 L 1403 432 Q 1421 423 1421 397 Q 1421 380 1409 368 T 1380 356 Q 1370 356 1366 360 L 190 915 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2079.26758, 0.00000)"></path><path d="M 158 35 Q 158 47 160 53 L 313 664 Q 328 721 328 764 Q 328 852 268 852 Q 204 852 173 775 T 113 582 Q 113 576 107 572 T 96 569 H 72 Q 65 569 60 576 T 55 590 Q 77 679 97 741 T 161 854 T 270 905 Q 347 905 406 856 T 465 733 Q 526 813 608 859 T 782 905 Q 855 905 908 880 T 990 804 T 1020 684 Q 1020 600 982 481 T 889 215 Q 860 148 860 92 Q 860 31 907 31 Q 987 31 1040 117 T 1116 301 Q 1120 313 1133 313 H 1157 Q 1165 313 1170 308 T 1176 295 Q 1176 293 1174 289 Q 1146 173 1076 75 T 903 -23 Q 831 -23 780 26 T 729 147 Q 729 185 745 227 Q 771 294 804 387 T 859 565 T 881 715 Q 881 772 857 812 T 778 852 Q 703 852 640 819 T 530 731 T 444 602 L 305 45 Q 298 17 273 -3 T 219 -23 Q 194 -23 176 -7 T 158 35 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 3134.82617, 0.00000)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 3735.04614, 0.00000)"></path><g transform="translate(4123.93604, 0.00000)"><path d="M 63 0 V 72 Q 133 72 178 83 T 223 137 V 1212 Q 223 1267 206 1291 T 159 1321 T 63 1327 V 1399 L 367 1421 V 137 Q 367 94 412 83 T 526 72 V 0 H 63 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 61 0 V 72 Q 131 72 176 83 T 221 137 V 696 Q 221 751 204 775 T 157 805 T 61 811 V 883 L 358 905 V 705 Q 399 793 479 849 T 655 905 Q 797 905 868 837 T 940 629 V 137 Q 940 94 985 83 T 1100 72 V 0 H 631 V 72 Q 701 72 746 83 T 791 137 V 623 Q 791 723 762 787 T 643 852 Q 524 852 447 757 T 371 541 V 137 Q 371 94 416 83 T 530 72 V 0 H 61 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 277.78000, 0.00000)"></path></g><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 5123.94287, 0.00000)"></path><path d="M 115 -471 Q 115 -465 117 -463 L 829 1511 Q 833 1523 843 1529 T 866 1536 Q 884 1536 895 1525 T 907 1495 V 1487 L 195 -487 Q 183 -512 156 -512 Q 139 -512 127 -500 T 115 -471 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 5644.54199, 0.00000)"></path><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 6144.54199, 0.00000)"></path><g transform="translate(6665.14111, 0.00000)"><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(388.89001, -362.89200)"><path d="M 233 160 Q 268 114 324 85 T 443 44 T 571 33 Q 658 33 715 78 T 798 198 T 825 356 Q 825 442 798 515 T 713 634 T 569 680 H 418 Q 410 680 402 687 T 395 702 V 723 Q 395 732 402 738 T 418 745 L 547 754 Q 653 754 717 858 T 782 1077 Q 782 1173 725 1232 T 571 1292 Q 487 1292 413 1267 T 291 1188 Q 334 1188 363 1154 T 393 1077 Q 393 1033 362 1001 T 285 969 Q 238 969 206 1001 T 174 1077 Q 174 1172 235 1236 T 388 1330 T 571 1360 Q 664 1360 760 1329 T 922 1234 T 989 1077 Q 989 950 905 855 T 694 717 Q 785 698 867 649 T 1001 525 T 1053 356 Q 1053 236 981 145 T 798 7 T 571 -41 Q 463 -41 358

Knuth [1] recently showed how to estimate the size of a backtrack tree by repeatedly following random paths from the root. Often the efficiency of his method can be greatly improved by occasionally following more than one path from a node. This results in estimating the size of the backtrack tree by doing a very abbreviated partial backtrack search. An analysis shows that this modification results in an improvement which increases exponentially with the height of the tree. Experimental results for a particular tree of height 84 show an order of magnitude improvement. The measuring method is easy to add to a backtrack program.

We assume a directed graph whose nodes are labeled by integers between 1 and n. The arcs of this graph correspond to the flow of control between blocks of a computer program. The initial node of this graph (corresponding to the entry point of the program) is labeled by the integer 1. For optimizing the object code generated by a compiler, the relationship of immediate predominator has been used by Lowry and Medlock [3]. We say that node i predominates node k if every path from node 1 to node k passes through (ie both into and out of) node i. Node j is an immediate predominator of node k if node j predominates node k and if every other node i which predominates node k also predominates node j. It can easily be proved that if k≠ 1 and node k is reachable from node 1t hen node k has exactly one immediate predominator. In case k= 1, or node k is not reachable from node 1, the immediate predominator of …

The utilization of space and the running speed of the buddy system are considered Equations are derived that give various statistical properties of the buddy system. For the bottom level with Poisson requests and exponential service times the expected amount of space wasted by pairing full cells with empty cells is about 0.513 ρ 1/2 and the mean time between requests from the bottom level to the next level is about 1.880 ρ 1/2 λ-1, where ρ is the mean number of blocks in use on the bottom level and λ-1 is the mean time between requests for blocks on the bottom level. The results of a number of simulations of the buddy system are also given and compared with the analytical studies.

The order in which the variables are tested in a backtrack program can have a major effect on its running time. The best search order usually varies among the branches of the backtrack tree, so the number of possible search orders can be astronomical. We present an algorithm that chooses a search order dynamically by investigating all possibilities for k levels below the current level, extending beyond k levels wherever possible by setting the variables that have unique forced values. The algorithm takes time O(n ^k+1) to process a node. For k=2 and binary variables the analysis for selecting the next variable to introduce into the backtrack tree makes complete use of the information contained in the two-level investigations. For larger k or variables of higher degree there is no polynomial-time algorithm that makes complete use of the k-level investigations to limit searching (unless P=NP). The search …

A class of random conjunctive-normal-form (CNF) predicates is characterized by v, the number of variables from which literals may be formed (giving 2v literals); p (v), the probability that a given literal is in a random clause; and t (v), the number of random independently selected clauses in a random predicate. Determining satisfiability on such a class using backtracking takes polynomial average time under the following conditions:(1) lim v→∞ vp (v)= 0 and t (v)⩾(ln 2+ ϵ) v [− ln ((v+ l) p (v))]; and (2) lim vp (v)=∞, lim p (v)= 0, and t (v)⩾[(ln 2+ ϵ) ep (v)] exp [2vp (v)] for any fixed ϵ&gt; 0. Additional cases are also covered. An analysis by Goldberg showed that problems for which p (v) is constant can be solved in polynomial average time by a simplified Davis-Putnam procedure. We give an algorithm for solving problems with t (v)⩽(ln ln v) ln 3 in polynomial worst-case time. Thus all problem sets for which p (v) or t (v) grows …

The search rearrangement backtracking algorithm of Bitner and Reingold [Comm. ACM, 18 (1975), pp. 651–655] introduces at each level of the backtrack tree a variable with a minimal number of remaining values; search order may differ on different branches. For conjunctive normal form formulas with v variables, s literals per term <svg aria-label="(s \geqq 3)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="43px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.54200)"><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 178 125 Q 233 31 399 31 Q 471 31 536 55 T 643 129 T 686 248 Q 686 301 648 335 T 555 381 L 444 403 Q 368 422 319 474 T 270 600 Q 270 691 319 761 T 450 868 T 618 905 Q 711 905 784 860 T 858 729 Q 858 682 831 646 T 758 610 Q 731 610 711 627 T 692 672 Q 692 696 705 718 T 741 754 T 788 768 Q 770 812 720 832 T 614 852 Q 562 852 510 831 T 426 769 T 395 674 Q 395 637 421 609 T 485 569 L 604 545 Q 661 533 708 502 T 783 425 T 811 319 Q 811 243 768 169 T 664 51 Q 555 -23 397 -23 Q 288 -23 197 27 T 106 176 Q 106 232 138 273 T 227 315 Q 260 315 282 295 T 305 242 Q 305 195 270 160 T 188 125 H 178 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 388.89001, 0.00000)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 170 397 Q 170 423 197 436 L 1284 950 L 190 1466 Q 170 1476 170 1501 Q 170 1518 181 1530 T 211 1542 Q 221 1542 227 1540 L 1403 985 Q 1421 976 1421 950 Q 1421 926 1397 911 L 227 360 Q 221 356 211 356 Q 194 356 182 369 T 170 397 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1135.44861, 0.00000)"></path><path d="M 195 158 Q 243 88 324 54 T 498 20 Q 617 20 667 121 T 717 352 Q 717 410 706 468 T 671 576 T 602 656 T 496 686 H 360 Q 342 686 342 705 V 723 Q 342 739 360 739 L 473 748 Q 545 748 592 802 T 662 933 T 684 1081 Q 684 1179 638 1242 T 498 1305 Q 420 1305 349 1275 T 236 1186 Q 240 1187 243 1187 T 250 1188 Q 296 1188 327 1156 T 358 1079 Q 358 1035 327 1003 T 250 971 Q 205 971 173 1003 T 141 1079 Q 141 1167 194 1232 T 330 1330 T 498 1364 Q 560 1364 629 1345 T 754 1292 T 845 1204 T 881 1081 Q 881 995 842 922 T 737 796 T 590 717 Q 679 700 759 650 T 887 522 T 936 354 Q 936 241 874 149 T 711 6 T 498 -45 Q 402 -45 305 -9 T 147 101 T 86 276 Q 86 327 120 361 T 205 395 Q 238 395 265 379 T 308 336 T 324 276 Q 324 226 289 192 T 205 158 H 195 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2191.00732, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2691.00732, 0.00000)"></path></g></svg>, and <svg aria-label="v^\alpha " class="gs_fsvg" height="10px" style="vertical-align:0px;" width="14px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 9.40229)"><g><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 123 338 Q 123 483 210 614 T 435 824 T 717 903 Q 800 903 872 874 T 999 792 T 1083 668 T 1114 514 L 1118 399 Q 1255 578 1307 788 Q 1311 805 1327 805 H 1360 Q 1371 805 1376 798 T 1382 780 V 774 Q 1359 684 1322 601 T 1236 441 T 1124 293 Q 1124 245 1128 193 T 1148 93 T 1194 45 Q 1235 45 1259 64 T 1301 115 T 1329 147 H 1362 Q 1371 147 1377 140 T 1384 123 Q 1384 85 1352 52 T 1273 0 T 1190 -20 Q 1110 -20 1054 27 T 973 154 Q 867 72 746 26 T 498 -20 Q 394 -20 308 25 T 172 151 T 123 338 Z M 504 45 Q 624 45 741 94 T 956 227 Q 956 239 955 246 T 954 262 L 944 477 Q 944 559 922 642 T 848 781 T 713 838 Q 616 838 538 784 T 408 642 T 328 453 T 301 264 Q 301 170 356 107 T 504 45 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 484.72000, -362.89200)"></path></g></g></svg> terms <svg aria-label="((s/2) &lt; \alpha &lt; s)" class="gs_fsvg" height="14px" style="vertical-align:-4px;" width="95px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.50000)"><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 388.89001, 0.00000)"></path><path d="M 178 125 Q 233 31 399 31 Q 471 31 536 55 T 643 129 T 686 248 Q 686 301 648 335 T 555 381 L 444 403 Q 368 422 319 474 T 270 600 Q 270 691 319 761 T 450 868 T 618 905 Q 711 905 784 860 T 858 729 Q 858 682 831 646 T 758 610 Q 731 610 711 627 T 692 672 Q 692 696 705 718 T 741 754 T 788 768 Q 770 812 720 832 T 614 852 Q 562 852 510 831 T 426 769 T 395 674 Q 395 637 421 609 T 485 569 L 604 545 Q 661 533 708 502 T 783 425 T 811 319 Q 811 243 768 169 T 664 51 Q 555 -23 397 -23 Q 288 -23 197 27 T 106 176 Q 106 232 138 273 T 227 315 Q 260 315 282 295 T 305 242 Q 305 195 270 160 T 188 125 H 178 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 777.78003, 0.00000)"></path><path d="M 115 -471 Q 115 -465 117 -463 L 829 1511 Q 833 1523 843 1529 T 866 1536 Q 884 1536 895 1525 T 907 1495 V 1487 L 195 -487 Q 183 -512 156 -512 Q 139 -512 127 -500 T 115 -471 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1246.56006, 0.00000)"></path><path d="M 102 0 V 55 Q 102 60 106 66 L 424 418 Q 496 496 541 549 T 630 671 T 699 811 T 725 963 Q 725 1047 694 1123 T 601 1246 T 453 1292 Q 364 1292 293 1238 T 193 1100 Q 201 1102 215 1102 Q 261 1102 293 1071 T 326 991 Q 326 944 293 911 T 215 879 Q 167 879 134 912 T 102 991 Q 102 1068 131 1135 T 214 1255 T 337 1336 T 483 1364 Q 600 1364 701 1314 T 861 1174 T 920 963 Q 920 874 881 794 T 781 648 T 625 500 T 500 389 L 268 166 H 465 Q 610 166 707 168 T 811 176 Q 835 202 860 365 H 920 L 862 0 H 102 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1746.56006, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2246.56006, 0.00000)"></path><path d="M 190 477 Q 170 486 170 512 Q 170 538 197 551 L 1366 1102 Q 1374 1106 1380 1106 Q 1398 1106 1409 1093 T 1421 1065 Q 1421 1040 1397 1026 L 307 512 L 1403 -6 Q 1421 -12 1421 -41 Q 1421 -57 1409 -70 T 1380 -82 Q 1374 -82 1366 -78 L 190 477 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2913.22876, 0.00000)"></path><path d="M 412 -23 Q 315 -23 239 23 T 123 147 T 82 324 Q 82 463 159 599 T 365 820 T 635 905 Q 739 905 818 850 T 938 705 T 979 512 L 981 375 Q 1051 472 1099 576 T 1174 793 Q 1178 805 1190 805 H 1214 Q 1233 805 1233 786 Q 1233 784 1231 780 Q 1207 686 1171 599 T 1086 432 T 981 285 Q 981 31 1040 31 Q 1078 31 1102 53 T 1145 109 T 1169 143 H 1194 Q 1210 143 1210 123 Q 1210 72 1151 24 T 1036 -23 Q 962 -23 913 25 T 846 150 Q 750 68 638 22 T 412 -23 Z M 416 31 Q 635 31 836 211 Q 835 223 833 240 T 831 260 V 481 Q 831 852 631 852 Q 511 852 421 749 T 285 504 T 240 244 Q 240 155 285 93 T 416 31 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 3968.78735, 0.00000)"></path><path d="M 190 477 Q 170 486 170 512 Q 170 538 197 551 L 1366 1102 Q 1374 1106 1380 1106 Q 1398 1106 1409 1093 T 1421 1065 Q 1421 1040 1397 1026 L 307 512 L 1403 -6 Q 1421 -12 1421 -41 Q 1421 -57 1409 -70 T 1380 -82 Q 1374 -82 1366 -78 L 190 477 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 4889.98779, 0.00000)"></path><path d="M 178 125 Q 233 31 399 31 Q 471 31 536 55 T 643 129 T 686 248 Q 686 301 648 335 T 555 381 L 444 403 Q 368 422 319 474 T 270 600 Q 270 691 319 761 T 450 868 T 618 905 Q 711 905 784 860 T 858 729 Q 858 682 831 646 T 758 610 Q 731 610 711 627 T 692 672 Q 692 696 705 718 T 741 754 T 788 768 Q 770 812 720 832 T 614 852 Q 562 852 510 831 T 426 769 T 395 674 Q 395 637 421 609 T 485 569 L 604 545 Q 661 533 708 502 T 783 425 T 811 319 Q 811 243 768 169 T 664 51 Q 555 -23 397 -23 Q 288 -23 197 27 T 106 176 Q 106 232 138 273 T 227 315 Q 260 315 282 295 T 305 242 Q 305 195 270 160 T 188 125 H 178 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 5945.54639, 0.00000)"></path><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 6414.32617, 0.00000)"></path></g></svg>, the average number of nodes in a search rearrangement backtrack tree is <svg aria-label="\exp [\Theta (v^{(s - \alpha - 1)/(s - 2)} )]" class="gs_fsvg" height="16px" style="vertical-align:-4px;" width="136px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 12.43049)"><g><path d="M 510 -23 Q 385 -23 280 42 T 116 217 T 57 449 Q 57 569 111 677 T 263 851 T 481 918 Q 575 918 644 886 T 759 799 T 827 667 T 850 500 Q 850 473 829 473 H 236 V 451 Q 236 281 304 159 T 528 37 Q 591 37 644 65 T 737 143 T 791 250 Q 793 257 798 262 T 811 268 H 829 Q 850 268 850 242 Q 821 126 725 51 T 510 -23 Z M 238 524 H 705 Q 705 601 683 680 T 612 811 T 481 864 Q 365 864 301 755 T 238 524 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 25 0 V 72 Q 103 72 172 102 T 289 193 L 475 430 L 233 745 Q 197 790 154 800 T 35 811 V 883 H 461 V 811 Q 434 811 410 799 T 387 764 Q 387 756 393 745 L 557 532 L 680 690 Q 705 720 705 750 Q 705 775 688 793 T 645 811 V 883 H 1022 V 811 Q 943 811 873 780 T 756 690 L 594 483 L 856 137 Q 895 92 937 82 T 1057 72 V 0 H 631 V 72 Q 656 72 679 84 T 702 119 Q 702 128 696 137 L 512 381 L 365 193 Q 342 167 342 133 Q 342 108 359 90 T 399 72 V 0 H 25 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 444.44000, 0.00000)"></path><path d="M 53 -397 V -326 Q 123 -326 168 -314 T 213 -260 V 727 Q 213 783 173 797 T 53 811 V 883 L 356 905 V 778 Q 412 840 486 872 T 645 905 Q 766 905 863 839 T 1014 667 T 1069 442 Q 1069 318 1008 211 T 843 40 T 614 -23 Q 465 -23 362 98 V -260 Q 362 -302 407 -314 T 522 -326 V -397 H 53 Z M 362 199 Q 398 126 462 78 T 602 31 Q 673 31 727 69 T 819 171 T 873 305 T 891 442 Q 891 524 861 619 T 771 780 T 625 846 Q 542 846 472 803 T 362 688 V 199 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 972.22003, 0.00000)"></path></g><path d="M 242 -512 V 1536 H 522 V 1454 H 324 V -430 H 522 V -512 H 242 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1527.78003, 0.00000)"></path><path d="M 797 -45 Q 602 -45 446 58 T 203 333 T 115 694 Q 115 834 165 971 T 306 1214 T 524 1382 T 797 1444 Q 942 1444 1069 1381 T 1288 1212 T 1428 972 T 1477 694 Q 1477 505 1389 333 T 1145 58 T 797 -45 Z M 449 207 Q 488 150 541 105 T 660 35 T 797 10 Q 900 10 990 63 T 1143 207 Q 1270 390 1270 694 Q 1270 1001 1143 1190 Q 1082 1280 991 1335 T 797 1391 Q 691 1391 600 1335 T 449 1190 Q 380 1087 351 962 T 322 694 Q 322 601 333 516 T 373 353 T 449 207 Z M 438 549 V 852 H 498 V 782 H 1094 V 852 H 1153 V 549 H 1094 V 618 H 498 V 549 H 438 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1805.56006, 0.00000)"></path><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 2583.34009, 0.00000)"></path><g transform="translate(2972.22998, 0.00000)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(484.72000, -362.89200)"><path d="M 715 -512 Q 554 -395 445 -233 T 284 119 T 231 512 Q 231 662 260 807 T 350 1084 T 501 1330 T 715 1534 Q 718 1535 720 1535 T 725 1536 H 745 Q 755 1536 761 1529 T 768 1511 Q 768 1498 760 1493 Q 658 1405 584 1292 T 465 1051 T 400 788 T 379 512 Q 379 219 469 -41 T 760 -471 Q 768 -476 768 -489 Q 768 -500 761 -507 T 745 -514 H 725 Q 723 -513 720 -513 T 715 -512 Z " transform="scale(0.34180, -0.34180)"></path><path d="M 244 123 Q 300 45 477 45 Q 544 45 615 65 T 734 131 T 782 248 Q 782 299 738 330 T 637 373 L 504 397 Q 425 413 370 468 T 315 598 Q 315 693 369 762 T 511 867 T 692 903 Q 752 903 815 885 T 919 828 T 961 727 Q 961 678 933 641 T 858 604 Q 829 604 807 623 T 786 672 Q 786 707 810 735 T 868 770 Q 822 838 688 838 Q 601 838 528 796 T 455 672 Q 455 597 561 573 L 696 549 Q 788 531 855 470 T 922 319 Q 922 242 876 168 T 762 51 Q 647 -20 475 -20 Q 350 -20 247 25 T 145 178 Q 145 235 179 277 T 270 319 Q 305 319 328 298 T 352 242 Q 352 196 321 162 T 244 123 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 312.50800, 0.00000)"></path><path d="M 268 461 Q 248 464 234 477 T 221 512 Q 221 554 268 561 H 1559 Q 1606 554 1606 512 Q 1606 491 1592 477 T 1559 461 H 268 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 689.92700, 0.00000)"></path><path d="M 123 338 Q 123 483 210 614 T 435 824 T 717 903 Q 800 903 872 874 T 999 792 T 1083 668 T 1114 514 L 1118 399 Q 1255 578 1307 788 Q 1311 805 1327 805 H 1360 Q 1371 805 1376 798 T 1382 780 V 774 Q 1359 684 1322 601 T 1236 441 T 1124 293 Q 1124 245 1128 193 T 1148 93 T 1194 45 Q 1235 45 1259 64 T 1301 115 T 1329 147 H 1362 Q 1371 147 1377 140 T 1384 123 Q 1384 85 1352 52 T 1273 0 T 1190 -20 Q 1110 -20 1054 27 T 973 154 Q 867 72 746 26 T 498 -20 Q 394 -20 308 25 T 172 151 T 123 338 Z M 504 45 Q 624 45 741 94 T 956 227 Q 956 239 955 246 T 954 262 L 944 477 Q 944 559 922 642 T 848 781 T 713 838 Q 616 838 538 784 T 408 642 T 328 453 T 301 264 Q 301 170 356 107 T 504 45 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 1314.90796, 0.00000)"></path><path d="M 268 461 Q 248 464 234 477 T 221 512 Q 221 554 268 561 H 1559 Q 1606 554 1606 512 Q 1606 491 1592 477 T 1559 461 H 268 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 1834.77686, 0.00000)"></path><path d="M 233 0 V 82 Q 516 82 516 143 V 1202 Q 401 1147 219 1147 V 1229 Q 341 1229 447 1258 T 629 1360 H 666 Q 685 1355 690 1335 V 143 Q 690 82 973 82 V 0 H 233 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 2459.75781, 0.00000)"></path><path d="M 166 -514 Q 156 -514 149 -507 T 143 -489 Q 143 -476 152 -471 Q 256 -382 329 -268 T 446 -28 T 511 236 T 532 512 Q 532 652 511 788 T 446 1052 T 327 1293 T 152 1493 Q 143 1498 143 1511 Q 143 1521 149 1528 T 166 1536 H 186 Q 189 1536 191 1535 T 197 1534 Q 356 1417 465 1255 T 627 904 T 680 512 Q 680 307 627 117 T 464 -234 T 197 -512 Q 194 -512 191 -513 T 186 -514 H 166 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 2858.36572, 0.00000)"></path><path d="M 143 -463 Q 143 -458 147 -444 L 924 1505 Q 940 1536 971 1536 Q 990 1536 1005 1521 T 1020 1487 Q 1020 1480 1019 1476 T 1018 1468 L 242 -481 Q 221 -512 195 -512 Q 175 -512 159 -497 T 143 -463 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 3170.87378, 0.00000)"></path><path d="M 715 -512 Q 554 -395 445 -233 T 284 119 T 231 512 Q 231 662 260 807 T 350 1084 T 501 1330 T 715 1534 Q 718 1535 720 1535 T 725 1536 H 745 Q 755 1536 761 1529 T 768 1511 Q 768 1498 760 1493 Q 658 1405 584 1292 T 465 1051 T 400 788 T 379 512 Q 379 219 469 -41 T 760 -471 Q 768 -476 768 -489 Q 768 -500 761 -507 T 745 -514 H 725 Q 723 -513 720 -513 T 715 -512 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 3569.48169, 0.00000)"></path><path d="M 244 123 Q 300 45 477 45 Q 544 45 615 65 T 734 131 T 782 248 Q 782 299 738 330 T 637 373 L 504 397 Q 425 413 370 468 T 315 598 Q 315 693 369 762 T 511 867 T 692 903 Q 752 903 815 885 T 919 828 T 961 727 Q 961 678 933 641 T 858 604 Q 829 604 807 623 T 786 672 Q 786 707 810 735 T 868 770 Q 822 838 688 838 Q 601 838 528 796 T 455 672 Q 455 597 561 573 L 696 549 Q 788 531 855 470 T 922 319 Q 922 242 876 168 T 762 51 Q 647 -20 475 -20 Q 350 -20 247 25 T 145 178 Q 145 235 179 277 T 270 319 Q 305 319 328 298 T 352 242 Q 352 196 321 162 T 244 123 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 3881.98975, 0.00000)"></path><path d="M 268 461 Q 248 464 234 477 T 221 512 Q 221 554 268 561 H 1559 Q 1606 554 1606 512 Q 1606 491 1592 477 T 1559 461 H 268 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 4259.40869, 0.00000)"></path><path d="M 129 0 V 59 Q 129 68 137 76 L 502 432 Q 523 454 535 466 T 571 502 Q 692 623 759 727 T 827 956 Q 827 1024 804 1083 T 739 1187 T 641 1254 T 516 1278 Q 425 1278 349 1231 T 236 1104 H 242 Q 291 1104 322 1071 T 354 991 Q 354 945 322 912 T 242 879 Q 195 879 162 912 T 129 991 Q 129 1101 190 1185 T 349 1314 T 551 1360 Q 675 1360 786 1313 T 965 1174 T 1034 956 Q 1034 865 993 786 T 892 648 T 726 505 T 588 395 L 338 182 H 526 Q 603 182 687 182 T 836 185 T 905 193 Q 923 212 934 261 T 956 381 H 1034 L 973 0 H 129 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 4884.38965, 0.00000)"></path><path d="M 166 -514 Q 156 -514 149 -507 T 143 -489 Q 143 -476 152 -471 Q 256 -382 329 -268 T 446 -28 T 511 236 T 532 512 Q 532 652 511 788 T 446 1052 T 327 1293 T 152 1493 Q 143 1498 143 1511 Q 143 1521 149 1528 T 166 1536 H 186 Q 189 1536 191 1535 T 197 1534 Q 356 1417 465 1255 T 627 904 T 680 512 Q 680 307 627 117 T 464 -234 T 197 -512 Q 194 -512 191 -513 T 186 -514 H 166 Z " transform="matrix(0.34180, 0.00000, 0.00000, -0.34180, 5282.99756, 0.00000)"></path></g></g><path d="M 133 -512 Q 115 -512 115 -494 Q 115 -485 119 -481 Q 469 -139 469 512 Q 469 1163 123 1501 Q 115 1506 115 1518 Q 115 1525 120 1530 T 133 1536 H 152 Q 158 1536 162 1532 Q 309 1416 407 1250 T 550 896 T 596 512 Q 596 367 571 226 T 493 -51 T 358 -303 T 162 -508 Q 158 -512 152 -512 H 133 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 9052.45508, 0.00000)"></path><path d="M 45 -512 V -430 H 244 V 1454 H 45 V 1536 H 326 V -512 H 45 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 9441.34473, 0.00000)"></path></g></svg> (i.e., for some positive constants <svg aria-label="a_1 ,a_2 " class="gs_fsvg" height="9px" style="vertical-align:-3px;" width="34px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 6.18800)"><g><path d="M 356 -23 Q 227 -23 152 74 T 78 305 Q 78 436 146 577 T 329 811 T 578 905 Q 639 905 687 872 T 762 782 Q 785 864 852 864 Q 878 864 895 848 T 913 807 Q 913 801 912 798 T 911 791 L 768 219 Q 754 158 754 119 Q 754 31 813 31 Q 877 31 910 112 T 967 301 Q 971 313 983 313 H 1008 Q 1016 313 1021 306 T 1026 293 Q 990 150 947 63 T 809 -23 Q 740 -23 687 17 T 621 125 Q 489 -23 356 -23 Z M 358 31 Q 432 31 501 86 T 621 217 Q 623 219 623 223 L 733 668 L 735 674 Q 723 747 682 799 T 573 852 Q 504 852 444 795 T 344 662 Q 304 580 267 437 T 231 215 Q 231 144 261 87 T 358 31 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(528.60999, 150.00000)"><path d="M 233 0 V 82 Q 516 82 516 143 V 1202 Q 401 1147 219 1147 V 1229 Q 341 1229 447 1258 T 629 1360 H 666 Q 685 1355 690 1335 V 143 Q 690 82 973 82 V 0 H 233 Z " transform="scale(0.34180, -0.34180)"></path></g></g><path d="M 203 -369 Q 203 -360 211 -352 Q 285 -281 326 -188 T 367 8 V 33 Q 334 0 285 0 Q 238 0 205 33 T 172 113 Q 172 161 205 193 T 285 225 Q 358 225 389 157 T 420 8 Q 420 -106 374 -209 T 246 -393 Q 238 -397 233 -397 Q 223 -397 213 -388 T 203 -369 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 977.21802, 0.00000)"></path><g transform="translate(1421.66516, 0.00000)"><path d="M 356 -23 Q 227 -23 152 74 T 78 305 Q 78 436 146 577 T 329 811 T 578 905 Q 639 905 687 872 T 762 782 Q 785 864 852 864 Q 878 864 895 848 T 913 807 Q 913 801 912 798 T 911 791 L 768 219 Q 754 158 754 119 Q 754 31 813 31 Q 877 31 910 112 T 967 301 Q 971 313 983 313 H 1008 Q 1016 313 1021 306 T 1026 293 Q 990 150 947 63 T 809 -23 Q 740 -23 687 17 T 621 125 Q 489 -23 356 -23 Z M 358 31 Q 432 31 501 86 T 621 217 Q 623 219 623 223 L 733 668 L 735 674 Q 723 747 682 799 T 573 852 Q 504 852 444 795 T 344 662 Q 304 580 267 437 T 231 215 Q 231 144 261 87 T 358 31 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(528.60999, 150.00000)"><path d="M 129 0 V 59 Q 129 68 137 76 L 502 432 Q 523 454 535 466 T 571 502 Q 692 623 759 727 T 827 956 Q 827 1024 804 1083 T 739 1187 T 641 1254 T 516 1278 Q 425 1278 349 1231 T 236 1104 H 242 Q 291 1104 322 1071 T 354 991 Q 354 945 322 912 T 242 879 Q 195 879 162 912 T 129 991 Q 129 1101 190 1185 T 349 1314 T 551 1360 Q 675 1360 786 1313 T 965 1174 T 1034 956 Q 1034 865 993 786 T 892 648 T 726 505 T 588 395 L 338 182 H 526 Q 603 182 687 182 T 836 185 T 905 193 Q 923 212 934 261 T 956 381 H 1034 L 973 0 H 129 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg>, and <svg aria-label="v_0 " class="gs_fsvg" height="8px" style="vertical-align:-2px;" width="13px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 6.20200)"><g><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(484.72000, 150.00000)"><path d="M 582 -41 Q 396 -41 289 60 T 143 314 T 104 651 Q 104 951 208 1155 T 582 1360 Q 853 1360 956 1155 T 1059 651 Q 1059 468 1019 314 T 874 60 T 582 -41 Z M 582 25 Q 710 25 772 134 T 849 380 T 864 686 Q 864 848 849 973 T 773 1196 T 582 1294 Q 482 1294 422 1233 T 337 1081 T 305 897 T 299 686 Q 299 564 305 464 T 338 262 T 424 92 T 582 25 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg>, when <svg aria-label="v \geqq v_0 " class="gs_fsvg" height="13px" style="vertical-align:-2px;" width="39px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 10.54200)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 209 -356 Q 192 -356 181 -344 T 170 -315 Q 170 -300 181 -287 T 209 -274 H 1384 Q 1400 -274 1410 -287 T 1421 -315 Q 1421 -332 1410 -344 T 1384 -356 H 209 Z M 209 41 Q 192 41 181 53 T 170 82 Q 170 97 181 110 T 209 123 H 1384 Q 1400 123 1410 110 T 1421 82 Q 1421 65 1410 53 T 1384 41 H 209 Z M 170 397 Q 170 423 197 436 L 1284 950 L 190 1466 Q 170 1476 170 1501 Q 170 1518 181 1530 T 211 1542 Q 221 1542 227 1540 L 1403 985 Q 1421 976 1421 950 Q 1421 926 1397 911 L 227 360 Q 221 356 211 356 Q 194 356 182 369 T 170 397 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 798.37756, 0.00000)"></path><g transform="translate(1853.93616, 0.00000)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(484.72000, 150.00000)"><path d="M 582 -41 Q 396 -41 289 60 T 143 314 T 104 651 Q 104 951 208 1155 T 582 1360 Q 853 1360 956 1155 T 1059 651 Q 1059 468 1019 314 T 874 60 T 582 -41 Z M 582 25 Q 710 25 772 134 T 849 380 T 864 686 Q 864 848 849 973 T 773 1196 T 582 1294 Q 482 1294 422 1233 T 337 1081 T 305 897 T 299 686 Q 299 564 305 464 T 338 262 T 424 92 T 582 25 Z " transform="scale(0.34180, -0.34180)"></path></g></g></g></svg> the number of nodes is between <svg aria-label="\exp (a_1 v^{(s - \alpha - 1)/(s - 2)} )" class="gs_fsvg" height="16px" style="vertical-align:-4px;" width="131px"><g transform="matrix(0.01400, 0.00000, 0.00000, 0.01400, 0.00000, 12.43049)"><g><path d="M 510 -23 Q 385 -23 280 42 T 116 217 T 57 449 Q 57 569 111 677 T 263 851 T 481 918 Q 575 918 644 886 T 759 799 T 827 667 T 850 500 Q 850 473 829 473 H 236 V 451 Q 236 281 304 159 T 528 37 Q 591 37 644 65 T 737 143 T 791 250 Q 793 257 798 262 T 811 268 H 829 Q 850 268 850 242 Q 821 126 725 51 T 510 -23 Z M 238 524 H 705 Q 705 601 683 680 T 612 811 T 481 864 Q 365 864 301 755 T 238 524 Z " transform="scale(0.48828, -0.48828)"></path><path d="M 25 0 V 72 Q 103 72 172 102 T 289 193 L 475 430 L 233 745 Q 197 790 154 800 T 35 811 V 883 H 461 V 811 Q 434 811 410 799 T 387 764 Q 387 756 393 745 L 557 532 L 680 690 Q 705 720 705 750 Q 705 775 688 793 T 645 811 V 883 H 1022 V 811 Q 943 811 873 780 T 756 690 L 594 483 L 856 137 Q 895 92 937 82 T 1057 72 V 0 H 631 V 72 Q 656 72 679 84 T 702 119 Q 702 128 696 137 L 512 381 L 365 193 Q 342 167 342 133 Q 342 108 359 90 T 399 72 V 0 H 25 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 444.44000, 0.00000)"></path><path d="M 53 -397 V -326 Q 123 -326 168 -314 T 213 -260 V 727 Q 213 783 173 797 T 53 811 V 883 L 356 905 V 778 Q 412 840 486 872 T 645 905 Q 766 905 863 839 T 1014 667 T 1069 442 Q 1069 318 1008 211 T 843 40 T 614 -23 Q 465 -23 362 98 V -260 Q 362 -302 407 -314 T 522 -326 V -397 H 53 Z M 362 199 Q 398 126 462 78 T 602 31 Q 673 31 727 69 T 819 171 T 873 305 T 891 442 Q 891 524 861 619 T 771 780 T 625 846 Q 542 846 472 803 T 362 688 V 199 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 972.22003, 0.00000)"></path></g><path d="M 635 -508 Q 521 -418 438 -302 T 303 -53 T 225 223 T 199 512 Q 199 659 225 803 T 304 1080 T 441 1329 T 635 1532 Q 635 1536 645 1536 H 664 Q 670 1536 675 1530 T 680 1518 Q 680 1509 676 1505 Q 576 1407 509 1295 T 402 1056 T 344 794 T 326 512 Q 326 -139 674 -477 Q 680 -483 680 -494 Q 680 -499 674 -506 T 664 -512 H 645 Q 635 -512 635 -508 Z " transform="matrix(0.48828, 0.00000, 0.00000, -0.48828, 1527.78003, 0.00000)"></path><g transform="translate(1916.67004, 0.00000)"><path d="M 356 -23 Q 227 -23 152 74 T 78 305 Q 78 436 146 577 T 329 811 T 578 905 Q 639 905 687 872 T 762 782 Q 785 864 852 864 Q 878 864 895 848 T 913 807 Q 913 801 912 798 T 911 791 L 768 219 Q 754 158 754 119 Q 754 31 813 31 Q 877 31 910 112 T 967 301 Q 971 313 983 313 H 1008 Q 1016 313 1021 306 T 1026 293 Q 990 150 947 63 T 809 -23 Q 740 -23 687 17 T 621 125 Q 489 -23 356 -23 Z M 358 31 Q 432 31 501 86 T 621 217 Q 623 219 623 223 L 733 668 L 735 674 Q 723 747 682 799 T 573 852 Q 504 852 444 795 T 344 662 Q 304 580 267 437 T 231 215 Q 231 144 261 87 T 358 31 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(528.60999, 150.00000)"><path d="M 233 0 V 82 Q 516 82 516 143 V 1202 Q 401 1147 219 1147 V 1229 Q 341 1229 447 1258 T 629 1360 H 666 Q 685 1355 690 1335 V 143 Q 690 82 973 82 V 0 H 233 Z " transform="scale(0.34180, -0.34180)"></path></g></g><g transform="translate(2893.88818, 0.00000)"><path d="M 219 231 Q 219 277 230 332 T 252 422 T 302 561 T 342 668 Q 369 743 369 791 Q 369 852 324 852 Q 243 852 190 768 T 113 582 Q 109 569 96 569 H 72 Q 55 569 55 588 V 594 Q 88 716 156 810 T 328 905 Q 401 905 451 857 T 502 735 Q 502 697 485 655 Q 445 551 422 488 T 379 348 T 360 205 Q 360 128 395 79 T 506 31 Q 648 31 762 250 Q 798 321 830 417 T 862 573 Q 862 635 842 669 T 790 741 T 758 801 Q 758 841 791 874 T 864 907 Q 913 907 934 862 T 956 760 Q 956 692 936 598 T 882 403 T 819 244 Q 684 -23 504 -23 Q 375 -23 297 41 T 219 231 Z " transform="scale(0.48828, -0.48828)"></path><g transform="translate(484.72000, -362.89200)"><path d="M 715 -512 Q 554 -395 445 -233 T 284 119 T 231 512 Q 231 662 260 807 T 350 1084 T 501 1330 T 715 1534 Q 718 1535 720 1535 T 725 1536 H 745 Q 755 1536 761 1529 T 768 1511 Q 768 1498 760 1493 Q 658 1405 584 1292 T 465 1051 T 400 788 T 379 512 Q 379 219 469 -41 T 760 -471 Q 768 -476 768 -489 Q 768 -500 761 -507 T 745 -514 H 725 Q 723 -513 720 -513 T 715 -512 Z " transform="scale(0.34180, -0.34180)"></path><path d="M 244 123 Q 300 45 477 45 Q 544 45 615 65 T 734 131 T 782 248 Q 782 299 738 330 T 637 373 L 504 397