Implementing a Propagator

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

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_new_decision_level

Notifies the propagator about a new decision level.

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

---

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 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_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 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 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_keys

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

---

function get_out_data

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

---