06.28.06
Take the Lead
Plot Outline:The real story of a dance teacher who believed in the talent of a group of problem kids.
Personal Comments:
The main reason why I went to see this movie is because it’s about dancing and Banderas seemed a very nice choice due to its latino vein. Still, it’s not a great dancing movie. I wouldn’t dare compare it with Dirty Dancing, Dirty Dancing II or Shall We Dance or some other nice titles. There are not many great dancing steps, in my oppinion. Still, due to the fact that’s a real story with a very nice plot around it, I do recommend it. However, if you really only wish to see some nice dancing moves, try another one…
06.20.06
The Island
Plot Outline:A man (Ewan McGregor) goes on the run after he discovers that he is actually a “harvested being”, and is being kept along with others in a utopian facility.
Personal Comments:
The movie is overall very nice. I rented it some time ago and the review was waiting on my post stack… Finally, here it is.
The plot is, I think, quite different of what we are used to. Some action mixed with Sci-Fi and some political/ethical questions on cloning and human harvesting. I like this… it is surely a very nice spent afternoon in front of the TV.
Mission: Impossible III
Plot Outline:Super-spy Ethan Hunt (Tom Cruise) has retired from active duty to trains new IMF agents. But he is called back into action to confront the toughest villain he’s ever faced – Owen Davian (Philip Seymour Hoffman), an international weapons and information provider with no remorse and no conscience. Hunt assembles his team – his old friend Luther Strickell (Ving Rhames), transportation expert Declan (Jonathan Rhys Meyers), and background operative Zhen (Maggie Q), to rescue one of his very own trainees, Lindsey (Keri Russell) who was kidnapped while on a surveillance detail of Davian. It soon becomes evident that Davian is well-protected, well-connected, and downright malicious, forcing Hunt to extend his journey back into the field in order to rescue his wife, Julia (Michelle Monaghan), and uncover IMF double agents in the process.
Personal Comments:
I went to the cinema on Sunday afternoon alone so I needed something strong. This movie did the trick. It was full of action from minute one. The pace was incredible, and the images unbelievable. The movie was really very good. You don’t need to see the previous M.I. or even to like them before this one. This seems to be just a new start for MI-III. Really very good.
One thing left me wondering… How the hell Hunt’s wife in the end with about a 30 second tutorial on how to shoot a gun is able to kill 2 terrorists which were surely much more experienced in killing than she was… Well, this was the only goof I found. But no problem, we forgive the director. The movie is great!
SMT for everyone…
or SMT in 20 minutes!
The Beginning
In fact, this is my attempt to create a SMT tutorial, which everyone is able to grasp. In fact, the only requirement is basic knowledge of Mathematics and basic knowledge of the English language.
This tutorial will serve as an anchor to everyone which will, in the future, ask me what is my research all about. If you asked me that recently, then that’s why I told you to come here. It will be brief and simple but at least you’ll understand what I’m currently working on, from a non-specific point of view. From a specific point of view I’d have to write a tutorial on “Architectural Design for Lazy SMT Multi-Theory Solvers in 2 years” or something! (Yes, I tried to find a very complex title just for the fun of it…) :-)
Propositional Logic
OK, so, yesterday I went to the beach and to the cinema. Note that although, yesterday I went to the cinema, I did not went to the beach (which was a pity), but anyway, the sentence is false! For it to be true, I had to go both to the cinema and to the beach, i.e. both conditions had to be true. This is intuitive, right?
If had used an or I would have said tommorrow I will go to the beach or to the cinema. If I happen to go to one, or both of those places the sentence is true, otherwise, i.e. I go neither to the beach nor the cinema tommorrow, it is false. Note that usually in current speech when we say this or that, we mean one thing or the other but not both. In mathematics, this is not the case. An or is true whenever one or both things happen. The kind of or we usually use in current speech is known as xor (which stands for exclusive or).
We can instead of using sentences, which have a true of false value, use letters for variables which can have true of false values depending on their meaning. So, briefly, A or B is false if both A is false and B is false but true otherwise. A and B is true if A is true and B is true and false otherwise. Note that we can define the and in terms of the or and vice-versa. We also have the negation (not) operator ~. ~A is false if A is true and true otherwise. We can define many other operators in terms of these, like implication (If this then that), equivalence (this if and only if that), exclusive or (this or that but not both), and so on.. In practice, we can translate a sentence with a lot of operators into a sentence which maintains it’s truthness (it’s value of true of false) with only ands, ors and nots.
The truth value of a sentence depends usually on its variables:
(A or ~(B and C)) cannot be said true of false. It depends on the values for the variables. If I tell you that A is false, B is false and C is false then you can say that the sentence is true. Note that we do not always need to specify the values of all the variables in the sentence to know the sentence value. If I say that A is true, no matter the values of B and C, the sentence is true. However, there are (evil) sentences which are false no matter what (kind’a like some people). For example, (A and ~A). There are obviously some which are true no matter what, (A or ~A).
Now, imagine that I give you the formula:
~(A or (B and ~A)) and ~(~B and A)
Now, can you find values for this sentence which makes it true, or is it always false?
(… trumpets …)
Ah, you’re trying to solve the SAT(isfiability) problem for that sentence. The formula is satisfiable if there are some values to the variables in the sentence (which we usually call formula) which make it true. If the formula is false no matter what, we say that the formula is unsatisfiable.
Who would imagine that this is one of the major problems in Computer Science? And it turns out to be pretty hard (which is fortunate since it turns out to employ a lot of colleagues of mine).
So, now, if someone tells you that it is working on SAT, you should say: “Ah, that’s nice!” instead of “Huh? What’s that?” and imagine that same person day after day trying to find new ways to solve this problem as fast as possible for huge formulas. Humm, so, let me give you an idea… Imagine that I write the formula on one straight line, in toilet paper, where a character is square and takes up the whole height of the toilet paper. Then, you would need about 180Km of toilet paper to write the whole formula… and that’s what I mean by huge.
Since, a lot of development has been done in SAT recently, there are a lot of people translating their problems in to SAT so that they are able to solve them using current efficient SAT solvers.
Adding a Mathematical Component
Problem is… there are problems which are not easily translated into SAT since they have inherently mathematical contraints which are hard to translate to SAT under certain circunstances. So, people decided to extend the SAT are to what is currently known as the SAT Modulo Theories (SMT) problem.
Now, in place of formulas like the ones in the last section which are composed of variables which are true or false, you can also have mathematical constraints like 2x + 3y >= 4, or f(a) – f(b) = 2, or even a[2] > 5.
What happened is that we substituted the Boolean variables (variables which can only have true or false values) into more complex expression, but otherwise more expressive which still have themselves a Boolean value. These expressions can belong to any decidable theory, linear arithmetic, uninterpreted functions and theory of arrays respectively (from the examples above).
So, the SMT formula syntax depends on the background theory (or theories) we are considering. If we consider Integer Linear Arithmetic, (x + 2y >= 3 and x < 3) or B is correct if the x,y are integers but is not correct if we consider Integer Difference Logic.
Now, we can use mix the theories and the expressions, generate arbitrarily large formulas to solve specific problems and check for their satisfiability like we did for SAT. In SAT we would search for a solution and if one existed we could output a value find for each of the variables which makes the formula true (satisfies the formula), and these values would be Boolean. Now, the values can be integer, real, Boolean, whatever.
The requirement is that the main underlying logic of these formulas is a many-sorted version of first order logic, which still leaves us the possibility of adding quantifiers but I think there are still few those who are working on Quantified SMT formulas.
Guess what? You can easily translate a Sudoku problem to SMT (which can be done to SAT, but not easily and not so intuitively)… you can also translate thousands of other (more practicaly interesting) problems to SMT. The translation, technically called encoding is also studied by some since the way you encode the problem strongly influences how easy it’ll be to solve.
Well, I think this is it for now… Hope you are SATisfied with this brief tutorial!
Pointers:
- SAT on MathWorld
- SAT on Wikipedia
- SAT Live! : Somewhere where you can find the latest news on SAT.
- SATLIB : Library of SAT benchmarks.
- Journal on Satisfiability
- SMTLIB : Library of SMT benchmarks.
06.16.06
Imposto Municipal sobre Veículos… ONLINE!
É possível a partir de hoje e até dia 16 de Julho pagar online o Imposto Municipal sobre Veículos, aka Selo Automóvel.
Existe um “catch” para quem tentar fazer isto… aliás… mais do que um, mas aquele a que me refiro fez-me anular 3 vezes o pedido de pagamento. Bom, basicamente, tem-se um login (se não se tem, pede-se e a password é enviada para o endereço fiscal), e entra-se. Faz-se o pedido de pagamento e o que eles dão é uma guia de pagamento… Que desilusão! Isto porque eu pensava que tinham mesmo implementado um sistema de pagamentos online. Mas não, ou se tem outra forma de fazer o pagamento online, através do banco online, ou tem de se levar a guia a um sitio qualquer para realizar o pagamento. Ora, felizmente tenho banco online mas até conseguir ver a guia…
Tudo deve funcionar muito bem no Windows (imagino), no Linux a coisa pia mais fino. Se usarmos o Firefox 1.5, este apanha logo o pop-up e bloqueia-o. Depois de o desbloquear aparece uma janela com o download de um ficheiro PDF mas com o nome de externalBinary.jsp. Este ficheiro é o PDF. Quando se tenta abrir com o gv (que é o que eu regularmente uso) dá erro! O problema não é do ficheiro PDF per se, mas sim de alguma coisa que o ficheiro contém que dá cabo do software. Assim, tentem abrir com o kpdf que funciona (ou o Acrobat Reader, mas eu não gosto muito dele). De mencionar que o konqueror funciona bem com a página do ministério das finanças e percebe logo que externalBinary.jsp é PDF e abre-o com o kpdf. O PDF não contém mais que uma referência para depois no banco online se introduzir em Pagamentos ao Estado.
Bom, a experiência foi engraçada. Resta esperar que o dístico chegue a casa… mas eles deixam-nos logo de sobreaviso. Se o dístico não chegar é porque se extraviou e teremos então que pagar a respectiva multa…
06.14.06
The Chain Rule… inside out!
The Chain Rule is definitely an extremely useful tool, whether you’re working in single-variable calculus or multi-variable calculus. Since I had some fun with it today I’ll give a brief explanation here today… hopefully I’ll help someone in the future!
Chain Rule for single-variable functions ([tex]f : \mathbb{R} \rightarrow \mathbb{R}[/tex])
This is the simplest case and in fact to understand the rule for the general case you should start here.
Basically consider [tex]g = f(r(t))[/tex], so we simply have [tex]g’(t) = f’(r(t)) \cdot r’(t)[/tex].
As an example, consider:
[tex]f(x) = 1/x[/tex] and,
[tex]r(t) = t^2, t \neq 0 [/tex].
So if we wish to compute the derivative of [tex]g(t) = f(r(t))[/tex], we just need to apply the chain rule above:
[tex]g’(t) = f’(r(t)) \cdot r’(t) = [/tex]
[tex] = f’(t^2) \cdot 2t = [/tex]
[tex] = -1/(t^2) \cdot 2t = \frac{-2t}{t^2} = \frac{-2}{t} [/tex]
I left the obvious part unmentioned (the why I had to restrict [tex]r[/tex]). Since, [tex]D_f = ]-\infty, 0[ \cup ]0, +\infty[ [/tex] and [tex]D^’_g = \mathbb{R}[/tex], this is only valid if we restrict [tex]r[/tex].
Now, onto a more general case.
Chain Rule for multi-variable functions ([tex]f : \mathbb{R}^n \rightarrow \mathbb{R}[/tex])
So, given a scalar field defined on an open set [tex]S[/tex] in [tex]\mathbb{R}^n[/tex], and let [tex]r[/tex] be a vector-valued function which maps an interval J from [tex]\mathbb{R}^1[/tex] into [tex]S[/tex]. Define the composite function [tex]g = f \circ r[/tex] on [tex]J[/tex] by the equation:
[tex]g(t) = f[r(t)][/tex] if [tex]t \in J[/tex]
Let [tex]t[/tex] be a point in [tex]J[/tex] at which [tex]r’(t)[/tex] exists and assume that [tex]f[/tex] is differenciable at [tex]r(t)[/tex]. Then [tex]g’(t)[/tex] exists and is equal to the dot product:
[tex]g’(t) = \nabla f(a) \cdot r’(t)[/tex], where [tex]a = r(t)[/tex]
Note that [tex]\nabla f(a)[/tex] known as the gradient of [tex]f[/tex] at [tex]a[/tex] is the vector whose components are the partial derivatives of [tex]f[/tex] at [tex]a[/tex]:
[tex]\nabla f(a) = (D_1 f(a), \ldots, D_n f(a))[/tex]
So, [tex]\nabla f(a)[/tex] is a vector field defined at each point [tex]a[/tex] where the partial derivatives [tex]D_1 f(a), \ldots, D_n f(a)[/tex] exist.
Consider that [tex]F = f \circ r[/tex] and as we have been considering in this section [tex]f : \mathbb{R}^2 \rightarrow \mathbb{R}[/tex] and [tex]r : \mathbb{R} \rightarrow \mathbb{R}^2[/tex], so we have that [tex]F : \mathbb{R} \rightarrow \mathbb{R}[/tex]. They are given by [tex]f(x, y) = x^2 + y^2, r(t) = (t, t^2)[/tex] and let’s compute [tex]F’(t), F”(t)[/tex].
By using the chain rule we have: [tex]F’(t) = \nabla f(r(t)) \cdot r’(t)[/tex]. So,
[tex]\nabla f = \left(\frac{\partial f}{\partial x}, \frac{\partial f}{\partial y}\right) = (2x, 2y)[/tex] and
[tex]r’(t) = (1, t^2)[/tex]
Substituting in the chain rule:
[tex]F’(t) = \nabla f(r(t)) \cdot r’(t) = [/tex]
[tex] = (2t, 2t^2) \cdot (1, 2t) = [/tex]
[tex] = 2t + 4t^3 [/tex]
And trivially, we need no chain rule for the second derivative: [tex]F”(t) = [F'(t)]‘ = 12t^2+2 [/tex].
In general, the chain rule for multi-variable vector fields ([tex]f : \mathbb{R}^n \rightarrow \mathbb{R}^m[/tex])
Now, let’s look at the general case when we have vector fields.
Chain Rule: Let [tex]f[/tex], and [tex]g[/tex] be vector fields such that the composition [tex]h = f \circ g[/tex] is defined in a neighborhood of a point [tex]a[/tex]. Assume that [tex]g[/tex] is differentiable at [tex]a[/tex], with total derivative [tex]g’(a)[/tex]. Let [tex]b = g(a)[/tex] and assume that [tex]f[/tex] is differentiable at [tex]b[/tex], with total derivative [tex]f’(b)[/tex]. Then [tex]h[/tex] is differentiable at [tex]a[/tex], and the total derivative [tex]h’(a)[/tex] is given by:
[tex]h’(a) = f’(b) \circ g’(a)[/tex],
the composition of the linear transformations [tex]f’(b)[/tex] and [tex]g’(a)[/tex].
Note that the derivatives of vector fields are given by their respective jacobian matrices and that the composition of the linear transformation is obtained by the multiplication of the jacobian matrices (which represent the linear transformations).
Ok, so let’s try to do a complete exercise (since officially, or from a theoretical point-of-view, we already know how to do it).
Given:
[tex]f: \mathbb{R}^2 \rightarrow \mathbb{R}^2[/tex]
[tex]f(x, y) = (e^{x+2y}, \sin(y+2x))[/tex]
[tex]g: \mathbb{R}^3 \rightarrow \mathbb{R}^2[/tex]
[tex]g(u,v,w) = (u + 2v^2 + 3w^3, 2v-u^2)[/tex]
Let’s compute the jacobian matrices of [tex]f[/tex] and [tex]g[/tex]:
[tex]D_f = \begin{pmatrix} \frac{\partial f_1}{\partial x} & \frac{\partial f_1}{\partial y} \\ \frac{\partial f_2}{\partial x} & \frac{\partial f_2}{\partial y} \end{pmatrix} = [/tex]
[tex] = \begin{pmatrix} e^{x+2y} & 2e^{x+2y} \\ 2\cos(y+2x) & \cos(y+2x) \end{pmatrix}[/tex]
[tex]D_g = \begin{pmatrix}\frac{\partial g_1}{\partial u} & \frac{\partial g_1}{\partial v} & \frac{\partial g_1}{\partial w}\\ \frac{\partial g_2}{\partial u} & \frac{\partial g_2}{\partial v} & \frac{\partial g_2}{\partial w}\end{pmatrix} = [/tex]
[tex] = \begin{pmatrix}1 & 4v & 9w^2 \\ -2u & 2 & 0 \end{pmatrix}[/tex]
Now, define [tex]h(u,v,w) = f(g(u,v,w))[/tex] and compute [tex]D_h(1,-1,1)[/tex]. Well, well… here’s the application of our chain rule. So, by the chain rule:
[tex]h(1,-1,1) = f’(g(1,-1,1)) \circ g’(1,-1,1)[/tex]
By substitution in the expression:
[tex]g(1,-1,1) = (1+2+3, -2-1) = (6,-3)[/tex]
By substituting in the jacobian matrix computed previously for [tex]f[/tex] the value of [tex]g(1,-1,1)[/tex]:
[tex]f’(g(1,-1,1)) = f’(6,3) = \begin{pmatrix} 1 & 2 \\ 2\cos(9) & \cos(9) \end{pmatrix}[/tex]
By substituting in the jacobian matrix computed previously for [tex]g[/tex]:
[tex]g’(1,-1,1) = \begin{pmatrix} 1 & -4 & 9 \\ -2 & 2 & 0 \end{pmatrix}[/tex]
Now that we have computed all the values needed for the chain rule application, applying it is just composing the linear transformations given by the derivatives of [tex]f[/tex] and [tex]g[/tex], which is another way of saying that we need to multiply their jacobian matrices:
[tex]h’(1,-1,1) = \begin{pmatrix} 1 & 2 \\ 2\cos(9) & \cos(9) \end{pmatrix} \cdot \begin{pmatrix} 1 & -4 & 9 \\ -2 & 2 & 0 \end{pmatrix} = [/tex]
[tex] = \begin{pmatrix}-3 & 0 & 9 \\ 0 & -6\cos(9) & 18\cos(9) \end{pmatrix}[/tex]
And we’re done… :-)
Computing Jacobian’s and working with these kinds of tools are extremelly helpful in Geometry, Differential Calculus and some branches of Physics.
References:
- Weisstein, Eric W. “Chain Rule.” From MathWorld–A Wolfram Web Resource. http://mathworld.wolfram.com/ChainRule.html
- Apostol, Tom “Calculus”, Volume II, Second Edition
- Anton, Bivens and Davis, Calculus, Seventh Edition
06.11.06
Menos ais…
Incrível é como todo Portugal passa semanas antes do campeonato a cantar em uníssono “Menos ais” e a nossa selecção faz uma exibição tão fraca frente a Angola. Para além das faltas desnecessárias existiu pelo menos uma simulação de falta por parte da nossa selecção o que é tudo menos admissível. Angola jogou acima do nível que esperávamos e por isso devemos-lhe tirar o chapeu. No entanto, não conseguiu empatar. Apesar de tudo, no final de tão pobre exibição penso que seria justo empatarmos a 1 com Angola. Portugal não mereceu a vitória e se não abrir os olhos dentro de pouco tempo temos a nossa selecção de volta a Portugal. Tanta coisa, tanta bandeira e cantoria… os portugueses tentam mostrar-se alegres com o futebol para camuflar o resto da desgraça nacional, no entanto, ou a nossa selecção melhora a sua “performance” ou a desgraça é geral! Parabéns a ambas as equipas mas considero que teria sido pedagógico que a selecção Portuguesa tivesse empatado frente a Angola…
“Scheme Slides 101″ slides are online!
Last May 4th, I’ve given a presentation for the Lisp group at my University, the Lispnicks. From a mostly Common Lisp background I tried to introduce to them how to create presentations using PLT Scheme tools. The slides are finally online in PDF and a tar.bz2 archive containing all the source code, images and the generated pdf for those wanting to check out the source. You can use it in any way you want. Have fun! The code may not be properly commented but contact me if you need help with something. I’ve been doing presentations in PLT Scheme since 2004 and I have a lot of presentation code which I can put online but due to lazyness and lack of time I have been keeping it to myself. Hopefully, in short-term, I’ll put them all online in my webpage and will announce it here.
Now, that’s omni-presence…
Just a happy announcement that I’m now, on two planets at the same time. :-) I’m living on both at the same time. P* and Planet Scheme. For those interested in Scheme, you should definitely read Planet Scheme and if you happen to write about it, contact Jens Axel Soegaard and ask for a ticket into the planet!
Crash
Plot Outline:Several stories interweave during two days in Los Angeles involving a collection of inter-related characters, a black police detective with a drugged out mother and a thieving younger brother, two car thieves who are constantly theorizing on society and race, the distracted district attorney and his irritated and pampered wife, a racist veteran cop (caring for a sick father at home) who disgusts his more idealistic younger partner, a successful black Hollywood director and his wife who must deal with racist cop, a Persian-immigrant father who buys a gun to protect his shop, a Hispanic locksmith and his young daughter who is afraid of bullets, and more.
Personal Comments:
Since the latest Oscars I’ve been willing to watch this movie so I rented it a couple days ago and I must say the film is good. Still, there was in my oppinion too much turbulence due to it. The movie surrounds the racism subject and all sorts of racism happens during the all movie. It is somewhat heavy and sometimes probably even confusing. Still, I must say that I was somewhat disappointed, probably because I was expecting something really great. The movie is just good, not great! But it was not a waste…
