Class Paramita::Testing::NonIncrMaxSatSolverDummy¶

Inherits the following classes: Paramita::NonIncrMaxSatSolver

Public Static Attributes inherited from Paramita::NonIncrMaxSatSolver¶

Type	Name
constexpr const char *const	m_interface_id = `/* multi line expression */`

Public Static Attributes inherited from Paramita::WClauseContainer¶

See Paramita::WClauseContainer

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::WClauseContainer"`

Public Static Attributes inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::Plugin"`

Public Functions¶

Type	Name
virtual	add_clause (const Clause & clause, Weight weight) override Add a single clause with the specified weight.
virtual std::uint64_t	max_var () override const Get the largest variable used in the container.
virtual std::vector< Literal >	model () override const Get the model (solution) after solving.
virtual	set_minimum_var (std::uint64_t var) override Sets the maximum variable known to the container to at least this one.
virtual MAXSAT_ANSWER	solve (const std::vector< Literal > & assumptions, const SolvingBudget & budget) override Solve the formula under given assumptions.
virtual std::uint64_t	val_objective () override const The sum of weights for satisfied soft clauses from the last feasible solution.

Public Functions inherited from Paramita::NonIncrMaxSatSolver¶

See Paramita::NonIncrMaxSatSolver

Type	Name
	NonIncrMaxSatSolver () = default
	NonIncrMaxSatSolver (const NonIncrMaxSatSolver &) = delete Deleted copy constructor (pure interface).
	NonIncrMaxSatSolver (NonIncrMaxSatSolver &&) = delete Deleted copy constructor (pure interface).
virtual	assume (Literal lit) Add an assumption for the next `solve` call.
virtual NonIncrMaxSatSolver *	clone () override Clone the current solver.
virtual std::pair< std::uint64_t, std::vector< Literal > >	core () Retrieve the unsatisfiable core.
virtual	interrupt () Interrupts the resolution process.
virtual std::uint64_t	lower_bound () Returns a lower bound on the objective value of the formula.
virtual std::vector< Literal >	model () const = 0 Get the model (solution) after solving.
virtual std::uint64_t	num_conflicts () The number of conflicts triggered by a `solve` call.
NonIncrMaxSatSolver &	operator= (const NonIncrMaxSatSolver & container) = delete Deleted copy constructor (pure interface).
NonIncrMaxSatSolver &	operator= (NonIncrMaxSatSolver &&) = delete Deleted copy constructor (pure interface).
virtual	simplify (unsigned int num_rounds) Simplify the formula.
virtual MAXSAT_ANSWER	solve (const std::vector< Literal > & assumptions, const SolvingBudget & budget) = 0 Solve the formula under given assumptions.
virtual std::optional< bool >	val_lit (Literal lit) The truth value for a literal in the best solution.
virtual std::uint64_t	val_objective () const = 0 The sum of weights for satisfied soft clauses from the last feasible solution.
	~NonIncrMaxSatSolver () override

Public Functions inherited from Paramita::WClauseContainer¶

See Paramita::WClauseContainer

Type	Name
	WClauseContainer () = default
	WClauseContainer (const WClauseContainer &) = delete
	WClauseContainer (WClauseContainer &&) = delete
virtual	add_clause (const Clause & clause, Weight weight) = 0 Add a single clause with the specified weight.
virtual	add_clauses (const std::vector< Clause > & clauses, Weight weight) Add multiple clauses to the container.
virtual	add_lit (Literal lit) Add a clause literal by literal.
virtual	add_soft_lit (Literal lit, std::uint64_t weight) Declare a literal as a soft literal with a weight.
virtual	add_weight (Weight weight) Changes the weight for the next clause that is added literal by literal.
virtual WClauseContainer *	clone () Clones the current container.
virtual std::uint64_t	max_var () const = 0 Get the largest variable used in the container.
virtual std::unordered_map< Weight, int >	num_clauses () const Obtain the distribution of clauses hold by the container over weights.
WClauseContainer &	operator= (const WClauseContainer & container) = delete
WClauseContainer &	operator= (WClauseContainer &&) = delete
virtual	set_minimum_var (std::uint64_t var) = 0 Sets the maximum variable known to the container to at least this one.
	~WClauseContainer () override

Public Functions inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
	Plugin () = default
	Plugin (const Plugin &) = delete Deleted constructor (pure interface).
	Plugin (Plugin &&) = delete Deleted constructor (pure interface).
