Different Classes for CDCL (Conflict-Driven Clause Learning) solvers interaction. More...

Collaboration diagram for CDCL Solvers:

Classes
class	Cadical
	Implements the different interfaces to interact with the Cadical CDCL solver. More...

class	GlucoseSyrup
	Instance of a Glucose solver. More...

class	Kissat
	Instance of a Kissat solver. More...

class	KissatINCSolver
	Instance of a KissatINCSolver solver. More...

class	KissatMABSolver
	Instance of a KissatMABSolver solver. More...

class	Lingeling
	Instance of a Lingeling solver. More...

class	MapleCOMSPSSolver
	Instance of a MapleCOMSPS solver. More...

class	MiniSat
	Instance of a Minisat solver. More...

struct	SolvingCdclStatistics
	Structure for solver statistics. More...

class	SolverCdclInterface
	Interface for CDCL (Conflict-Driven Clause Learning) solvers This class provides a common interface for all CDCL solvers. It inherits from SolverInterface for solving primitives and SharingEntity for sharing primitives. More...

Enumerations
enum class	SolverCdclType { GLUCOSE = 0 , LINGELING = 1 , CADICAL = 2 , MINISAT = 3 , KISSAT = 4 , MAPLECOMSPS = 5 , KISSATMAB = 6 , KISSATINC = 7 }
	Code for the type of solvers.

Detailed Description

Different Classes for CDCL (Conflict-Driven Clause Learning) solvers interaction.

This group provides a common interface for all CDCL solvers.

Classes