Class for solver. More...

#include <tsolver.h>

Inheritance diagram for TSolver:

Collaboration diagram for TSolver:

Public Member Functions
	TSolver (int verb=_VERBOSITY_MINIMAL_, int enc=_CARD_TOTALIZER_)
	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.

Definition at line 25 of file tsolver.h.

Constructor & Destructor Documentation

◆ TSolver()

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

Constructs the TSolver object.

Parameters

[in]	verb	The verbosity value to be given to the OLL object
[in]	enc	The encoding value to be given to the OLL object

Definition at line 48 of file tsolver.cpp.

Member Function Documentation

◆ tSearch()

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

Definition at line 61 of file tsolver.cpp.

References tWeighted().

◆ tWeighted()

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.

Definition at line 87 of file tsolver.cpp.

Referenced by tSearch().

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

/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/latest/include/tsolver.h
/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/latest/src/tsolver.cpp