Skip to content

Class Paramita::NonIncrSatSolver

A SAT solver.

Note:

Use SATSOLVER_C_INTERFACE to register any subclass of this interface.

  • #include <NonIncrSatSolver.hpp>

Inherits the following classes: Paramita::ClauseContainer

Public Static Attributes

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
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 orpropagate 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::NonIncrSatSolver::m_interface_id;

Public Functions Documentation

function NonIncrSatSolver [1/3]

Paramita::NonIncrSatSolver::NonIncrSatSolver () = default

function NonIncrSatSolver [2/3]

Deleted copy constructor (pure interface). 

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

function NonIncrSatSolver [3/3]

Deleted move constructor (pure interface). 

Paramita::NonIncrSatSolver::NonIncrSatSolver (
    NonIncrSatSolver &&
) = delete

function assume

Add an assumption for the next solve orpropagate call. 

virtual Paramita::NonIncrSatSolver::assume (
    Literal lit
)

See BALYO201645 for more details.

Exception:

function clone

Clones the SAT solver. 

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

Returns:

The cloned SAT solver.

Exception:

Implements Paramita::ClauseContainer::clone

function core

Retrieve the unsatisfiable core. 

virtual std::vector< Literal > Paramita::NonIncrSatSolver::core ()

Returns:

A vector filled with a subset of the assumptions that are jointly unsatisfiable.

Precondition:

solve was called with assumptions.

Precondition:

The instance must be unsatisfiable under the given assumptions.

Exception:

function failed

Check if a literal belongs to the unsatisfiable core. 

virtual bool Paramita::NonIncrSatSolver::failed (
    Literal lit
)

Parameters:

  • lit The literal to be checked.

Returns:

true if the literal belongs to the unsatisfiable core, false otherwise.

Precondition:

The instance must be unsatisfiable under the given assumptions.

See BALYO201645 for more details.

Exception:

function freeze

Freeze a variable. 

virtual Paramita::NonIncrSatSolver::freeze (
    Literal lit
)

A frozen variable is a variable that is potentially needed in the future (for example, new assumptions). Internally, the solver can decide to perform variable elimination.

A variable can be frozen multiple times, as in Lingeling or CaDiCaL. You must call melt the same number of times to "unfreeze" a variable.

See

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

See also: melt, is_frozen

Exception:

function get_phase

Returns the default phase for a decision variable. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::get_phase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.

Returns:

True if the phase is positive, False if negative, or std::nothing if it was not set.

Exception:

function interrupt

Interrupts the resolution process. 

virtual Paramita::NonIncrSatSolver::interrupt ()

This method instructs the solver to stop solving or propagating. Note that this is a notification, not an immediate stop, when the solver is interrupted is implementation defined.

Precondition:

The solver is solving or propagating.

Postcondition:

After interrupting, the solver must stay in a stable state.

Exception:

function is_fixed

Detect if a variable is implied at root level. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::is_fixed (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

Returns:

True if the variable is implied by the formula, False if its negation is implied, or std::nothing if it has not yet been determined.

Exception:

function is_frozen

Checks if a variable is frozen. 

virtual bool Paramita::NonIncrSatSolver::is_frozen (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

Returns:

See also: freeze, melt

Exception:

function melt

Melts a variable. 

virtual Paramita::NonIncrSatSolver::melt (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

See also: freeze, is_frozen

Exception:

function model

Get the model (solution) after solving. 

virtual std::vector< Literal > Paramita::NonIncrSatSolver::model () const = 0

Returns:

The vector where the solution will be stored. Each element of the vector is a literal that was set to true.

Precondition:

The method solve was called.

Precondition:

A solution was found by solve.

Warning:

Undefined behaviour if solve returned std::nothing.

Exception:

function num_active_vars

Counts how many variables are active. 

virtual int Paramita::NonIncrSatSolver::num_active_vars ()

An active variable is a variable that exists in an irredundant clause (i.e. not satisfied, subsumed, or eliminated). Variable become inactive if they are eliminated or fixed at the root level.

Returns:

The number of active variables.

Exception:

function num_conflicts

Get the number of conflicts encountered. 

virtual long Paramita::NonIncrSatSolver::num_conflicts ()

Returns:

The total number of conflicts found during solve.

Exception:

function operator=

Deleted copy assignment (pure interface). 

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

function operator=

Deleted move assignment (pure interface). 

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

function phase

Set the default phase for a decision variable during branching. 

virtual Paramita::NonIncrSatSolver::phase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable and its phase (positive if we want the phase to be True and negative if we want it to be False).

Exception:

function propagate

Propagate the given assumptions. 

virtual std::pair< bool, std::vector< Literal > > Paramita::NonIncrSatSolver::propagate (
    const std::vector< Literal > & assumptions
)

Parameters:

  • assumptions A list of literals assumed to be true.

Returns:

A pair with a) true if propagation succeeded without a conflict, false if a conflict was found; and b) a vector with the literals propagated as a result of the assumptions. In case the propagation fails, the vector might be empty.

Exception:

function simplify

Simplify the formula. 

virtual Paramita::NonIncrSatSolver::simplify (
    unsigned int num_rounds
)

Parameters:

  • num_rounds The number of simplification rounds to apply.

Exception:

function solve

Solve the underlying formula under the given assumptions. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) = 0

If interrupted, the solver is responsible from clearing the interruption.

See also: interrupt

Parameters:

  • assumptions A vector with literals that will be fixed during this solve call.
  • budget Solving limits for this call.

Precondition:

The method solve was not called previously OR no the formula has not been modified since the last solve call.

Postcondition:

The solving budget is reset to unlimited.

Returns:

An option with a boolean representing the satisfiability status of the formula under the specified assumptions, or std::nullopt if it could not be determined.

function unphase

Removes the default phase for a decision variable. 

virtual Paramita::NonIncrSatSolver::unphase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.

Exception:

function val_lit

Get the truth value for a literal. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::val_lit (
    Literal lit
)

Parameters:

  • lit The literal to check.

Returns:

lit if the literal belongs to the model, -lit if its negation belongs to the model, and 0 if it is not determined.

Precondition:

solve was called.

Precondition:

A solution was found by solve.

See BALYO201645 for more details.

Exception:

function ~NonIncrSatSolver

Paramita::NonIncrSatSolver::~NonIncrSatSolver () override