Base class for SAT solvers. More...

#include <SatSolver.h>

Inheritance diagram for dlinear::SatSolver:

Public Member Functions
	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.

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

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

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

virtual void	FixedTheoryLiterals (LiteralSet &fixed_literals)=0
	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.

virtual void	Assume (const Literal &lit)=0
	Assumption a literals to be fixed for the next iteration.

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

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

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
virtual void	AddClauseToSat (const Formula &f)=0
	Add a clause `f` to the internal SAT solver.

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

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

virtual void	AddLiteral (const Literal &l, bool learned)=0
	Add a literal `l` to the SAT solver.

virtual std::set< int >	GetMainActiveLiterals ()=0
	Get a set of the currently active literals in the clauses, ignoring those required by learned clauses.

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.

Protected Attributes
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

Base class for SAT solvers.

The SAT solver's role is to convert a generic formula into a CNF of boolean clauses, abstracting away the theory literals. Then, it checks the satisfiability of the CNF. If the CNF is satisfiable, it returns a model for the formula. Otherwise, it returns an empty optional. The SAT solver can learn clauses during the solving process, guided by the theory solver.

See also: TheorySolver

Definition at line 38 of file SatSolver.h.

Constructor & Destructor Documentation

◆ SatSolver()

dlinear::SatSolver::SatSolver	(	PredicateAbstractor &	predicate_abstractor,
		const std::string &	class_name = "SatSolver" )

explicit

Construct a new SatSolver object.

The predicate_abstractor is shared between the theory solver and the SAT solver, in order to have a common understanding of the literals. The class_name is used to identify the theory solver in the logs.

Note: The predicate abstractor will share its configuration with the SAT solver.

Parameters

class_name	name of the subclass of the SAT solver used
predicate_abstractor	predicate abstractor linking boolean literals to theory literals

See also: TheorySolver

Definition at line 17 of file SatSolver.cpp.

Member Function Documentation

◆ AddClause()

void dlinear::SatSolver::AddClause ( const Formula & f )

Add a formula f to the solver.

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

Parameters

f	formula to add

Definition at line 63 of file SatSolver.cpp.

◆ AddClauses()

void dlinear::SatSolver::AddClauses ( const std::vector< Formula > & formulas )

Add a vector of formulas formulas to the solver.

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

Parameters

formulas vector of formulas to add

Definition at line 59 of file SatSolver.cpp.

◆ AddClauseToSat()

virtual void dlinear::SatSolver::AddClauseToSat ( const Formula & f )

protectedpure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ AddFormula()

void dlinear::SatSolver::AddFormula ( const Formula & f )

Add a formula f to the solver.

Note: If f is a clause, please use AddClause function. This function does not assume anything about f and perform pre-processing (CNFize and PredicateAbstraction).

Parameters

f	formula to add

Definition at line 42 of file SatSolver.cpp.

◆ AddFormulas()

void dlinear::SatSolver::AddFormulas ( const std::vector< Formula > & formulas )

Add the formulas to the solver.

Parameters

formulas vector of formulas to add

Definition at line 55 of file SatSolver.cpp.

◆ AddLearnedClause() [1/2]

virtual void dlinear::SatSolver::AddLearnedClause ( const Literal & literals )

pure virtual

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

Parameters

literals literals to add as the inverted clause

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ AddLearnedClause() [2/2]

virtual void dlinear::SatSolver::AddLearnedClause ( const LiteralSet & literals )

pure virtual

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

Parameters

literals literals to add as the inverted clause

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ AddLiteral() [1/2]

void dlinear::SatSolver::AddLiteral ( const Formula & f )

protected

Add a formula f to the solver.

f must be a Boolean variable or a negation of Boolean variable (b or ¬b).

Parameters

f	formula to add

Definition at line 71 of file SatSolver.cpp.

◆ AddLiteral() [2/2]

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

protectedpure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ Assume() [1/2]

virtual void dlinear::SatSolver::Assume ( const Literal & lit )

pure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ 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 88 of file SatSolver.cpp.

◆ CheckSat()

virtual std::optional< Model > dlinear::SatSolver::CheckSat ( )

pure virtual

Check the satisfiability of the current configuration.

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ cnfizer_stats()

const IterationStats & dlinear::SatSolver::cnfizer_stats ( ) const

nodiscard

Get read-only access to the statistics of the cnfizer of the SAT solver.

Returns: statistics of the cnfizer of the SAT solver

Definition at line 24 of file SatSolver.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 83 of file SatSolver.cpp.

◆ FixedTheoryLiterals() [2/2]

virtual void dlinear::SatSolver::FixedTheoryLiterals ( LiteralSet & fixed_literals )

pure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ GetMainActiveLiterals() [1/2]

virtual std::set< int > dlinear::SatSolver::GetMainActiveLiterals ( )

protectedpure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ GetMainActiveLiterals() [2/2]

void dlinear::SatSolver::GetMainActiveLiterals ( std::set< int > & lits ) const

protected

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. This method is called from GetMainActiveLiterals. The set of literals is updated by reference.

Parameters

[out] lits set of literals

Definition at line 97 of file SatSolver.cpp.

◆ MakeSatVar()

virtual void dlinear::SatSolver::MakeSatVar ( const Variable & var )

protectedpure virtual

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

Implemented in dlinear::CadicalSatSolver, and dlinear::PicosatSatSolver.

◆ MarkAsCnfVariable()

void dlinear::SatSolver::MarkAsCnfVariable ( const Variable & var )

Mark var as a CNF variable.

It won't be present in the model produced by the SAT solver.

Parameters

var	variable to mark

Definition at line 81 of file SatSolver.cpp.

◆ OnSatResult()

Model dlinear::SatSolver::OnSatResult ( )

protected

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

Returns: model returned by the SAT solver

Definition at line 130 of file SatSolver.cpp.

◆ predicate_abstractor()

const PredicateAbstractor & dlinear::SatSolver::predicate_abstractor ( ) const

inlinenodiscard

Get read-only access to the predicate abstractor of the SAT solver.

Returns: predicate abstractor of the SAT solver

Definition at line 154 of file SatSolver.h.

◆ stats()

const IterationStats & dlinear::SatSolver::stats ( ) const

inlinenodiscard

Get read-only access to the statistics of the SAT solver.

Returns: statistics of the SAT solver

Definition at line 150 of file SatSolver.h.

◆ UpdateLookup()

void dlinear::SatSolver::UpdateLookup ( int lit )

protected

Update data structures used to minimize the number of assigned literals the theory solver has to verify.

Parameters

lit	literal from the SAT solver

Definition at line 92 of file SatSolver.cpp.

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

dlinear/solver/SatSolver.h
dlinear/solver/SatSolver.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ SatSolver()

Member Function Documentation

◆ AddClause()

◆ AddClauses()

◆ AddClauseToSat()

◆ AddFormula()

◆ AddFormulas()

◆ AddLearnedClause() [1/2]

◆ AddLearnedClause() [2/2]

◆ AddLiteral() [1/2]

◆ AddLiteral() [2/2]

◆ Assume() [1/2]

◆ Assume() [2/2]

◆ CheckSat()

◆ cnfizer_stats()

◆ FixedTheoryLiterals() [1/2]

◆ FixedTheoryLiterals() [2/2]

◆ GetMainActiveLiterals() [1/2]

◆ GetMainActiveLiterals() [2/2]

◆ MakeSatVar()

◆ MarkAsCnfVariable()

◆ OnSatResult()

◆ predicate_abstractor()

◆ stats()

◆ UpdateLookup()