 |
Doxygen Generated Documentation of Ben-Jose Trainable SAT Solver Library
|
|
Doxygen Generated Documentation of Ben-Jose Trainable SAT Solver Library
|
A skeleton_glb is a directory holding a database. More...
#include <skeleton.h>
Collaboration diagram for skeleton_glb:A skeleton_glb is a directory holding a database.
The skeleton class handles all disk related functions and management. The database is basically a directory and all its sub-directories in disk. The directory (skeleton) 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 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. Unsatisfiable canoncnf 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 canoncnf :
The guide. It is the canoncnf 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 canoncnf resulting of stabilizing the CNF sub-formula covered by both search branches charged quanton s (used variables).
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 canoncnf 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).
1.8.11
