All posts by msoos

My Dell Vostro 3560 review

Personal, Uncategorized

In this post I would like to share with you a personal review of my new business line laptop from Dell, the Vostro 3560. It’s a 15.6″ laptop that has Full HD screen using TN display technology, a 750GB HDD spinning at 7500rpm, 6GB of DDR3 RAM clocked at 1600MHz, with the highest possible Core i7 processor available for this machine, the i7-3612QM, that goes to 3.1GHz with all cores still active.

Overview of the laptop

The good

First, let me talk about what I found to be great about this laptop. The display is great: it’s sharp, the colors are good and it’s bright enough even in strong sunlight — though admittedly here in Berlin there is not much of that.

The keyboard is also magnificent. It’s one of the best keyboards I have ever used, even though I am very particular about my peripherals, especially keyboards and mice. I used to own business Thinkpads and this is the first keyboard that I have found to be as good as or maybe even better than a Thinkpad keyboard.

The system is built sturdily, and the materials used don’t feel cheap in your hands. Though the system isn’t light, it feels easy to hold due to its rigidity and smooth (but not slippery) surfaces.

Finally, the system contains extras that are only mentioned in the service manual. For example, there is an mSATA socket inside the laptop, meaning you can plug a 256GB mSATA SSD into the system in a couple of minutes for a reasonable price (around 200EUR), significantly speeding things up.

The mediocre

The CPU is a trade-off. It’s not the i7-3610QM which would go up to 3.3GHz with all cores still active. The reason for this is interestingly not price: the two CPUs cost the same from intel — the reason is heat removal. The CPU installed only generates 35W of heat while the other generates 45W. Essentially, Dell didn’t work hard enough on the cooling system and the result is that a better CPU cannot be installed. Unfortunately, Dell is not the only one that couldn’t install the 3610QM, other manufacturers such as Sony with the Vaio S series had the same issue. Naturally, Apple with the new MacBook Pro lineup didn’t mess this up.

The included charger is rather bulky. Interestingly, there is a slimmer charger available, for a mere 114 EUR — the one included costs 50EUR on the same Dell webpage. I find this to be rather disappointing.

Bulky charger included

Slim charger, available at 114EUR


The wireless card inside the system doesn’t support 5GHz WiFi. This sounds minor, until you go to a conference or a public place with a WiFi where everyone seems to be able to connect, except you. 2.4GHz WiFi uses a band that is substantially more noisy and since routers on that band cover more area, if many people are in the same place, connection can be very spotty. In comparison, my IBM X61t, released in 2007 (!) had 5GHz WiFi, so it’s hardly new technology. In fact, for about 30EUR you can change your WiFi card inside the case for one that supports Bluetooth+802.11abgn, i.e. all that is inside plus 5GHz WiFi. I still cannot understand why a computer that costs 900+ EUR would cheap out on such a component — especially since Dell can get bulk discount, so the upgrade for them would be around 10 EUR at most.

The system comes with a DVD writer included, but I don’t have any use for that. Who uses DVDs nowadays? If I want to watch a movie, I use Blu-Ray — after all, the display is Full HD! Having a Blu-Ray option would have been easy for the manufacturer, as the DVD player included is a standard one, so it can be easily swapped to an internal notebook Blu-Ray reader. Such readers cost around 60EUR at any online retailer. In fact, a Blu-Ray internal writer would cost no more than 80EUR. Dell missed out on this completely, for no good reason. Yes, it’s for business, but even business people need to back up their HDD and a DVD writer with a capacity of 4GB won’t be of any help.

The bad

Build quality is terrible. This is very surprising at this price range and in this category (i.e. business). First off, the screen’s backplate fits so badly to the front that there are holes larger than 2mm on the right side, and almost none on the left:

Left side of panel

Right side of panel



The same, though less accentuated, is true for the palmrest. You can clearly see that the plastic fits differently on the two sides, and in fact fits unevenly on both:

Left side of front

Right side of bottom

 

Similarly, the bottom sticker of the laptop with the most important piece of information, the Service Tag, is of such a low quality that after only 2 months of use the numbers got completely erased, and only the barcode (blacked out for privacy) remains readable:

My Service Tag — other than the barcode (blacked out) it’s unreadable


Finally, Linux support is terrible. I wanted to get reimbursed for the Windows 7 licence, but they refused it, which I think is clearly illegal, but of course I don’t have months to waste and money to burn to get some 50-100 EUR back. In the same spirit, there is no proper support for controlling the fan under Linux, as the highest level of the fan cannot be attained with the linux driver, and there is no proper palm detection support for the touchpad. The AMD Linux driver available at the time of purchase crashed X11 at startup, but the new one (fglrx 8.980) is flawless, and I have to commend AMD the on that.

