SMT Solvers

Satisfiability Modulo Theory problems were introduced in my sphere of interest lately as I need to find a way to check whether a set of constraints remains satisfiable when new constraints are added.

What is an SMTproblem? It is a problem that includes a set of expressions (like inequalities between symbols and numbers) that needs estimation on whether it is satisfiable or not. That means whether there is a set of values for the variables that appear in the expressions that make all the expressions true at the same time. If there is then the set is satisfiable, if not then the set is unsatisfiable.

At this case it would be good to make a distinction between satisfiability and validity. Valid is an expression that is always true independent of the values that its variables will take. An expression is satisfiable when there is at least a combination of the variables that makes it true. It is easy to see that:

P is valid when not P is not satisfiable.

and

P is satisfiable if and only if not P is not valid.

As an SMT solver can check for satisfiability, it can also check for validity by checking the satisfiability of the opposite expression! (It blew my mind when I realized that).

So I was looking for a tool that could do all this maths for me, automatically, for any instance of my problems that I could feed it and thus I searched for an SMT solver. I found many descent ones like the following:

OpenSMT: Is an open SMT solver. It can be integrated with other projects.

STP Contraint solver: Is a constraint solver that has been developed in MIT.

CVC4: Is a solver that seems to be vibrant. There have been previous versions like CVC, CVC Lite, CVC3 but the project claims that despite a successor it is code independent from the previous ones.\

Z3: Is a solver developed by Microsoft Research which by the way seems to be doing great research on automatic theorem proving (for further information you can check the Coq proof assistant that is an advanced theorem proover under development). Although I have no specific criteria yet I chose to work with this one initially because of the support of many platforms (windows and linux (well and OSX but I don’t use it)) and the support of many input formats (more on that later).

Other that I found but had no lack in checking out were:

Yices,SMT-RAT,Mini-SAT and there are plenty more in the wikipedia page for SMT solvers.

A good thing here is to mention the difference on SAT solvers and SMT solvers:

SAT solvers use only boolean expressions in contrast with the SMT that uses integers. The expressions that can be used are either inequalities or equalities between unknown functions. A SMT solver can be implemented as a transformer to a boolean representation of the problem and then a solution using an SAT solver like BASolver. This is actually used by it has its drawbacks thus there are native SMT solvers too.

All these solver get a set of expressions and check whether they are satisfiable or not. This input can be expressed in a variety of ways with the most prominent being the following:

SMT-LIB v1.x – v2.0: Is a library that is being created from 2003 in an attempt to formalize the domain. It seemed to me most satisfactory to use thus I chose to use it.
SATLIB – The Satisfiability Library: Is the equivalent library for SAT problems. It introduces the DIMACS input style.
CVC: It is a style used by the CVC solver (and some others too).

Note: Not all solvers support all available formats.
I found a couple more that I won’t mention as I did not find any documentation on them.

Moderncv LaTeX package. A really easy way to create a modern CV

As far as the options are concerned these are the following:

I had created my CV many months ago and I put it in good use, I found a PhD position. However I was still meddling with my girlfriend’s CV as she is looking for a job. So I came up with moderncv package that provides a way to easily create a really nice proffesional CV.

You can install the moderncv package manually after downloading it from CTAN directory or if you use MiKTeK like I do, you can go to the package manager search for moderncv package and install it. However I pretty sure that by default MiKTeK prompts you to download any missing packages.

To use moderncv you simply use:

\documentclass[11pt,a4paper]{moderncv}


and you set the CV theme that you want to create:


\moderncvtheme[options]{theme}


Where theme you can have casual, classic and empty:

Casual is a resume created with a simple header on the first page with the name and a picture. Information of the address, telephone number and email is placed in the bottom of each page of the CV.

Classic creates a full header with name, information and passport image on the first page. There is no information on the footer of each page. I recommend this on for most professional uses.

Empty creates a very simple moderncv resume without headers and footers.

