Implementation of a faster search engine, using newer techniques. More...
Implementation of a faster search engine, using newer techniques.
This search engine is engineered for greater speed. It seeks to eliminate the use of recursion, and instead replace it with iterative procedures that have cleanly defined invariants. This will hopefully not only eliminate bugs or inefficiencies that have been difficult to track down in the default version, but it should also make it easier to trace, read, and understand. It strives to be in line with the most modern SAT techniques.
There are three other significant changes.
One, we want to improve the performance on heavily non-CNF problems. Unlike the older CVC, CVC3 does not expand problems into CNF and solve, but rather uses decision procedures to effect the same thing, but often much more slowly. This search engine will leverage off knowledge gained from the DPs in the form of conflict clauses as much as possible.
Two, the solver has traditionally had a difficult time getting started on non-CNF problems. Modern satsolvers also have this problem, and so they employ "restarts" to try solving the problem again after gaining more knowledge about the problem at hand. This allows a more accurate choice of splitters, and in the case of non-CNF problems, the solver can immediately leverage off CNF conflict clauses that were not initially available.
Third, this code is specifically designed to deal with the new dependency tracking. Lazy maps will be eliminated in favor implicit conflict graphs, reducing computation time in two different ways.
|friend class Circuit