Conclusions

The Vostro 3560 is a nice piece of machine but it’s not quite business quality and its makers prefer not to hear the word Linux uttered. However, if you are ready to shell out some money on a Blu-Ray drive, don’t intend to use Linux and are content with mediocre build quality with holes between elements the size an edge of a penny, the Vostro 3560 is a good choice. Otherwise, maybe hold out for a better offer.

[paypal-donation]

How to use CryptoMiniSat 2.9 as a library

Development, SAT,

There have been some questions asked about how to use CryptoMiniSat as a library. Here, I give a simple example usage to help any future potential users. If there are any question that seems unanswered, please feel free to add them as a comment to this post.

First, we initialize the solver with high verbosity:

#include "cmsat/Solver.h"
using namespace CMSat;

SolverConf conf;
conf.verbosity = 2;
Solver solver(conf);

Then we add the variables 0..9:

for(int i = 0; i < 10; i++) {
  solver.newVar();
}

And add a clause that would look in the DIMACS input format as "2 -5 10 0":

vec clause;
clause.push(Lit(1, false));
clause.push(Lit(4, true));
clause.push(Lit(9, false));
solver.addClause(clause);

We now create the assumptions that would look in DIMACS input format as "1 0" and "-5 0":

vec assumps;
assumps.push(Lit(0, false));
assumps.push(Lit(4, true));

We now solve with these assumptions:

lbool ret = solver.solve(assumps);

Let's see if the state of the solver after solving is UNSAT regardless of the assumptions:

if (!solver.okay()) {
  printf("UNSAT!\n");
  exit(0);
}

Note that okay() can only be FALSE if "ret" was "l_False". However, it is important to distinguish between two kinds of l_False: one where only the assumptions couldn't be satisfied, and one where no matter what the assumptions are, the problem is unsatisfiable. See below for more.

Now let's check that the solution is UNSAT relative to the assumptions we have given. In this case, let's print the conflicting clause:

if (ret == l_False) {
  printf("Conflict clause expressed in terms of the assumptions:\n");
  for(unsigned i = 0; i != solver.conflict.size(); i++) {
    printf("%s%d ", (solver.conflict[i].sign()) ? "" : "-", solver.conflict[i].var()+1);
  }
  printf("0\n");
}

The above will print an empty clause if solver.okay() is FALSE.

Now, let's see if the solution is SAT, and if so, print the solution to console, using DIMACS notation:

if (ret == l_True) {
  printf("We have the solution, it's here: \n");
  for (unsigned var = 0; var != solve.nVars(); var++)
    if (S.model[var] != l_Undef) {
      printf("%s%d ", (solver.model[var] == l_True)? "" : "-", var+1);
      printf("0\n");
    }
}

If solver.okay() is still TRUE (which it must be, if the ret was l_True), we can now add new clauses and new variables without restriction, and solve again (potentially with different assumptions). Note that most of the above applies to MiniSat as well.

When compiling the code, you have to pass the parameters such as:

$ g++ -fopenmp -lcryptominisat myprogram.cpp -o myprogram

PS: Thanks go to Martin Albrecht for pointing out some ambiguities in my explanation of the library usage, which have now been fixed.

Visualizing SAT solving

Uncategorized,

Visualizing the solving of mizh-md5-47-3.cnf


Visualizing what happens during SAT solving has been a long-term goal of mine, and finally, I have managed to pull together something that I feel confident about. The system is fully explained in the liked image on the right, including how to read the graphs and why I made them. Here, I would like to talk about the challenges I had to overcome to create the system.

Gathering information

Gathering information during solving is challenging for two reasons. First, it’s hard to know what to gather. Second, gathering the information should not affect overall speed of the solver (or only minimally), so the code to gather the information has to be well-written. To top it all, if much information is gathered, these have to be structured in a sane way, so it’s easy to access later.

It took me about 1-1.5 months to write the code to gather all information I wanted. It took a lot of time to correctly structure and to decide about how to store/summarize the information gathered. There is much more gathered than shown on the webpage, but more about that below.

Selecting what to display, and how

This may sound trivial. Some would simply say: just display all information! But what we really want is not just plain information: what good is it to print 100’000 numbers on a screen? The data has to be displayed in a meaningful and visually understandable way.

Getting to the current layout took a lot of time and many-many discussions with all all my friends and colleagues. I am eternally grateful for their input — it’s hard to know how good a layout is until someone sees it for the first time, and completely misunderstands it. Then you know you have to change it: until then, it was trivial to you what the graph meant, after all, you made it!