As far as the options are concerned these are the following: blue, orange, green, red, purple, grey  (which are to choose the color of the cv lines and roman to use roman fonts instead of sans serif fonts.
Then you continue writing down your personal data using:

\firstname {name}    % Your name
\lastname {Last name} % Your last name
\title {Title}              % Your title (optional)
\mobile {number}    % Your mobile phone number
\phone {number}    % Your phone number
\extrainfo {information} % Possible extra information e.g. website
\quote {quote} % Life motto or something like that (optional)


These are used with the \maketitle command. Further more the moderncv had some structures that can be used to enter your skills and qualities. Some of these are:

\cventry{year--year}{Degree}{Institution}{City}{\textit{Grade}}{Description}
\cvlanguage{Language 1}{Skill level}{Comment}
\cvcomputer{category 1}{XXX, YYY, ZZZ}{category 4}{XXX, YYY, ZZZ}
\cvline{hobby 1}{\small Description}


cventry is used to enter education and work experience entries. cvlanguage to enter linguistic skills, cvcomputer computer skills. Finally cvline is used to enter generic information. More structures and information can be found in the templates code in the CTAN directory found here.

The results are the following:
Using [green]{classic}: pdf, tex
Using [blue]{casual}: pdf, tex
Using classic with photo: pdf

Sony VAIO bloatware list

After having to remove manually all the useless software preinstalled to my computer I decided that a list to remind what is useful and what’s not would be nice.

• Vaio Care – Recomended , maintenance tool
• Vaio Content Metadata Intelligent Analyzing Manager – Used for media library
• Vaio Content Metadata Intelligent Intelligent Network Service Manager – Used for media library
• Vaio Content Metadata Manager Settings – Used for media library
• Vaio Content Metadata XML Interface Settings – Used for media library
• Vaio Content Monitoring Settings – Used for media library
• Vaio Control Centre – Recommended, control panel for many useful things on the laptop
• Vaio CW screensaver – Media content
• Vaio Data Restore Tool – Software used to restore erased data
• Vaio DVD Menu Data – Software used to create DVD menus
• Vaio Entertainment Platform – Media
• Vaio Event Service – Recommended , makes all he extra buttons and the fn functions work
• Vaio Gate – The floating menu on top of screen
• Vaio Gate Default – Settings for Vaio gate
• Vaio Marketing Tools – Seems useless, I uninstalled
• Vaio Media Plus – Media
• Vaio Media Plus Opening Movie – Media
• Vaio Movie Story Template Data – Media
• Vaio Original Function Settings – Media
• Vaio Personalization Manager – Media
• Vaio Power Management – Recommended
• Vaio Premium Partners – SONY partners, uninstall
• Vaio Smart Network – Update: Recommended, Wireless devices manager
• Vaio Transfer Support – To transfer media among devices
• Vaio Update 5 – To update SONY software
• Vaio Wallpaper Contents – The wallpapers in the device

Personally I prefer to Unistall everything but:

• Vaio Care (useful)
• Vaio Power Management (useful)
• Vaio Control Center (useful)
• Vaio Event Service (essential)
• Vaio Wallpapers (because I like them)

I believe that the only thing essential is the Vaio event service. I used to keep vaio update but at some point it was installing some drivers for Playstation 3 controllers to the laptop and I find it really stupid to keep now. Also I remove McAfee, Norton, Arcsoft and any other software that may be there that I don’t use.

The above list is from a CW series VAIO. It is not complete as there are a couple more programs that I don’t mention (such us the media gallery, I think) because I don’t remember them and I don’t plan to recover the laptop to factory settings anytime soon, I just got it working! Hope that this is going to be helpful for many other trying to make their VAIO working machinery and not a digital playground of SONY crapware.

From Opera mail to Thunderbird

It has been more almost a year that I have been using Opera mail for my email needs. I must say that it is one of the best desktop mail implementations that I have used. However I wanted to have calendar and to do lists as well and Opera is not providing that in a convenient way.

Thus I was thinking of using Thunderbird (which I used before). I was thinking about the migration for weeks. There were features in Opera that I did not like to sacrifice. One of them is Opera Contacts. The way Opera lets you organize your contacts and view your mails by contact is something that I found very useful from time to time. Also using these little faces for each contact allowed me to identify the significance and the origin of a mail in a glimpse and that is something that I am going to miss. Plus it made my mail way more pleasant.

Till now I used calendar and to do lists using Rainlendar. Rainlendar is a really subtle program that used to decorate my empty desktop but I must admit it is not a good one to keep track of a to do list and calendar inputs. I never felt I was in control with it although using it is really straight forward. Thus I migrated my calendar and to do lists to Thunderbird. There the calendar is a bliss. Maybe it is not as good as Microsoft’s Outlook solution which might be the best in the domain but still really good. A note should be done here, I don’t want to use Outlook, I don’t feel confortable with it.

My first obstacle during the tranfer were the contacts. The Opera exports the contacts in .adr format which is an Opera specific format. It cannot be imported to Thunderbird directly (which is a same) and I had to use a converter found on here. The converter gets .adr files and exports .tab or .cvs (tab separated or comma separated contacts). Although the converter seems to be old (it mentions Opera 7) it worked just fine with my Opera 11.50 contacts. The problem with that is that any data I had on the contacts were lost apart from the name and the address. As Thunderbird contacts have many more fields available it did not bother me much. After a couple of hours most of my contacts were in good shape.

In an attempt to get those small faces that Opera uses I installed the Display Contact Photo Thunderbird add-on. However this only got me to have some more images to use that will be displayed only when I was to write a new mail. Not as helpful as I wanted it to be but I kept it.

In a second attempt to get the contacts on the side and trying to get access to the mails of single contact easily I tried to install Contacts Sidebar Thunderbird add-on only to find out that it is not compatible with Thunderbird 6… To cheer me up a bit I got a wood looking theme for the Thunderbird which I really liked.

However, there are still a couple of issues that I am going to try to resolve. These are the text wrapping of my mails that will render them more readable. This is a features that I have seen in mails that I receive. I suspect that it has something to do with Microsoft’s Outlook but I believe that there should be something that can be done about it in Thunderbird.

That is the good part of using Thunderbird. There is almost an add-on for anything that you can think off. However this may lead to a really slow experience using the application. so one must be careful.

Finally, Opera seems a bit barren now that I removed the mail from it. However it still has the feeds that I get there. I really like this browser and I plan to continue using it as it completely serves my needs.

Dynamic variable name change using Matlab

There are plenty of times in the past that I needed to store many different data srtuctures in different file names but I didn’t know the way to change the name of a variable during the execution of the code.

So now that I really needed to do so (storing 1500 different matrices one by one takes some time so naming them automatically while calculating them makes it much more efficient!) I searched the Matlab capabilities and found exactly what I was looking for!

Thus if for example you have table A and you want to store 10 different instances of the table like A_1 – A_10 then the eval() function is just what you need:

Here is the code that would do the trick:


for ii = 1 : 10
% Creating the filename
filename = [‘A_’ num2str(ii)];

% Creating the new variable name
varname = [‘A_’ num2str(ii)];

% calculating the new value of A
value = function();

% This is the instruction that will assign the value to A_ii
s = [‘A_’ num2str(ii) ‘= value ‘];

% Do not use eval with no reason because it is much slower than the normal assignment.
eval(s) ;

% Saving the result
save(filename,varname)
end

Now lets say that we have 10 .mat files that need to be read from (the A_1 – A_10) here is how to do it:

for ii = 1 : 10
end


Although the following might work as well:

for ii = 1 : 10
filename = [‘A_’ num2str(ii)]; % Creating the filename