Changeset 206
- Timestamp:
- Feb 5, 2008, 9:55:58 AM (18 years ago)
- Author:
- neil.c.c.brown
- Message:
-
Various tweaks to the notes pages of the slides to make the whole thing mroe readable.
- File:
-
- 1 edited
- docs/trunk/omega-test-slides/omega-test.tex (modified) (14 diffs)
Legend:
- Unmodified
- Added
- Removed
-
docs/trunk/omega-test-slides/omega-test.tex
r205 r206 93 93 94 94 \note{We are checking if any of array indexes can be equal to each other 95 within the bounds of the array. So we set (削除) the (削除ここまで)indexes equal in an95 within the bounds of the array. So we set (追記) a pair of (追記ここまで) indexes equal in an 96 96 equation, and also add inequalities specifying that each index must 97 97 be within bounds. … … 100 100 No solution to any of the equations means the indexes are disjoint, and 101 101 hence the access is safe. If there is a solution to any of them, the 102 access is unsafe (削除) (削除ここまで)}102 access is unsafe(追記) . (追記ここまで)} 103 103 104 104 \end{frame} … … 318 318 \begin{frame} 319 319 \fullframegraph{Inequalities}{inequality-normal} 320 \note{This is an acceptable pair of inequalities (削除) (削除ここまで)}320 \note{This is an acceptable pair of inequalities(追記) with parallel bounds. (追記ここまで)} 321 321 \end{frame} 322 322 323 323 \begin{frame} 324 324 \fullframegraph{Unsolveable Inequalities}{inequality-unsolveable} 325 \note{This is an unsolveable pair of inequalities (削除) ; there is no overlap between the two regions (削除ここまで)}325 \note{This is an unsolveable pair of inequalities(追記) (with parallel bounds); there is no overlap between the two regions. (追記ここまで)} 326 326 \end{frame} 327 327 … … 330 330 \note{Here, the green inequality is redundant; anything in the red area 331 331 is also in the green area, so we should only concern ourselves with the 332 red area (and drop the green inequality).} 332 red area (and drop the green inequality). You can also think of it as 333 taking the stricter equality of the two.} 333 334 \end{frame} 334 335 … … 371 372 is irrelevant.}} 372 373 \only<2>{\fullframegraph{Normalising Inequalities}{inequality-tightening-2} 373 \note{We can eliminate this wastefulness by effectively "snap (削除) (削除ここまで)-to-grid". We374 \note{We can eliminate this wastefulness by effectively "snap(追記) ping (追記ここまで)-to-grid". We 374 375 move the inequality in a direction perpendicular to its line (informally, 375 (削除) "towards the red") until it hits (削除ここまで)the first cross(es). This is now shown376 (追記) ``towards the rest of the red region'') until it ``hits'' (追記ここまで) the first cross(es). This is now shown 376 377 on the graph.}} 377 378 \only<3>{\fullframegraph{Normalising Inequalities}{inequality-tightening-3}} … … 422 423 \only<2>{\fullframegraph{Eliminate $x$}{inequality-scalene-4}} 423 424 \only<3>{\fullframegraph{Eliminate $x$}{inequality-scalene-5} 424 \note{Similarly, in order for a point to be in both the re (削除) a (削除ここまで)d and425 \note{Similarly, in order for a point to be in both the re(追記) (追記ここまで)d and 425 426 blue regions, it must be above ($y$ axis again) the point at which 426 427 they join ($y=1$). Therefore our new inequality is $y \geq 1$. This … … 453 454 \text{\textcolor{KentRed}{Red}}\wedge\text{\textcolor{KentBlue}{Blue}:} & 10 - 4y &\leq 2x \leq 7 - y \implies &y \geq 1 454 455 \end{array}$ 456 (追記) (追記ここまで) 457 (追記) \note{This is an example/preview of the more detailed method to come. (追記ここまで) 458 (追記) But briefly: we arrange each inequality to be in terms of a positive (追記ここまで) 459 (追記) multiple of $x,ドル then cross-multiply, join the inequalities together (追記ここまで) 460 (追記) and remove the central item involving $x$. Much more details follow.} (追記ここまで) 455 461 456 462 \end{frame} … … 479 485 %N.B. $a > 0,ドル $b > 0$ 480 486 487 (追記) \only<2>{\note{ (追記ここまで) 488 (追記) We classify the inequalities with regards to the sign of the coefficient (追記ここまで) 489 (追記) of the variable we are looking to eliminate. We rearrange the inequality (追記ここまで) 490 (追記) so that on one side we have a positive multiple of $x_n,ドル and everything else (追記ここまで) 491 (追記) on the other side. Thus the sign determines whether we have a lower or (追記ここまで) 492 (追記) upper bound for $x_n$. (追記ここまで) 493 (追記) }} (追記ここまで) 494 (追記) (追記ここまで) 481 495 \end{frame} 482 496 … … 501 515 otherwise it would screw up the inequalities (multiplying 502 516 an inequality by a negative number reverses the direction 503 of the inequality) (削除) (削除ここまで)}517 of the inequality)(追記) . (追記ここまで)} 504 518 505 519 … … 531 545 the equation is solveable.} 532 546 533 (削除) (削除ここまで)\note{534 (削除) (削除ここまで)\begin{itemize}535 (削除) (削除ここまで)\item Set of constraints $C_R$ ($a\beta \leq b\alpha$ for all pairs) is real shadow of constraints $C$536 537 % (削除) (削除ここまで)New slide:538 (削除) (削除ここまで)\item No integer solution to $C_R$ $\implies$ no integer solution to $C$539 (削除) (削除ここまで)\item Integer solution to $C_R$ $\land$ no integer solution to $C$ $\implies$ $(\lnot \exists x: a\beta \leq abx \leq b\alpha)$540 (削除) (削除ここまで)\item $\therefore$ Integer solution to $C_R$ $\land (\exists x: a\beta \leq abx \leq b\alpha) \implies $ integer solution to $C$541 (削除) (削除ここまで)\end{itemize}542 (削除) (削除ここまで)}547 (追記) % (追記ここまで)\note{ 548 (追記) % (追記ここまで)\begin{itemize} 549 (追記) % (追記ここまで)\item Set of constraints $C_R$ ($a\beta \leq b\alpha$ for all pairs) is real shadow of constraints $C$ 550 % 551 %(追記) % (追記ここまで)New slide: 552 (追記) % (追記ここまで)\item No integer solution to $C_R$ $\implies$ no integer solution to $C$ 553 (追記) % (追記ここまで)\item Integer solution to $C_R$ $\land$ no integer solution to $C$ $\implies$ $(\lnot \exists x: a\beta \leq abx \leq b\alpha)$ 554 (追記) % (追記ここまで)\item $\therefore$ Integer solution to $C_R$ $\land (\exists x: a\beta \leq abx \leq b\alpha) \implies $ integer solution to $C$ 555 (追記) % (追記ここまで)\end{itemize} 556 (追記) % (追記ここまで)} 543 557 544 558 \end{frame} … … 549 563 %\end{itemize} 550 564 %$\operatorname{hasIntSol}(C_R) \land \lnot \operatorname{hasIntSol}(C) \implies (\lnot \exists x: a\beta \leq abx \leq b\alpha)$ 551 (削除) \note{Using (削除ここまで):552 (削除) (削除ここまで)553 (削除) (削除ここまで)$(A \land \lnot B) \implies C$554 (削除) (削除ここまで)555 (削除) (削除ここまで)$\lnot (A \land \lnot B) \lor C$ (by definition)556 (削除) (削除ここまで)557 (削除) (削除ここまで)$(\lnot A \lor B) \lor C$ (De Morgan's Law)558 (削除) (削除ここまで)559 (削除) (削除ここまで)$(\lnot A \lor C) \lor B$ (Distributivity of Or)560 (削除) (削除ここまで)561 (削除) (削除ここまで)$\lnot (A \land \lnot C) \lor B$ (De Morgan's Law)562 (削除) (削除ここまで)563 (削除) (削除ここまで)$(A \land \lnot C) \implies B$ (by definition)564 (削除) (削除ここまで)}565 (追記) %\note{Last bullet point uses (追記ここまで): 566 (追記) % (追記ここまで) 567 (追記) % (追記ここまで) $(A \land \lnot B) \implies C$ 568 (追記) % (追記ここまで) 569 (追記) % (追記ここまで) $\lnot (A \land \lnot B) \lor C$ (by definition) 570 (追記) % (追記ここまで) 571 (追記) % (追記ここまで) $(\lnot A \lor B) \lor C$ (De Morgan's Law) 572 (追記) % (追記ここまで) 573 (追記) % (追記ここまで) $(\lnot A \lor C) \lor B$ (Distributivity of Or) 574 (追記) % (追記ここまで) 575 (追記) % (追記ここまで) $\lnot (A \land \lnot C) \lor B$ (De Morgan's Law) 576 (追記) % (追記ここまで) 577 (追記) % (追記ここまで) $(A \land \lnot C) \implies B$ (by definition) 578 (追記) % (追記ここまで)} 565 579 %$\operatorname{hasIntSol}(C_R) \land (\exists x: a\beta \leq abx \leq b\alpha) \implies \operatorname{hasIntSol}(C)$ 566 580 … … 600 614 601 615 \only<4>{ 602 \note{ We now translate this greater-than back into a greater-than-or-equal-to.} 616 \note{ We now translate this greater-than back into a greater-than-or-equal-to and factor. 617 The last bullet is pointing out that if $a = 0$ or $b = 0,ドル the `dark' constraint 618 will be the same as the `real' constraint. If this is the case across all 619 bounds (which requires that either the coefficient in all upper bounds is one, 620 or the coefficient in all lower bounds is one), $C_D = C_R,ドル which is termed 621 an exact projection, and you can proceed solving this one problem. 622 } 603 623 } 604 624 \only<4> … … 672 692 \item $C_R$ is the real shadow of $C$ (variable removed) 673 693 \item $C_D$ is the dark shadow of $C$ (window large enough) 674 \only<2>{ \note{ 675 $(C_R = C_D) \implies (\operatorname{hasIntSol}(C) \iff \operatorname{hasIntSol}(C_R))$ 676 $\lnot \operatorname{hasIntSol}(C_R) \implies \lnot \operatorname{hasIntSol}(C)$ 677 $\operatorname{hasIntSol}(C_R) \land \operatorname{hasIntSol}(C_D) \implies \operatorname{hasIntSol}(C)$ 678 If $\operatorname{hasIntSol}(C_R) \wedge \neg \operatorname{hasIntSol}(C_D) \wedge (C_R \neq C_D),ドル we can't yet tell the value of $\operatorname{hasIntSol}(C)$ 694 \only<4>{ \note{ 695 The logical formulae this table is derived from: 696 \begin{itemize} 697 \item $(C_R = C_D) \implies (\operatorname{hasIntSol}(C) \iff \operatorname{hasIntSol}(C_R))$ 698 \item $\lnot \operatorname{hasIntSol}(C_R) \implies \lnot \operatorname{hasIntSol}(C)$ 699 \item $\operatorname{hasIntSol}(C_R) \land \operatorname{hasIntSol}(C_D) \implies \operatorname{hasIntSol}(C)$ 700 \end{itemize} 701 If $\operatorname{hasIntSol}(C_R) \wedge \neg \operatorname{hasIntSol}(C_D) \wedge (C_R \neq C_D),ドル we can't yet tell the value of $\operatorname{hasIntSol}(C)$ (the difficult case). 679 702 } } 680 703 \end{itemize} … … 726 749 \end{itemize} 727 750 \end{itemize} 751 (追記) (追記ここまで) 752 (追記) \note{ According to the Omega Test paper, you take the (single) highest value of (追記ここまで) 753 (追記) $a$ from the upper bounds, and pair it with each value of $b$ from the (追記ここまで) 754 (追記) lower bounds. So you will end up with $a \times \operatorname{avg}(b)$ new Omega Tests to run! (追記ここまで) 755 (追記) (追記ここまで) 756 (追記) Thankfully, this step is very rarely needed. (追記ここまで) 757 (追記) } (追記ここまで) 728 758 \end{frame} 729 759
Note:
See TracChangeset
for help on using the changeset viewer.