[ sat4j-Bugs-304554 ] Problem with isAssertive

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Bugs item #304554, was opened at 25/01/2006 15:45
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=304554&group_id=228

Category: pseudo boolean
Group: ongoing version (cvs)
>Status: Closed
Resolution: None
Priority: 7
Submitted By: Daniel Le Berre (leberre)
Assigned to: Anne Parrain (parrain)
Summary: Problem with isAssertive

Initial Comment:
80% of the time spent when solving pigeon hole problems relates to
isAssertive() method:


boolean isAssertive(int dl) {
        BigInteger slack = BigInteger.ZERO;
        for (Integer i : coefs.keySet()) {
            if ((coefs.get(i).signum() > 0)
                    && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl)))
                slack = slack.add(coefs.get(i));
        }
        slack = slack.subtract(degree);
        if (slack.signum() < 0)
            return false;
        for (Integer i : coefs.keySet()) {
            if ((coefs.get(i).signum() > 0)
                    && (voc.isUnassigned(i) || voc.getLevel(i) >= dl)
                    && (slack.subtract(coefs.get(i)).signum() < 0))
                return true;
        }
        return false;
    }


We need to find a way to incrementally compute isAssertive.


----------------------------------------------------------------------

Comment By: Laurent Stemmer (stemlaur)
Date: 25/01/2006 16:01

Message:
connecté 
user_id=8598

The problem may come from the huge memory usage from BigInteger:


----------------------------------------------------------------------

You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=304554&group_id=228