Class Paramita::Propagator

Interface for implementing external propagation.

A Propagator extends the behavior of a SAT solver by maintaining its own state alongside the solver state. The solver notifies the propagator of assignments and backtracking events, and the propagator may in turn:

• Propagate additional literals.
• Provide explanations (reason clauses) for propagated literals.
• Suggest branching decisions.
• Reject candidate models.
• Add external clauses to the solver.

Note:

Use EXTERNAL_PROPAGATOR_C_INTERFACE to register any subclass of this interface.

• #include <Propagator.hpp>

Inherits the following classes: Paramita::Plugin

Public Static Attributes

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

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
	Propagator () = default
	Propagator (const Propagator &) = delete Deleted copy constructor (pure interface).
	Propagator (Propagator &&) = delete Deleted move constructor (pure interface).
virtual bool	check_found_model (const std::vector< int > & model) = 0 Checks whether a candidate model is acceptable.
virtual int	decide () Suggests the next branching literal.
virtual std::vector< int >	get_external_clause () = 0 Returns an external clause to be added to the solver.
virtual OutData::Value	get_out_data (const std::string & key) const
virtual std::vector< std::string >	get_out_data_keys () const
virtual std::vector< int >	get_reason_clause (int propagated_lit) Returns the reason clause for a propagated literal.
virtual bool	has_external_clause () = 0 Indicates whether the propagator has an external clause to add.
virtual	on_assignment (const std::vector< int > & lits) = 0 Notifies the propagator of newly assigned literals.
virtual	on_backtrack (std::size_t new_level) = 0 Notifies the propagator that the solver has backtracked.
virtual	on_new_decision_level () = 0 Notifies the propagator about a new decision level.
Propagator &	operator= (const Propagator & container) = delete Deleted copy assignment (pure interface).
Propagator &	operator= (Propagator &&) = delete Deleted move assignment (pure interface).
virtual std::vector< int >	propagate () Performs external propagation.
	~Propagator () 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::Propagator::m_interface_id;

---

Public Functions Documentation

function Propagator [1/3]

Paramita::Propagator::Propagator () = default

---

function Propagator [2/3]

Deleted copy constructor (pure interface).

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

---

function Propagator [3/3]

Deleted move constructor (pure interface).

Paramita::Propagator::Propagator (
    Propagator &&
) = delete

---

function check_found_model

Checks whether a candidate model is acceptable.

virtual bool Paramita::Propagator::check_found_model (
    const std::vector< int > & model
) = 0

The solver calls this method when it has found a model.

Parameters:

• model The candidate model.

Returns:

true if the model is accepted, false otherwise.

---

function decide

Suggests the next branching literal.

inline virtual int Paramita::Propagator::decide () 

Returning 0 indicates that the propagator does not provide a decision and the solver should use its own branching heuristic.

Returns:

The next decision literal, or 0 if none is suggested.

---

function get_external_clause

Returns an external clause to be added to the solver.

virtual std::vector< int > Paramita::Propagator::get_external_clause () = 0

This method is called only if has_external_clause() returns true.

Returns:

The external clause.

---

function get_out_data

inline virtual OutData::Value Paramita::Propagator::get_out_data (
    const std::string & key
) const

---

function get_out_data_keys

inline virtual std::vector< std::string > Paramita::Propagator::get_out_data_keys () const

---

function get_reason_clause

Returns the reason clause for a propagated literal.

inline virtual std::vector< int > Paramita::Propagator::get_reason_clause (
    int propagated_lit
) 

The returned clause must justify the propagation of propagated_lit.

Parameters:

• propagated_lit The propagated literal.

Returns:

The reason clause.

---

function has_external_clause

Indicates whether the propagator has an external clause to add.

virtual bool Paramita::Propagator::has_external_clause () = 0

Returns:

true if an external clause is available, false otherwise.

---

function on_assignment

Notifies the propagator of newly assigned literals.

virtual Paramita::Propagator::on_assignment (
    const std::vector< int > & lits
) = 0

The propagator should update its internal state to reflect the assignments.

Parameters:

• lits The literals assigned since the previous notification.

---

function on_backtrack

Notifies the propagator that the solver has backtracked.

virtual Paramita::Propagator::on_backtrack (
    std::size_t new_level
) = 0

The propagator should restore its internal state to match the given decision level.

Parameters:

• new_level The decision level after backtracking.

---

function on_new_decision_level

Notifies the propagator about a new decision level.

virtual Paramita::Propagator::on_new_decision_level () = 0

---

function operator=

Deleted copy assignment (pure interface).

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

---

function operator=

Deleted move assignment (pure interface).

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

---

function propagate

Performs external propagation.

inline virtual std::vector< int > Paramita::Propagator::propagate () 

Returns:

A list of literals that should be propagated by the solver.

---

function ~Propagator

Paramita::Propagator::~Propagator () override

---