virtual ParameterType	get (const std::string & name) Get the parameter's value.
virtual ParameterSpace	get_parameter_space () Get the parameter space for this class.
Plugin &	operator= (const Plugin & container) = delete Deleted constructor (pure interface).
Plugin &	operator= (Plugin &&) = delete Deleted constructor (pure interface).
virtual	set (const std::string & name, const ParameterType & value) Set a parameter.
virtual	~Plugin () = default

Public Functions Documentation¶

function add_clause¶

Add a single clause with the specified weight.

inline virtual Paramita::Testing::NonIncrMaxSatSolverDummy::add_clause (
    const Clause & clause,
    Weight weight
) override

Parameters:

clause The clause to be added to the container.
weight The associated weight for this clause.

Implements Paramita::WClauseContainer::add_clause

function max_var¶

Get the largest variable used in the container.

inline virtual std::uint64_t Paramita::Testing::NonIncrMaxSatSolverDummy::max_var () override const

Postcondition:

The return value is equal or larger to the absolute value for any literal passed to add_clause, add_clauses, or add_lit.

Returns:

The (positive) integer assigned to the largest variable.

Implements Paramita::WClauseContainer::max_var

function model¶

Get the model (solution) after solving.

inline virtual std::vector< Literal > Paramita::Testing::NonIncrMaxSatSolverDummy::model () override const

The model in a MaxSAT solver will correspond to the best solution found during solving (not only from the last call).

Precondition:

Method solve was called.

Precondition:

Method solve returned MAXSAT_ANSWER::SATISFIABLE or MAXSAT_ANSWER::OPTIMAL.

Warning:

Undefined behaviour if solve returned MAXSAT_ANSWER::UNKNOWN.

Returns:

A vector with the literals that were set to true by the last solve call.

Exception:

NotSolvedException if solve was not called before.
UnsatisfiableException if solve returned MAXSAT_ANSWER::UNSATISFIABLE.

Implements Paramita::NonIncrMaxSatSolver::model

function set_minimum_var¶

Sets the maximum variable known to the container to at least this one.

inline virtual Paramita::Testing::NonIncrMaxSatSolverDummy::set_minimum_var (
    std::uint64_t var
) override

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the WClauseContainer::max_var method to determine the next free variable, this method ensures that existing variables cannot be reused.

Postcondition:

The value returned by max_var must be larger or equal than the one provided.

Postcondition:

The value returned by max_var cannot be reduced by this call.

Parameters:

var The variable to be registered to the container.

Implements Paramita::WClauseContainer::set_minimum_var

function solve¶

Solve the formula under given assumptions.

inline virtual MAXSAT_ANSWER Paramita::Testing::NonIncrMaxSatSolverDummy::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) override

The feasible solutions of the formula are assignments that satisfy all the hard clauses in the formula.

The cost of a solution is the sum of the weights of the soft clauses not satisfied by the solution.

An optimal solution is a feasible solution with minimal cost.

If interrupted, the solver is responsible from clearing the interruption.

See also: interrupt

Precondition:

solve method has not been called, or no clause has been added since the last solve call.

Postcondition:

The internal solving budget is reset to unlimited.

Parameters:

assumptions The literals manually assigned to true.
budget Budget restrictions for the solve process.

Returns:

MAXSAT_ANSWER::UNKNOWN if no feasible solution is found and the satisfiability of hard clauses has not been determined, MAXSAT_ANSWER::SATISFIABLE if a feasible solution is found but has not been proved to be optimal, MAXSAT_ANSWER::UNSATISFIABLE if the hard clauses are proven to be unsatisfiable, and MAXSAT_ANSWER::OPTIMAL if the feasible solution is proven to be optimal (each of those cases considering the given assumptions).

Implements Paramita::NonIncrMaxSatSolver::solve

function val_objective¶

The sum of weights for satisfied soft clauses from the last feasible solution.

inline virtual std::uint64_t Paramita::Testing::NonIncrMaxSatSolverDummy::val_objective () override const

The objective value of a solution corresponds to the sum of all the weights for the soft clauses minus the cost of the clauses.

Precondition:

Method solve was called.

Precondition:

Method solve returned MAXSAT_ANSWER::SATISFIABLE or MAXSAT_ANSWER::OPTIMAL.

Warning:

Undefined behaviour if solve returned MAXSAT_ANSWER::UNKNOWN.

Returns:

The sum of the weights of the satisfied soft clauses.

Exception:

NotSolvedException if solve was not called before.
UnsatisfiableException if solve returned MAXSAT_ANSWER::UNSATISFIABLE.

Implements Paramita::NonIncrMaxSatSolver::val_objective