Computer-implemented techniques are disclosed for verifying circuit designs using dynamic problem generation. A device under test (DUT) is modeled as part of a test bench where the test bench is a random process. A set of constraints is solved to generate stimuli for the DUT. Problem generation is repeated numerous times throughout a verification process with problems and sub-problems being generated and solved. When a problem is solved, the problem structure can be stored in a cache. The storage can be based on entropy of variables used in the problem. The problem storage cache can be searched for previously stored problems which match a current problem. By retrieving a problem structure from cache, the computational burden is reduced during verification. Problems can be multi-phase problems with storage and retrieval of problem structures based on the phase level. Caching can be accomplished using an information theoretic approach.