Class Paramita::MaxSatSolver¶

An incremental MaxSAT solver.

Note:

Use MAXSAT_SOLVER_C_INTERFACE to register any subclass of this interface.

#include <MaxSatSolver.hpp>

Inherits the following classes: Paramita::NonIncrMaxSatSolver

Public Static Attributes¶

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

Public Static Attributes inherited from Paramita::NonIncrMaxSatSolver¶

See 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
	MaxSatSolver () = default
	MaxSatSolver (const MaxSatSolver &) = delete Deleted copy constructor (pure interface).
	MaxSatSolver (MaxSatSolver &&) = delete Deleted copy constructor (pure interface).
virtual MaxSatSolver *	clone () override Clone the current solver.
MaxSatSolver &	operator= (const MaxSatSolver & container) = delete Deleted copy constructor (pure interface).
MaxSatSolver &	operator= (MaxSatSolver &&) = delete Deleted copy constructor (pure interface).
	~MaxSatSolver () override

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

variable m_interface_id¶

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

Public Functions Documentation¶

function MaxSatSolver [1/3]¶

Paramita::MaxSatSolver::MaxSatSolver () = default

function MaxSatSolver [2/3]¶

Deleted copy constructor (pure interface).

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

function MaxSatSolver [3/3]¶

Deleted copy constructor (pure interface).

Paramita::MaxSatSolver::MaxSatSolver (
    MaxSatSolver &&
) = delete

function clone¶

Clone the current solver.

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

Returns:

The cloned solver.

Implements Paramita::WClauseContainer::clone

function operator=¶

Deleted copy constructor (pure interface).

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

function operator=¶

Deleted copy constructor (pure interface).

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

function ~MaxSatSolver¶

Paramita::MaxSatSolver::~MaxSatSolver () override