SAT Solvers

Different Classes for SAT formula processing. More...

Collaboration diagram for SAT Solvers:

Topics
	Preprocessing Techniques
	Different Classes for SAT Formula preprocessing.
	CDCL Solvers
	Different Classes for CDCL (Conflict-Driven Clause Learning) solvers interaction.
	Local Search Solvers
	Different Classes for Local Search solver interaction.

Classes
class	SolverFactory
	Factory class for creating and managing SAT solvers. More...
class	SolverInterface
	Interface for a SAT solver with standard features. More...

Typedefs
using	SeedGenerator = std::function<int(SolverInterface*)>

Enumerations
enum class	SatResult { SatResult::SAT = 10 , SatResult::UNSAT = 20 , SatResult::TIMEOUT = 30 , SatResult::UNKNOWN = 0 }
	Enumeration for SAT solver results. More...
enum class	SolverAlgorithmType {   SolverAlgorithmType::CDCL = 0 , SolverAlgorithmType::LOCAL_SEARCH = 1 , SolverAlgorithmType::LOOK_AHEAD = 2 , SolverAlgorithmType::OTHER = 3 ,   SolverAlgorithmType::UNKNOWN = 255 }
	Enumeration for types of solver algorithms. More...

Detailed Description

Different Classes for SAT formula processing.

Enumeration Type Documentation

SatResult

enum class SatResult

strong

Enumeration for SAT solver results.

Enumerator
SAT	Satisfiable
UNSAT	Unsatisfiable
TIMEOUT	Timeout occurred
UNKNOWN	Unknown result

SolverAlgorithmType

enum class SolverAlgorithmType

strong

Enumeration for types of solver algorithms.

Enumerator
CDCL	Conflict-Driven Clause Learning
LOCAL_SEARCH	Local Search
LOOK_AHEAD	Look-Ahead
OTHER	Other algorithm types
UNKNOWN	Unknown algorithm type