Method certifyInfeasibility

src/engine/Engine.cpp:3378–3406

}

bool Engine::certifyInfeasibility( unsigned var ) const
{
    ASSERT( _produceUNSATProofs );

    Vector<double> contradiction = computeContradiction( var );

    if ( contradiction.empty() )
        return FloatUtils::isNegative( _groundBoundManager.getUpperBound( var ) -
                                       _groundBoundManager.getLowerBound( var ) );

    SparseUnsortedList sparseContradiction = SparseUnsortedList();

    contradiction.empty()
        ? sparseContradiction.initializeToEmpty()
        : sparseContradiction.initialize( contradiction.data(), contradiction.size() );

    // In case contradiction is a vector of zeros
    if ( sparseContradiction.empty() )
        return FloatUtils::isNegative( _groundBoundManager.getUpperBound( var ) -
                                       _groundBoundManager.getLowerBound( var ) );

    double derivedBound =
        UNSATCertificateUtils::computeCombinationUpperBound( sparseContradiction,
                                                             _tableau->getSparseA(),
                                                             _groundBoundManager.getUpperBounds(),
                                                             _groundBoundManager.getLowerBounds(),
                                                             _tableau->getN() );
    return FloatUtils::isNegative( derivedBound );
}

double Engine::explainBound( unsigned var, bool isUpper ) const
{