Class Paramita::NonIncrMaxSatSolver¶

A MaxSAT solver.

Note:

Use NON_INCR_MAXSAT_SOLVER_C_INTERFACE to register any subclass of this interface.

#include <NonIncrMaxSatSolver.hpp>

Inherits the following classes: Paramita::WClauseContainer

Public Static Attributes¶

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
	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 Static Attributes Documentation¶

variable m_interface_id¶

constexpr const char* const Paramita::NonIncrMaxSatSolver::m_interface_id;

Public Functions Documentation¶

function NonIncrMaxSatSolver [1/3]¶

Paramita::NonIncrMaxSatSolver::NonIncrMaxSatSolver () = default

function NonIncrMaxSatSolver [2/3]¶

Deleted copy constructor (pure interface).

Paramita::NonIncrMaxSatSolver::NonIncrMaxSatSolver (
    const NonIncrMaxSatSolver &
) = delete

function NonIncrMaxSatSolver [3/3]¶

Deleted copy constructor (pure interface).

Paramita::NonIncrMaxSatSolver::NonIncrMaxSatSolver (
    NonIncrMaxSatSolver &&
) = delete

function assume¶

Add an assumption for the next solve call.

virtual Paramita::NonIncrMaxSatSolver::assume (
    Literal lit
)

See ipamir2022 for more details.

function clone¶

Clone the current solver.

virtual NonIncrMaxSatSolver * Paramita::NonIncrMaxSatSolver::clone () override

Returns:

The cloned solver.

Implements Paramita::WClauseContainer::clone

function core¶

Retrieve the unsatisfiable core.

virtual std::pair< std::uint64_t, std::vector< Literal > > Paramita::NonIncrMaxSatSolver::core ()

Returns:

A pair with a) a lower bound associated to the core, and b) a vector filled with a subset of the assumptions that are jointly unsatisfiable.

Precondition:

solve was called with assumptions.

Precondition:

The instance must be unsatisfiable under the given assumptions.

Exception:

UnsupportedMethodException This method is optional.

function interrupt¶

Interrupts the resolution process.

virtual Paramita::NonIncrMaxSatSolver::interrupt ()

This method instructs the solver to stop solving or propagating. Note that this is a notification, not an immediate stop, when the solver is interrupted is implementation defined.

Precondition:

The solver is solving or propagating.

Postcondition:

After interrupting, the solver must stay in a stable state.

Exception:

UnsupportedMethodException This method is optional.

function lower_bound¶

Returns a lower bound on the objective value of the formula.

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::lower_bound ()

Note:

This method does not require a previous call to solve, as the solver could in theory compute an initial lower bound when adding clauses.

Returns:

The lower bound computed for the formula.

function model¶

Get the model (solution) after solving.

virtual std::vector< Literal > Paramita::NonIncrMaxSatSolver::model () const = 0

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.

function num_conflicts¶

The number of conflicts triggered by a solve call.

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::num_conflicts ()

Note:

The number of conflicts triggered while searching for a solution depends on each algorithm implementation.

Precondition:

Method solve was called.

Returns:

The number of conflicts.

function operator=¶

Deleted copy constructor (pure interface).

NonIncrMaxSatSolver & Paramita::NonIncrMaxSatSolver::operator= (
    const NonIncrMaxSatSolver & container
) = delete

function operator=¶

Deleted copy constructor (pure interface).

NonIncrMaxSatSolver & Paramita::NonIncrMaxSatSolver::operator= (
    NonIncrMaxSatSolver &&
) = delete

function simplify¶

Simplify the formula.

virtual Paramita::NonIncrMaxSatSolver::simplify (
    unsigned int num_rounds
)

Parameters:

num_rounds The number of simplification rounds to apply.

Exception:

UnsupportedMethodException This method is optional.

function solve¶

Solve the formula under given assumptions.

virtual MAXSAT_ANSWER Paramita::NonIncrMaxSatSolver::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) = 0

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

function val_lit¶

The truth value for a literal in the best solution.

virtual std::optional< bool > Paramita::NonIncrMaxSatSolver::val_lit (
    Literal lit
)

See also: model See ipamir2022 for more details.

function val_objective¶

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

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::val_objective () const = 0

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.

function ~NonIncrMaxSatSolver¶

Paramita::NonIncrMaxSatSolver::~NonIncrMaxSatSolver () override