Class Paramita::SatSolver¶

An incremental SAT Solver.

Note:

Use SATSOLVER_C_INTERFACE to register any subclass of this interface.

Incremental solvers allow to modify the formula and call solve as many times as needed. After modifying the formula (by adding new clauses), solve with the same parameters (i.e. assumptions, budgets...) can return different values.

#include <SatSolver.hpp>

Inherits the following classes: Paramita::NonIncrSatSolver

Public Static Attributes¶

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

Public Static Attributes inherited from Paramita::NonIncrSatSolver¶

See Paramita::NonIncrSatSolver

Type	Name
constexpr const char *const	m_interface_id = `/* multi line expression */`

Public Static Attributes inherited from Paramita::ClauseContainer¶

See Paramita::ClauseContainer

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

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
	SatSolver () = default
	SatSolver (const SatSolver &) = delete
	SatSolver (SatSolver &&) = delete
virtual	add_observed_var (int var) Marks a variable as observed by the external propagator.
virtual SatSolver *	clone () override Clones the incremental SAT solver.
virtual	connect_external_propagator (std::shared_ptr< Paramita::Propagator > propagator) Connects an external `Propagator` to the solver.
virtual	connect_learner (std::shared_ptr< Paramita::Learner > learner) Connects a `Learner` to the solver.
virtual	disconnect_external_propagator () Disconnects the currently connected external propagator.
virtual	disconnect_learner () Disconnects the currently connected learner.
virtual	force_backtrack (int new_level) Forces the solver to backtrack.
virtual bool	is_decision (int lit) Checks whether a literal is assigned as a decision.
SatSolver &	operator= (const SatSolver & container) = delete
SatSolver &	operator= (SatSolver &&) = delete
virtual	remove_observed_var (int var) Stops observing a variable.
virtual	reset_observed_vars () Removes all observed variables.
	~SatSolver () override

Public Functions inherited from Paramita::NonIncrSatSolver¶

See Paramita::NonIncrSatSolver

Type	Name
	NonIncrSatSolver () = default
	NonIncrSatSolver (const NonIncrSatSolver &) = delete Deleted copy constructor (pure interface).
	NonIncrSatSolver (NonIncrSatSolver &&) = delete Deleted move constructor (pure interface).
virtual	assume (Literal lit) Add an assumption for the next `solve` or`propagate` call.
virtual NonIncrSatSolver *	clone () override Clones the SAT solver.
virtual std::vector< Literal >	core () Retrieve the unsatisfiable core.
virtual bool	failed (Literal lit) Check if a literal belongs to the unsatisfiable core.
virtual	freeze (Literal lit) Freeze a variable.
virtual std::optional< bool >	get_phase (Literal lit) Returns the default phase for a decision variable.
virtual	interrupt () Interrupts the resolution process.
virtual std::optional< bool >	is_fixed (Literal lit) Detect if a variable is implied at root level.
virtual bool	is_frozen (Literal lit) Checks if a variable is frozen.
virtual	melt (Literal lit) Melts a variable.
virtual std::vector< Literal >	model () const = 0 Get the model (solution) after solving.
virtual int	num_active_vars () Counts how many variables are active.
virtual long	num_conflicts () Get the number of conflicts encountered.
NonIncrSatSolver &	operator= (const NonIncrSatSolver & container) = delete Deleted copy assignment (pure interface).
NonIncrSatSolver &	operator= (NonIncrSatSolver &&) = delete Deleted move assignment (pure interface).
virtual	phase (Literal lit) Set the default phase for a decision variable during branching.
virtual std::pair< bool, std::vector< Literal > >	propagate (const std::vector< Literal > & assumptions) Propagate the given assumptions.
virtual	simplify (unsigned int num_rounds) Simplify the formula.
virtual std::optional< bool >	solve (const std::vector< Literal > & assumptions, const SolvingBudget & budget) = 0 Solve the underlying formula under the given assumptions.
virtual	unphase (Literal lit) Removes the default phase for a decision variable.
virtual std::optional< bool >	val_lit (Literal lit) Get the truth value for a literal.
	~NonIncrSatSolver () override

