CVC3
Classes | Public Member Functions | Private Member Functions | Private Attributes | Friends

CVC3::SearchEngineFast Class Reference

Implementation of a faster search engine, using newer techniques. More...

#include <search_fast.h>

Inherits CVC3::SearchImplBase.

Collaboration diagram for CVC3::SearchEngineFast:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Private Member Functions

Processing a Conflict

Private Attributes

Friends


Detailed Description

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.

Definition at line 89 of file search_fast.h.


Friends And Related Function Documentation

friend class Circuit [friend]

Definition at line 91 of file search_fast.h.

Referenced by addNonLiteralFact().


The documentation for this class was generated from the following files: