SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields
smtrat::mcsat::fm::MinVarCountComparator Struct Reference

This heuristic tries to minimize the number of variables occuring in the explanation. More...

#include <ConflictGenerator.h>

Public Member Functions

bool operator() (const Bound &b1, const Bound &b2) const
 

Data Fields

bool symmetric = false
 

Detailed Description

This heuristic tries to minimize the number of variables occuring in the explanation.

It is a 2-approximation to the lowest possible number of variables in an explanation.

Definition at line 324 of file ConflictGenerator.h.

Member Function Documentation

◆ operator()()

bool smtrat::mcsat::fm::MinVarCountComparator::operator() ( const Bound &  b1,
const Bound &  b2 
) const
inline

Definition at line 327 of file ConflictGenerator.h.

Field Documentation

◆ symmetric

bool smtrat::mcsat::fm::MinVarCountComparator::symmetric = false

Definition at line 325 of file ConflictGenerator.h.

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