Timetabler
|
Class for solver. More...
#include <tsolver.h>
Public Member Functions | |
TSolver (int, int) | |
Constructs the TSolver object. More... | |
std::vector< lbool > | tSearch () |
Solves the MaxSAT problem by calling the solver. More... | |
void | tWeighted () |
Solves a weighted MaxSAT problem. More... | |
Class for solver.
This class inherits from the OLL algorithm of Open WBO. This reimplements the search() and the weighted() functions as tSearch() and tWeighted(). Most of the code is identical. The differences are that tSearch() does not print the output to stdout and exit, instead, it returns the model. tWeighted() also does not print to stdout, when the solver terminates, it simply returns.
TSolver::TSolver | ( | int | verb = _VERBOSITY_MINIMAL_ , |
int | enc = _CARD_TOTALIZER_ |
||
) |
Constructs the TSolver object.
[in] | verb | The verbosity value to be given to the OLL object |
[in] | enc | The encoding value to be given to the OLL object |
std::vector< lbool > TSolver::tSearch | ( | ) |
Solves the MaxSAT problem by calling the solver.
This is a modification of the search() function in the OLL algorithm of Open WBO. Most of the code is identical, except that it expects the problem to be weighted and returns the model found by the solver instead of exiting at the end.
void TSolver::tWeighted | ( | ) |
Solves a weighted MaxSAT problem.
This is a modification of the weighted() function in the OLL algorithm of Open WBO. Most of the code is identical, except that when the result is found, the function returns instead of printing the answer to stdout and exiting.