#include <bop_ls.h>

Public Member Functions
	SatWrapper (sat::SatSolver *sat_solver)

	SatWrapper (const SatWrapper &)=delete
	This type is neither copyable nor movable.

SatWrapper &	operator= (const SatWrapper &)=delete

std::vector< sat::Literal >	FullSatTrail () const
	Returns the current state of the solver propagation trail.

bool	IsModelUnsat () const

const sat::VariablesAssignment &	SatAssignment () const
	Return the current solver VariablesAssignment.

int	ApplyDecision (sat::Literal decision_literal, std::vector< sat::Literal > *propagated_literals)

void	BacktrackOneLevel ()
	Backtracks the last decision if any.

void	BacktrackAll ()
	Bactracks all the decisions.

void	ExtractLearnedInfo (LearnedInfo *info)
	Extracts any new information learned during the search.

double	deterministic_time () const

Detailed Description

This class is used to ease the connection with the SAT solver.

Todo: (user): remove? the meat of the logic is used in just one place, so I am not sure having this extra layer improve the readability.

Definition at line 63 of file bop_ls.h.

Constructor & Destructor Documentation

◆ SatWrapper() [1/2]

operations_research::bop::SatWrapper::SatWrapper ( sat::SatSolver * sat_solver )

explicit

SatWrapper

Definition at line 655 of file bop_ls.cc.

◆ SatWrapper() [2/2]

operations_research::bop::SatWrapper::SatWrapper ( const SatWrapper & )

delete

This type is neither copyable nor movable.

Member Function Documentation

◆ ApplyDecision()

int operations_research::bop::SatWrapper::ApplyDecision	(	sat::Literal	decision_literal,
		std::vector< sat::Literal > *	propagated_literals )

Applies the decision that makes the given literal true and returns the number of decisions to backtrack due to conflicts if any. Two cases:

No conflicts: Returns 0 and fills the propagated_literals with the literals that have been propagated due to the decision including the the decision itself.
Conflicts: Returns the number of decisions to backtrack (the current decision included, i.e. returned value > 0) and fills the propagated_literals with the literals that the conflicts propagated.
Note
the decision variable should not be already assigned in SAT.

Return the propagated literals, whenever there is a conflict or not. In case of conflict, these literals will have to be added to the last decision point after backtrack.

Definition at line 668 of file bop_ls.cc.

◆ BacktrackAll()

void operations_research::bop::SatWrapper::BacktrackAll ( )

Bactracks all the decisions.

Definition at line 657 of file bop_ls.cc.

◆ BacktrackOneLevel()

void operations_research::bop::SatWrapper::BacktrackOneLevel ( )

Backtracks the last decision if any.

Definition at line 694 of file bop_ls.cc.

◆ deterministic_time()

double operations_research::bop::SatWrapper::deterministic_time ( ) const

Returns a deterministic number that should be correlated with the time spent in the SAT wrapper. The order of magnitude should be close to the time in seconds.

Definition at line 705 of file bop_ls.cc.

◆ ExtractLearnedInfo()

void operations_research::bop::SatWrapper::ExtractLearnedInfo ( LearnedInfo * info )

Extracts any new information learned during the search.

Definition at line 701 of file bop_ls.cc.

◆ FullSatTrail()

std::vector< sat::Literal > operations_research::bop::SatWrapper::FullSatTrail ( ) const

Returns the current state of the solver propagation trail.

Definition at line 659 of file bop_ls.cc.

◆ IsModelUnsat()

bool operations_research::bop::SatWrapper::IsModelUnsat ( ) const

inline

Returns true if the problem is UNSAT.

Note: an UNSAT problem might not be marked as UNSAT at first because the SAT solver is not able to prove it; After some decisions / learned conflicts, the SAT solver might be able to prove UNSAT and so this will return true.

Definition at line 79 of file bop_ls.h.

◆ operator=()

SatWrapper & operations_research::bop::SatWrapper::operator= ( const SatWrapper & )