SAT solver based on CaDiCal. More...

#include <CadicalSatSolver.h>

Inheritance diagram for dlinear::CadicalSatSolver:

Public Member Functions
void	AddLiteral (const Literal &l, bool learned) override
	Add a literal `l` to the SAT solver.

void	AddLearnedClause (const LiteralSet &literals) override
	Given a clause = {f₁, ..., fₙ}, adds a clause (¬f₁ ∨ ... ∨ ¬ fₙ) to the solver.

void	AddLearnedClause (const Literal &lit) override
	Given a clause = {f}, adds a clause (¬f) to the solver.

void	MakeSatVar (const Variable &var) override
	Add a variable to the internal SAT solver.

std::optional< Model >	CheckSat () override
	Check the satisfiability of the current configuration.

void	FixedTheoryLiterals (LiteralSet &fixed_literals) override
	Get the theory literals that are fixed in the current configuration.

void	Assume (const Literal &l) override
	Assumption a literals to be fixed for the next iteration.

void	Assume (const LiteralSet &literals)
	Assumption a set of `literals` to be fixed for the next iteration.

LiteralSet	FixedTheoryLiterals ()
	Get the theory literals that are fixed in the current configuration.

Public Member Functions inherited from dlinear::SatSolver
	SatSolver (PredicateAbstractor &predicate_abstractor, const std::string &class_name="SatSolver")
	Construct a new SatSolver object.

void	AddFormula (const Formula &f)
	Add a formula `f` to the solver.

void	AddFormulas (const std::vector< Formula > &formulas)
	Add the `formulas` to the solver.

void	AddClause (const Formula &f)
	Add a formula `f` to the solver.

void	AddClauses (const std::vector< Formula > &formulas)
	Add a vector of formulas `formulas` to the solver.

LiteralSet	FixedTheoryLiterals ()
	Get the theory literals that are fixed in the current configuration.

void	Assume (const LiteralSet &literals)
	Assumption a set of `literals` to be fixed for the next iteration.

void	MarkAsCnfVariable (const Variable &var)
	Mark `var` as a CNF variable.

const IterationStats &	stats () const
	Get read-only access to the statistics of the SAT solver.

const IterationStats &	cnfizer_stats () const
	Get read-only access to the statistics of the cnfizer of the SAT solver.

const PredicateAbstractor &	predicate_abstractor () const
	Get read-only access to the predicate abstractor of the SAT solver.

Protected Member Functions
void	AddClauseToSat (const Formula &f) override
	Add a clause `f` to the internal SAT solver.

Protected Member Functions inherited from dlinear::SatSolver
void	AddLiteral (const Formula &f)
	Add a formula `f` to the solver.

void	GetMainActiveLiterals (std::set< int > &lits) const
	Get a set of the currently active literals in the clauses, ignoring those required by learned clauses.

Model	OnSatResult ()
	If the SAT solver returns SAT, this function can be used to obtain a model for the formula.

void	UpdateLookup (int lit)
	Update data structures used to minimize the number of assigned literals the theory solver has to verify.

Private Member Functions
std::set< int >	GetMainActiveLiterals () override
	Get a set of the currently active literals in the clauses, ignoring those required by learned clauses.

Private Attributes
CaDiCaL::Solver	sat_ {}
	SAT solver.

int	next_var_id_ {1}
	Next variable id.

Additional Inherited Members
Protected Attributes inherited from dlinear::SatSolver
const Config &	config_
	Configuration of the SAT solver.

std::vector< int >	main_clauses_copy_
	Store the main clauses to restore them after the SAT solver call.

std::map< int, std::set< std::size_t > >	main_clause_lookup_
	Lookup table for literals in the main clauses.

std::size_t	cur_clause_start_
	Index of the first clause added by the SAT solver.

ScopedUnorderedMap< Variable::Id, int >	var_to_sat_
	Map symbolic::Variable → int (Variable type in PicoSat).

ScopedUnorderedMap< int, Variable >	sat_to_var_
	Map int (Variable type in PicoSat) → symbolic::Variable.

ScopedUnorderedSet< Variable::Id >	cnf_variables_
	Set of temporary Boolean variables introduced by CNF transformations.

PlaistedGreenbaumCnfizer	cnfizer_
	Converts the formula to CNF.

PredicateAbstractor &	predicate_abstractor_
	Converts the theory literals to boolean variables.

IterationStats	stats_
	Statistics for the solver.

Detailed Description

SAT solver based on CaDiCal.

CaDiCal is a SAT solver written in C++.

Definition at line 30 of file CadicalSatSolver.h.

Member Function Documentation

◆ AddClauseToSat()

void dlinear::CadicalSatSolver::AddClauseToSat ( const Formula & f )

overrideprotectedvirtual

Add a clause f to the internal SAT solver.

Precondition: f must be a clause. That is, it is either a literal (b or ¬b) or a disjunction of literals (l₁ ∨ ... ∨ lₙ).

Parameters

f	clause to add

