Timetabler
Public Member Functions | List of all members
TSolver Class Reference

Class for solver. More...

#include <tsolver.h>

Inheritance diagram for TSolver:
Inheritance graph
[legend]
Collaboration diagram for TSolver:
Collaboration graph
[legend]

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...
 

Detailed Description

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.

Constructor & Destructor Documentation

TSolver::TSolver ( int  verb = _VERBOSITY_MINIMAL_,
int  enc = _CARD_TOTALIZER_ 
)

Constructs the TSolver object.

Parameters
[in]verbThe verbosity value to be given to the OLL object
[in]encThe encoding value to be given to the OLL object

Member Function Documentation

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.

Returns
The model found by the solver. This could be empty if the problem was unsatisfiable
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.


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