Public Functions inherited from Paramita::ClauseContainer¶

See Paramita::ClauseContainer

Type	Name
	ClauseContainer () = default Constructor that initializes an empty container.
	ClauseContainer (const ClauseContainer &) = delete Deleted copy constructor (pure interface).
	ClauseContainer (ClauseContainer &&) = delete Deleted move constructor (pure interface).
virtual	add_clause (const Clause & clause) = 0 Add a single clause.
virtual	add_clauses (const std::vector< Clause > & clauses) Add multiple clauses to the container.
virtual	add_lit (Literal lit) Add a clause literal by literal.
virtual ClauseContainer *	clone () Clones the current CNF Container.
virtual std::uint64_t	max_var () const = 0 Get the largest variable used by the container.
virtual int	num_clauses () const Get the number of clauses hold currently by the container.
ClauseContainer &	operator= (const ClauseContainer & container) = delete Deleted copy assignment (pure interface).
ClauseContainer &	operator= (ClauseContainer &&) = delete Deleted move assignment (pure interface).
virtual	set_minimum_var (std::uint64_t var) = 0 Sets the maximum variable known to the container to at least this one.
	~ClauseContainer () override Virtual destructor for the container.

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::SatSolver::m_interface_id;

Public Functions Documentation¶

function SatSolver [1/3]¶

Paramita::SatSolver::SatSolver () = default

function SatSolver [2/3]¶

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

function SatSolver [3/3]¶

Paramita::SatSolver::SatSolver (
    SatSolver &&
) = delete

function add_observed_var¶

Marks a variable as observed by the external propagator.

virtual Paramita::SatSolver::add_observed_var (
    int var
)

The solver notifies the propagator about assignments involving observed variables.

Parameters:

var The variable to observe.

function clone¶

Clones the incremental SAT solver.

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

Returns:

The cloned incremental SAT solver.

Exception:

UnsupportedMethodException This method is optional.

Implements Paramita::NonIncrSatSolver::clone

function connect_external_propagator¶

Connects an external Propagator to the solver.

virtual Paramita::SatSolver::connect_external_propagator (
    std::shared_ptr< Paramita::Propagator > propagator
)

The propagator receives notifications about the solver state and may perform external propagation, suggest branching decisions, reject candidate models, and add external clauses.

Only one propagator can be connected at a time. Connecting a new propagator replaces any previously connected propagator.

Parameters:

propagator The propagator to connect.

function connect_learner¶

Connects a Learner to the solver.

virtual Paramita::SatSolver::connect_learner (
    std::shared_ptr< Paramita::Learner > learner
)

The learner receives learnt clauses generated during solving according to its is_relevant() criterion.

Only one learner can be connected at a time. Connecting a new learner replaces any previously connected learner.

Parameters:

learner The learner to connect.

function disconnect_external_propagator¶

Disconnects the currently connected external propagator.

virtual Paramita::SatSolver::disconnect_external_propagator ()

After this call, the solver no longer issues notifications or callbacks to the propagator.

function disconnect_learner¶

Disconnects the currently connected learner.

virtual Paramita::SatSolver::disconnect_learner ()

After this call, learnt clauses are no longer reported.

function force_backtrack¶

Forces the solver to backtrack.

virtual Paramita::SatSolver::force_backtrack (
    int new_level
)

Parameters:

new_level The decision level to backtrack to.

function is_decision¶

Checks whether a literal is assigned as a decision.

virtual bool Paramita::SatSolver::is_decision (
    int lit
)

Parameters:

lit The literal to query.

Returns:

true if the literal is a decision assignment, false otherwise.

function operator=¶

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

function operator=¶

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

function remove_observed_var¶

Stops observing a variable.

virtual Paramita::SatSolver::remove_observed_var (
    int var
)

After this call, assignments to the variable are no longer reported to the external propagator.

Parameters:

var The variable to stop observing.

function reset_observed_vars¶

Removes all observed variables.

virtual Paramita::SatSolver::reset_observed_vars ()

After this call, no variable is observed until new ones are added using add_observed_var().

function ~SatSolver¶

Paramita::SatSolver::~SatSolver () override