Class Paramita::Learner

Interface for components that consume learnt clauses.

A Learner can be attached to a SAT solver to receive learnt clauses generated during the solving process. Implementations can use this information for tasks such as collecting statistics, learning new models, or building heuristics.

Before a learnt clause is reported, the solver calls is_relevant() to determine whether clauses of a given size should be forwarded to the learner.

Note:

Use LEARNER_C_INTERFACE to register any subclass of this interface.

• #include <Learner.hpp>

Inherits the following classes: Paramita::Plugin

Public Static Attributes

Type	Name
constexpr const char *const	m_interface_id = "Paramita::Learner"

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
	Learner () = default
	Learner (const Learner &) = delete Deleted copy constructor (pure interface).
	Learner (Learner &&) = delete Deleted move constructor (pure interface).
virtual bool	is_relevant (int size) = 0 Determines whether a learnt clause is relevant based on its size.
virtual	learnt (const std::vector< int > & clause) = 0 Reports a learnt clause.
Learner &	operator= (const Learner & container) = delete Deleted copy assignment (pure interface).
Learner &	operator= (Learner &&) = delete Deleted move assignment (pure interface).
	~Learner () 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::Learner::m_interface_id;

---

Public Functions Documentation

function Learner [1/3]

Paramita::Learner::Learner () = default

---

function Learner [2/3]

Deleted copy constructor (pure interface).

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

---

function Learner [3/3]

Deleted move constructor (pure interface).

Paramita::Learner::Learner (
    Learner &&
) = delete

---

function is_relevant

Determines whether a learnt clause is relevant based on its size.

virtual bool Paramita::Learner::is_relevant (
    int size
) = 0

The solver calls this method before forwarding a learnt clause. If it returns true, the clause is passed to learnt(). Otherwise, the clause is ignored.

Parameters:

• size The number of literals in the learnt clause.

Returns:

true if learnt clauses of the given size should be reported; false otherwise.

---

function learnt

Reports a learnt clause.

virtual Paramita::Learner::learnt (
    const std::vector< int > & clause
) = 0

This method is called for every learnt clause considered relevant by is_relevant().

Parameters:

• clause The learnt clause represented as a vector of literals.

---

function operator=

Deleted copy assignment (pure interface).

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

---

function operator=

Deleted move assignment (pure interface).

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

---

function ~Learner

Paramita::Learner::~Learner () override

---