Implements dlinear::SatSolver.

Definition at line 88 of file CadicalSatSolver.cpp.

◆ AddLearnedClause() [1/2]

void dlinear::CadicalSatSolver::AddLearnedClause ( const Literal & literals )

overridevirtual

Given a clause = {f}, adds a clause (¬f) to the solver.

Parameters

literals literals to add as the inverted clause

Implements dlinear::SatSolver.

Definition at line 42 of file CadicalSatSolver.cpp.

◆ AddLearnedClause() [2/2]

void dlinear::CadicalSatSolver::AddLearnedClause ( const LiteralSet & literals )

overridevirtual

Given a clause = {f₁, ..., fₙ}, adds a clause (¬f₁ ∨ ... ∨ ¬ fₙ) to the solver.

Parameters

literals literals to add as the inverted clause

Implements dlinear::SatSolver.

Definition at line 38 of file CadicalSatSolver.cpp.

◆ AddLiteral()

void dlinear::CadicalSatSolver::AddLiteral	(	const Literal &	l,
		bool	learned )

overridevirtual

Add a literal l to the SAT solver.

If the literal is learned, it is added to the learned clause set and won't be used by the theory solver.

Parameters

l	literal to add
learned	whether the literal is learned or was in the original formula

Implements dlinear::SatSolver.

Definition at line 47 of file CadicalSatSolver.cpp.

◆ Assume() [1/2]

void dlinear::CadicalSatSolver::Assume ( const Literal & lit )

overridevirtual

Assumption a literals to be fixed for the next iteration.

The lit is temporarily added to the solver with the indicated value.

Note: The solver will not remember the assumption after the next call to CheckSat.

Parameters

lit	literal to assume

Implements dlinear::SatSolver.

Definition at line 110 of file CadicalSatSolver.cpp.

◆ Assume() [2/2]

void dlinear::SatSolver::Assume ( const LiteralSet & literals )

Assumption a set of literals to be fixed for the next iteration.

The literals are temporarily added to the solver with the indicated value.

Note: The solver will not remember the assumptions after the next call to CheckSat.

Parameters

literals set of literals to assume

Definition at line 125 of file SatSolver.cpp.

◆ CheckSat()

std::optional< Model > dlinear::CadicalSatSolver::CheckSat ( )

overridevirtual

Check the satisfiability of the current configuration.

Returns: a witness, satisfying model if the problem is SAT.; empty optional if UNSAT

Implements dlinear::SatSolver.

Definition at line 68 of file CadicalSatSolver.cpp.

◆ FixedTheoryLiterals() [1/2]

LiteralSet dlinear::SatSolver::FixedTheoryLiterals ( )

Get the theory literals that are fixed in the current configuration.

This means that, for the model to be sat, these literals will never change their assignment. This allows for slight optimizations (e.g. their bound can be computed once, at the beginning of the run instead of at each iteration)

Returns: set of literals that are fixed

Definition at line 107 of file SatSolver.cpp.

◆ FixedTheoryLiterals() [2/2]

void dlinear::CadicalSatSolver::FixedTheoryLiterals ( LiteralSet & fixed_literals )

overridevirtual

Get the theory literals that are fixed in the current configuration.

This means that, for the model to be sat, these literals will never change their assignment. This allows for slight optimizations (e.g. their bound can be computed once, at the beginning of the run instead of at each iteration)

Parameters

[out] fixed_literals set of literals that are fixed

Implements dlinear::SatSolver.

Definition at line 101 of file CadicalSatSolver.cpp.

◆ GetMainActiveLiterals()

std::set< int > dlinear::CadicalSatSolver::GetMainActiveLiterals ( )

nodiscardoverrideprivatevirtual

Get a set of the currently active literals in the clauses, ignoring those required by learned clauses.

Here literals are expressed as integers, where the sign indicates whether the literal is negated or not.

Returns: set of literals

Implements dlinear::SatSolver.

Definition at line 57 of file CadicalSatSolver.cpp.

◆ MakeSatVar()

void dlinear::CadicalSatSolver::MakeSatVar ( const Variable & var )

overridevirtual

Add a variable to the internal SAT solver.

Also update the two mapping between each symbolic Variable and the internal SAT solver's variable (var_to_sat_) and the other way around (sat_to_var_). If the variable had already been mapped, this function does nothing.

Parameters

var	variable to add

Implements dlinear::SatSolver.

Definition at line 25 of file CadicalSatSolver.cpp.

The documentation for this class was generated from the following files:

dlinear/solver/CadicalSatSolver.h
dlinear/solver/CadicalSatSolver.cpp

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ AddClauseToSat()

◆ AddLearnedClause() [1/2]

◆ AddLearnedClause() [2/2]

◆ AddLiteral()

◆ Assume() [1/2]

◆ Assume() [2/2]

◆ CheckSat()

◆ FixedTheoryLiterals() [1/2]

◆ FixedTheoryLiterals() [2/2]

◆ GetMainActiveLiterals()

◆ MakeSatVar()