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.


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.


Java API features: JMX, RMI and AspectJ

Lately I came across some Java features that I was not aware of.

First of all the JMX:

JMX stands for Java eXtention Management. It provides an API where using the concept of Java beans one can expose some information of the program under execution to other programs. So running a java application that uses Java Beans we can connect to that application using the Java Console (comes with the Java – I did not know about it either). With this connection one can see what resources the application is using as well check for exposed variables and methods. One can also change values or invoke methods and constructors using the jconsole! I got really excited about that.

Secondly the RMI:

The RMI API provides the Remote interface which can be used so that java applications can communicate with each other. With this API client – server application can be created which opens the filed for way more applications. Well I feel a bit stupid mentioning this feature of the RMI as I figure that someone taught Java properly will be aware of it and use it but I didn’t have such luck and here I stand impressed.

Last but not least AspectJ:

AspectJ is not an API that can be used with Java is more like a different programming language that can be used on top of it. AspectJ uses semantics that can identify existing code and either enhance it with additional code or change it and replace the code with something different. This kind of programming is called Aspect Oriented Programming and is becoming quite popular as there are many advantages to it. First of all on should not read all the code that is written to modify and change it. For example (this is what a beginner does for an exercise but I think captures much of the concept of Aspect Oriented Programming) if there is a huge application that needs logging mechanism one does need to go through the code and add the code for the logging manually. Simply add an AspectJ application that identifies method calls and class constructors and prints the desired information. So logging is added as an aspect (thus Aspect Oriented)

AspectJ identifies existing code through pointcuts which are specific parts of the code. So for example one can write an AspectJ application that identifies that everytime an access to a database is done for the first time by a user a login information is needed. So the lofin aspect aspect is implemented etc.

All the above can be combined and refined into Adaptive Computing. This means that one can develop a system that can get information from its self (JMX), remotely (RMI) and change it self (AspectJ). The possibilities are endless and the technology is already deployed in networks to handle server failures, overloads and mobile systems where a user changes access point unpredictably.

Tiddly Wikki–keeping notes offline

I really love Evernote. I have been using it for a couple of years now and it has been a really nice experience. Due to the nature of my work I cannot use it as I have restricted access to "file – sharing" sites like Evernote. As a consequence I had to find alternatives. So I remembered that I had stumbled upon an offline wiki called Tiddly Wiki. To use it is really straightforward. You download an empty.html and you store it wherever you want. This file will contain everything that you will need. To use it you just open it using your favorite browser.

So I use it in a flash drive and I back it up to my main file repository in a frequent basis. Other people combine it with dropbox (which is something I would have done if I had access to dropbox). One would say that this would be the equivalent of using Evernote – but the difference is that in the case of Tiddly Wiki we are platform independent.

Once the html file is downloaded we can proceed by setting some variables like the name of the wiki and the name of us as a user. All these (as well as other settings) are done through tiddlers. A tiddler is the equivalent to note/post for tiddly wiki. Some of them are special and are used to set parameters for your wiki (as already mentioned). Using such special tiddlers we can also customize the theme, many can be found in TiddlyThemes.

Apart from this one can find a vibrant community providing all sorts of plugins. Plugins are easy to use just by copying and pasting the code of the appropriate tiddlers to your own tiddly wiki. Links to plugins sites can be found to the main site of tiddly wiki.

Inside the content of a tiddler a basic annotation language is used similar to the one used in wikis and forums. Also code can be inserted and power users can experiment by developing their own plugins and themes. Setting links to websites or even local files is really easy which made it a plus for me that I use it in a flash drive.

So far I have found it really useful and I use it in a daily basis to keep log and other information that I need to carry around in a structured format. Have fun using it and don’t forget that any time you can get it online and use it in your website!

OpenGL in Java and game development

Recently I got my self into OpenGL. It is a graphics library that helps you use the 3D graphics hardware on your PC. It is open in comparison to DirectX and it is cross – platform. To see what you create you need to use some kind of a viewer. One that I tried lately is libQGLViewer which is based on Qt and can also be used across platforms although I had some trouble setting it up for windows.

libQGLViewer is nice but from my understanding supports only C++ so for me that I wanted to use Java with OpenGL I searched and found LWJGL which stands for LightWeight Java Gaming Library. This library helps use OpenGL in Java really easily. I used it with eclipse on windows without much trouble. However if you want to build a game out of it you’ll need some kind of game engine to display the graphics. Unless you want to build your own from scratch you’d better use one that is already available.

I found jMonkeyEngine really interesting. It provides a really nice engine along with a very good integrated development environment that apart from the coding part includes the graphics.

Along with programs like blender and GIMP I’m setting off to an exploration of the potential of game development. If you always wanted to make a game these are the tools just give them a try!

