Database classes

Classes
class	skeleton_glb
	A skeleton_glb is a directory holding a database. More...

Detailed Description

The skeleton_glb class handles all disk related functions and management. The database is basically a directory and all its sub-directories in disk. The directory (skeleton_glb) is seen as a group of (''key'',''value'') pairs. Just like a common database ''index'', a ''dictionary'' class, or a ''map'' class. A path within the skeleton_glb is a ''key'' and the files in the path are the ''value''. To see if a ''key'' exists is to see if a path exists within the skeleton_glb. Unsatisfiable canon_cnf s are saved and searched by the SHA function of their content. They are saved in a path (''key'') that is constructed with the SHA and other relevant search info.

Since an unsatisfiable sub-formula might not be minimal (have some unnecessary clauses for unsatisfiability), each unsatisfiable CNF sub-formula has three relevant canon_cnf:

• The guide. It is the canon_cnf resulting of stabilizing the CNF sub-formula covered by first search branch variables. So it is a satisfiable part of the unsatisfiable CNF sub-formula that is a ''guide'' for the search.

• The tauto. It is the full unsatisfiable CNF sub-formula. It is the canon_cnf resulting of stabilizing the CNF sub-formula covered by both search branches charged quanton s (used variables).

• The diff. This canon_cnf contains all canon_clause s in tauto but not in guide. Each diff is saved in a path called 'variant' in the skeleton_glb. So one guide can have several variants.

A search of a target CNF sub-formula is conducted in two phases: the search for the guide of the target and the search for the variant that is a sub-formula of the target diff. Once the guide is stabilized the search for it is a simple: ''see if its path exists'' (remember that its path contains the SHA of its content). If the target canon_cnf is not equal to a variant (the path does not exist), the second phase is more time consuming because it involves reading each variant and comparing it to the target diff to see if the the variant is a sub-formula of the target diff (which would mean that the target is unsatisfiable and therefore can be backtracked).