Sunday, March 6, 2011

Instances solved during a run.

This morning I though of checking the number of variables in subinstances solved during a typical run. I created a histogram below (note log scale on both axis). Over 1.000.000 instances had 3 variables. That's a lot of overhead considering that an instance with very few variables is easy to solve by checking all possible assignments. In the picture below created represents the instances created and solved represents the instances created but not solved by the simplification procedure.

At some point I added a simple backtracking algorithm to deal away with small instances, however it didn't influence the results that much. Probably I should test it again. I could use, for example, sat4j to solve small instances, but since probably sat4j is more efficient than STRUCTure the results will be biased.

Nevertheless switching to another algorithm doesn't fix the root problem which I can't understand yet. My guess is that lookahead solvers are not that good on easy instances with many variables that appear in relatively few clauses. What I want to do next is to add another simplification procedure to eliminate these variables like variable elimination in SatElite, but simpler and at every branching node.

1 comment:

  1. These can be summarized in what recognized as|is called|is named} a Basic Strategy desk. However, sure performs in the desk need to be modified based on the particular mixture of guidelines in pressure. To make sure of half in} correctly, 우리카지노 it is necessary to generate a Basic Strategy desk for the particular guidelines of the game being performed. Surrender – Some casinos allow a player to give up, taking again half their guess and giving up their hand. Surrender should be the player's first and only action on the hand.