How to find a job

Well finding a job is not something that depends solely on yourself so there is no miracle algorithm that actually gets you one but this post aims at increasing the probabilities to get a vacancy that you desire.

Finding the vacancy in my opinion is not a big issue. There are plenty of sites that post positions, plenty of companies that you can track and lately many social networks help you get informed.

  1. Select target: I believe that applying in anything that moves is not the best strategy. You better apply to some of the positions (five to ten sounds a reasonable amount of applications) but each time you apply you need to make it right.
  2. Matchmaking: Don’t expect to be called for an interview if your CV is not looking right. Building a right CV is whole book of work to describe but a few tips are here:
    • Check what the job needs. make sure that you cover these needs clearly in your CV. You don’t need to lie (if you do you probably shouldn’t apply) but you can highlight skills and expertise that may not be your best assets.
    • Don’t fill in details. Long text is rarely read these days. Make short descriptive sentences and lists.This should do the trick.
    • Along with the CV you better write a cover letter that fits the vacancy.
    • This is also the reason you don’t want many interviews in the same time. If you need to study different things you don’t want to end up doing half – jobs for each one of them…
    • Being unemployed doesn’t mean that you don’t work. Keep a daily routine and fill your spare time enhancing those skills and features in your CV of yours.
  3. Prepare for interview: Before getting too an interview prepare your self. Do a quick study on the weak points and refresh your strong points (you don’t want to be asked something that you claim that you know and not remember it). In the interview you should have taken into account the following:
    • You are in need for a job but they also are in need for an employee so this is a two way dependency. If you have additional information you can know exactly why there is the particular opening and sell your self in the interview.
    • What are the skills that they really need from the new employee? If you lack experience you can always claim that it might not be needed. This applies to people who work for many years in the same position doing the same thing over and over. In that case 10 years of experience means 10 years the first year of experience.
    • Read carefully both the CV and the letter you have sent and the job offer. You should be able to talk about everything in these three.
    • They picked you for an interview which means that they liked what they saw in you CV or they have limited selection of people – both are good news for you!
  4. Know your self: This is something that one should do anyway. You should know your self. None of the above steps are applicable if you don’t really know what you want to do. So ask yourself, what do you want to do? What do you offer? Why you want the particular job vacancy?

You first need to convince yourself why you should be hired in order to convince other people to hire you! If you have enough knowledge of yourself on these matters then picking the right openings and answering the typical questions would be no big deal.

The above hints and tips are a way to build the self confidence that is needed to increase the acceptance probability when looking for a job. By no means there is any guarantee!

Hope these help.

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:


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


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)
\address{street and number}{post code and city} % Your current address
\mobile {number}    % Your mobile phone number
\phone {number}    % Your phone number
\email {email}          % Your email address
\homepage {link}    % Your website
\extrainfo {information} % Possible extra information e.g. website
\photo[64pt][0.4pt]{picture}  % Your photo (optional)
\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:

\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

Mind maps update: Blumind

As seen in my previous post (Mind Mapping) I have tested two programs for mind maps so far: Freemind and Xmind. I settled with Freemind for quite sometime mostly because of the lack of premium editions and internet dependability (accounts ,register etc) however I stumpled upon another freeware mind mapping software called blumind. I really enjoyed using it and the portability of the freeminfd maps made it easier for me to make the transition.
To sum up the programs I’ve tried so far are:

Xmind – link
Freemind – link
Blumind – link

Importing .mbs (Opera mail) to thunderbird

For some reason thunderbird still does not support an automatic way to import these .mbs files generated by Opera although it uses the format it self.

The procedure is quite simple and all you have to do is the following: First you have to find the folder where the mails are saved by thunderbird on your hard drive. That is on:

Tools->Account Settings->Local Folders->Local directory

By default this is:

C:\Users\<user_name>\AppData\Roaming\Thunderbird\Profiles\<random_sequence>.default\Mail\Local Folders

where <user_name> is the username of the user (as in windows username) and the <random_sequence> is a random sequence of characters.

There you will find files with no extension accompanied by files with the .msf extension. If you have created any subfolder you will see folders with the foldername.sdb format.

  1. To import your email create a folder in the Local directory (e.g. importedmail.sdb). You have to stick with that name to the following steps (that is importedmail).
  2. Then inside the folder copy the .mbs file and rename it to importedmail with no extension
  3. Copy the .mbs file again this time rename it to importedmail.msf.
  4. Restart thunderbird and wait for a while. A importedmail folder should appear under the Local Folders. After that you can copy these emails to a mail account.

I tried to create he folders directly in a gmail account but thunderbird wouldn’t find the mails. Thus I first imported to the Local folders and then copied to the account.