I have been writing software for more than 20 years now. I thought it’s about time to gather my experiences and write some advice on building better software.
1. Solve the right problem
It is all too often that one tries solving something before understanding the problem at hand. We have a certain understanding of what the issue is, write something to solve it, but it turns out that we wrote the wrong solution because we misunderstood the problem. Do some research, read some articles, talk to people and read some books before attempting to solve a problem.
The use of Gmail is now ubiquitous. Unfortunately, it’s easy to read email in transit and some national governments abuse their power to read email in transit. I have always been using PGP to encrypt email, and today I thought I’d put down how to communicate with me, or with your friends, using signed and encrypted mail. I think the biggest reason email encryption is not being used is because it’s hard to set up. So, here is a simple, step-by-step tutorial that is easy to follow.
Installing and creating a key
- Install Mailvelope . Click “add to chrome”, pop-up appears, click “add”
- little padlock icon appears on the top right of your Chrome
- Click little padlock icon, click “Options”
- At the bottom, click “Generate key”
- Fill in Name (you can put fictitious name, it’s good!), Email (the email you want to use, e.g. Jon.Doe@gmail.com), put in a password that you will remember. This password is never sent anywhere. It’s used so that when you want to read email that is encrypted to you, the encryption keys can be accessed.
- Click submit, wait for the generation to finish.
- Setup is done!
CyptoMinSat 3.2.0 has been released. This code should be extremely stable and should contain no bugs. In case it does, CryptoMiniSat will fail quite bady at the competition. I have fuzzed the solver for about 2-3000 CPU hours, with some sophisticated fuzzers (all available here — most of them not mine) so all should be fine, but fingers are crossed.
Additions and fixes
The main addition this time is certification proofs for UNSAT through the use of DRUP. This allows for use of the solver where certainty of the UNSAT result is a necessity — e.g. where lives could potentially depend on it. Unfortunately, proof checking is relatively slow through any system, though DRUP seems to be the best and fastest method. Other than the implementation of DRUP, I have fixed some issues with variable replacement.
The description of the solver sent in to the SAT Competition’13 is available from the subfolder “desc” of the tarball. The code of 3.2.0 is actually the same that will run during the competition, the only changes made were:
- the DRUP output had to be put into the standard output
- the line “o proof DRUP” had to be printed
- certified UNSAT binary uses the “–unsat 1” option by default
- compilation was changed to use the m4ri library that was included with the tarball
- linking is static so m4ri and other requirements don’t cause trouble
- boost minimum version had to be lowered
You can download my submissions to the competition, forl, from here and here.