[sat4j-dev] [ sat4j-Bugs-307847 ] Pseudo boolean solver fails to find optimal solution when tautology is added

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Bugs item #307847, was opened at 2007-11-14 09:20
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=307847&group_id=228

Category: None
Group: None
Status: Open
Resolution: None
Priority: 5
Submitted By: Pascal Rapicault (pascal)
Assigned to: Nobody (None)
Summary: Pseudo boolean solver fails to find optimal solution when tautology 
is added

Initial Comment:
Setup:
 Version: sat4j 1.7
 Solver: newMinimalOPBClauseCardConstrMaxSpecificOrder
 Reader: GoodOPBReader

When I give as input the attached problem to the solver mentioned previously,
the the solution returned is not the minimal one. However if I remove the last
constraint of the problem (+ 1 v1 = 1), the solution returned is the minimal 
one.


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

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