StructuredBVA Class Reference

Structured Binary Variable Addition (SBVA) preprocessing algorithm. More...

#include <StructuredBva.hpp>

Inheritance diagram for StructuredBVA:

Collaboration diagram for StructuredBVA:

Public Member Functions
	StructuredBVA (int _id, unsigned long maxReplacements, bool shuffleTies)
	Constructor.
	~StructuredBVA ()
	Destructor.
unsigned int	getVariablesCount () override
	Get the current number of variables.
void	setSolverInterrupt () override
	Interrupt resolution, solving cannot continue until interrupt is unset.
void	unsetSolverInterrupt () override
	Remove the SAT solving interrupt request.
SatResult	solve (const std::vector< int > &cube={}) override
	Solve the formula with a given cube.
void	addInitialClauses (const std::vector< simpleClause > &clauses, unsigned int nbVariables) override
	Add a list of initial clauses to the formula.
void	loadFormula (const char *filename) override
	Load formula from a given dimacs file.
void	printStatistics () override
	Print solver statistics.
std::vector< simpleClause >	getSimplifiedFormula () override
	Get the simplified formula after preprocessing.
PreprocessorStats	getPreprocessorStatistics ()
	Get statistics about the preprocessing.
int	getDivisionVariable ()
	Get a variable suitable for search splitting.
void	addClause (ClauseExchangePtr clause)
	Add a permanent clause to the formula.
void	addClauses (const std::vector< ClauseExchangePtr > &clauses)
	Add a list of permanent clauses to the formula.
void	diversify (const SeedGenerator &getSeed=[](SolverInterface *s) { return s->getSolverId();})
	Diversify the preprocessor's behavior.
void	updateAdjacencyMatrix (int var)
unsigned int	getThreeHopHeuristic (int lit1, int lit2)
int	leastFrequentLiteral (simpleClause &clause, int lit)
void	setTieBreakHeuristic (SBVATieBreak tieBreak)
void	releaseMemory ()
	Release memory used by the preprocessor.
void	restoreModel (std::vector< int > &model) override
	Restore the model by removing added clauses.
int	threeHopTieBreak (const std::vector< int > &ties, const int currentLit)
int	mostOccurTieBreak (const std::vector< int > &ties, const int currentLit)
int	leastOccurTieBreak (const std::vector< int > &ties, const int currentLit)
int	randomTieBreak (const std::vector< int > &ties, const int currentLit)
std::vector< int >	getModel () override
	Return the model in case of SAT result.
Public Member Functions inherited from PreprocessorInterface
	PreprocessorInterface (PreprocessorAlgorithm algo, int id)
	Constructor for PreprocessorInterface.
Public Member Functions inherited from SolverInterface
virtual void	printWinningLog ()
	Print the winning log.
bool	isInitialized ()
	Check if the solver is initialized.
void	setInitialized (bool value)
	Set the initialization status of the solver.
SolverAlgorithmType	getAlgoType ()
	Get the algorithm type of the solver.
unsigned int	getSolverTypeId ()
	Get the solver type ID.
void	setSolverTypeId (unsigned int typeId)
	Set the solver type ID.
unsigned int	getSolverId ()
	Get the solver ID.
void	setSolverId (unsigned int id)
	Set the solver ID.
unsigned int	getSolverTypeCount () const
	Get the current count of instances of this object's most-derived type.
	SolverInterface (SolverAlgorithmType algoType, int solverId)
	Constructor for SolverInterface.
virtual	~SolverInterface ()
	Virtual destructor for SolverInterface.

Additional Inherited Members
Protected Member Functions inherited from SolverInterface
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.
Static Protected Member Functions inherited from SolverInterface
template<typename Derived >
static unsigned int	getAndIncrementTypeCount ()
	Get and increment the instance count for a specific derived type.
