Introduction

This is the doxy generated documentation of the Ben-Jose Trainable SAT Solver Library. It is not a complete reference of all the classes and functions. It is a selection of the most releveant classes and functions that help in the understanding of the innerworkig of the library.

The User's API of the library is implemented in the files ben_jose.cpp and ben_jose.h, and documented in:

• User's API

The architecture of the ben-jose library is strongly monolitic in the sense that the basic functionality of the whole library is basically one function (brain::solve_instance) with three presentations:

• bj_solve_file
• bj_solve_data
• bj_solve_literals

That means that every piece of code within the 'library' directory of the source tree is tightly coupled. Having said that, this documentations should give a good idea of it's architecture.

The most relevant classes of the library implementation can be grouped as:

• DPLL+BCP+CDCL classes
• Stabilization classes
• Matching classes
• Database classes

The macro behavior of the innerwork of the library is described in:

• macro_algorithm_ben_jose.cpp