What to display is a bit more complex. There is a lot of data gathered, but what is interesting? Naturally, I couldn’t display everything, so I had to select. But selection may become a form of misrepresentation: if some important data isn’t displayed, the system is effectively lying. So, I tried to add as much as possible that still made sense. This lead to a very large table of graphs, but I think it’s still understandable. Further, the graphs can be moved around (just drag their labels), so doing comparative analysis is not hampered much by the large set of graphs.

The final layout is much influenced by Edward Tufte‘s books. Most graphic libraries for javascript, including what I used, Dygraphs, contain a lot of chartjunk by default. For example, the professional library HighCharts is full chartjunk (just look at their webpage), and is apparently used by many Fortune 500 companies. I was appalled at this — many-many graph libraries, none that offers a clean look? Luckily, I could do away with all that colorful beautifying mess — the data is interesting, and demands no embellishments.

Creating the webpage

Creating the webpage to display what I wanted was quite difficult. I am no expert at PHP or HTML, and this was the first time I had touched javascript. Although the final page doesn’t show it much, I struggled quite a bit with all these different tools. If I had to do this again, I would choose to use a page generation framework. This time, I wrote everything by hand.

I am most proud of two things on the webpage. First is the histogram at the bottom of the graphs. I know it may not seem like it, but that is all done with a javascript I wrote that pulls data from an array that could be dynamically changed. I think it does what it’s supposed to do, and does it well. The second is that I had to tweak the graph library used (Dygraphs, the best library out there, hands down), because it was too slow at printing these ~30 graphs. The graphs can be zoomed (just click and drag on X axis), and when zooming in&out the speed was really terrible. It now works relatively fast though I had to tweak the system to trade speed for a bit of visual beauty.

Final thoughts

Making the visualization webpage was a long marathon. I feel like it’s OK now, even though there were quite a number of ideas that weren’t implemented in the end. I hope you will enjoy playing with it as much as I have enjoyed making it.

Q-DIMM, an “innovation” by ASUS

Personal,

Lately, I have been having boot problems with my computer: the system would sometimes fail to boot, and at other times, it displayed the wrong memory readings. I was puzzled, so I took a look. I have six memory DIMMs installed in an ASUS motherboard. Memory modules are usually retained in their slots using two latches:

The point of these latches is to keep the memory modules in place when the computer is moved around. They thus serve the same purpose as the screws for PCIe slots or the mounting holes for the CPU coolers. My motherboard, however, is made by ASUS, and it has a “feature” called Q-DIMM, which is supposed to ease the installation of memory modules when the system has the video card already installed. This “feature” is rather simple: the latch on the right is completely missing:

Unsurprisingly, over time, some of my memory modules simply came out from their slots, making the system completely unstable. And I am far from being the only one who has had this problem.

Most probably the person who came up with this “feature” wasn’t an engineer, but a PR person. It is however rather sad that a technological company such as ASUS should make technical decisions based on PR. By the above logic, I wonder why they didn’t remove both latches. And while they were at it, get rid of all those pesky screw holes for the PCIe slots, and the mounting holes for the CPU cooler, too — things would be much easier to install!

Seriously, though, this is just unbelievable. Fun part is, ASUS sells this “feature” as an innovation that is available only to their high-end (and more expensive) motherboards. I don’t know whether to laugh or cry that you have to spend less to get a more robust, stable system.

On hyper-binary resolution

Research, SAT, ,

Hyper-binary resolution is actually quite straightforward, or at least appears to be. Let’s take the following example. The clauses in our database are the following:

-a V b
-a V c
-b V -c V g
-b V -c V d
-d V g

Let’s set a to true, and see what happens. Immediately, b and c get set to true through binary clauses. If we now propagate g through the clause -b V -c V g, we ought to do hyper-binary resolution straight away, and add the clause -a V g — some call this lazy hyper-binary resolution. Good, one more binary clause!

But then… So now we have nothing to propagate using only binary clauses, we have to propagate using a long clause, -b V -c V d. As good citizens, we also do (lazy) hyper-binary resolution, coming up with the clause -a V d. Good, one more binary clause! One slight glitch now… d propagates to g, using a binary clause. But this means that setting a can propagate to g without -a V g, the first hyper-binary clause we added! So the first hyper-binary clause we added is in fact useless, it needs to be removed. If we applied transitive reduction, it would remove the first hyper-binary clause -a V g automatically.

Let’s go a bit deeper here. How could we have avoided adding the first hyper-binary clause? The obvious answer is: we should have started with -b V -c V d instead of -b V -c V g. But how easy would have it been to know (i.e. calculate) that starting with that different long clause would have made our work easier? I am not sure it would have been easy to know. And of course the example above is very trivial. It could be made much-much more complicated: g could have been reached with any number of hyper-binary resolutions from d — so simple binary look-ahead would not have helped.

I am stuck here. Any ideas?