Protected Attributes inherited from SolverInterface
SolverAlgorithmType	m_algoType
std::atomic< bool >	m_initialized
unsigned int	m_solverTypeId
int	m_solverId
Static Protected Attributes inherited from SolverInterface
static std::unordered_map< std::type_index, std::atomic< unsigned int > >	s_instanceCounts
	Number of existing instances of derived classes.

Detailed Description

Structured Binary Variable Addition (SBVA) preprocessing algorithm.

This class implements the Structured BVA preprocessing technique for SAT solving. It is based on the original implementation from https://github.com/hgarrereyn/SBVA, reorganized and adapted for this solver framework.

Member Function Documentation

addClause()

void StructuredBVA::addClause ( ClauseExchangePtr clause )

inlinevirtual

Add a permanent clause to the formula.

Parameters

clause

The clause to add.

Implements SolverInterface.

addClauses()

void StructuredBVA::addClauses ( const std::vector< ClauseExchangePtr > & clauses )

inlinevirtual

Add a list of permanent clauses to the formula.

Parameters

clauses

The list of clauses to add.

Implements SolverInterface.

addInitialClauses()

void StructuredBVA::addInitialClauses ( const std::vector< simpleClause > & clauses, unsigned int nbVars )

overridevirtual

Add a list of initial clauses to the formula.

Parameters

clauses	The list of initial clauses.
nbVars	The number of variables.

Implements SolverInterface.

diversify()

void StructuredBVA::diversify ( const SeedGenerator & getSeed = [](SolverInterface *s) { return s->getSolverId();} )

virtual

Diversify the preprocessor's behavior.

Parameters

getSeed

Function to get a random seed (default uses solver ID).

Implements SolverInterface.

getDivisionVariable()

int StructuredBVA::getDivisionVariable ( )

inlinevirtual

Get a variable suitable for search splitting.

Returns

The division variable.

Implements SolverInterface.

getModel()

std::vector< int > StructuredBVA::getModel ( )

inlineoverridevirtual

Return the model in case of SAT result.

Returns

The model as a vector of integers.

Implements SolverInterface.

getPreprocessorStatistics()

PreprocessorStats StructuredBVA::getPreprocessorStatistics ( )

inlinevirtual

Get statistics about the preprocessing.

Returns

A PreprocessorStats object containing statistics.

Implements PreprocessorInterface.

getSimplifiedFormula()

std::vector< simpleClause > StructuredBVA::getSimplifiedFormula ( )

overridevirtual

Get the simplified formula after preprocessing.

Returns

A vector of simplified clauses.

Implements PreprocessorInterface.

getVariablesCount()

unsigned int StructuredBVA::getVariablesCount ( )

overridevirtual

Get the current number of variables.

Returns

The number of variables.

Implements SolverInterface.

loadFormula()

void StructuredBVA::loadFormula ( const char * filename )

overridevirtual

Load formula from a given dimacs file.

Parameters

filename

The name of the file to load from.

Implements SolverInterface.

printStatistics()

void StructuredBVA::printStatistics ( )

overridevirtual

Print solver statistics.

Reimplemented from SolverInterface.

releaseMemory()

void StructuredBVA::releaseMemory ( )

inlinevirtual

Release memory used by the preprocessor.

Implements PreprocessorInterface.

restoreModel()

void StructuredBVA::restoreModel ( std::vector< int > & model )

inlineoverridevirtual

Restore the model by removing added clauses.

Parameters

model

The model to be restored.

Implements PreprocessorInterface.

setSolverInterrupt()

void StructuredBVA::setSolverInterrupt ( )

overridevirtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

solve()

SatResult StructuredBVA::solve ( const std::vector< int > & cube = {} )

overridevirtual

Solve the formula with a given cube.

Parameters

cube	The cube to solve with.

Returns

The result of the solving process.

Implements SolverInterface.

unsetSolverInterrupt()

void StructuredBVA::unsetSolverInterrupt ( )

overridevirtual

Remove the SAT solving interrupt request.

Implements SolverInterface.

---

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

• /github/workspace/src/preprocessors/StructuredBva.hpp