[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.


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

>Comment By: Pascal Rapicault (pascal)
Date: 2007-11-14 10:43

Message:
Logged In: YES 
user_id=13911

Here is the file. Sorry about that.

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

Comment By: Daniel Le Berre (leberre)
Date: 2007-11-14 09:41

Message:
connecté 
user_id=4369

Pascal, the problem is not attached to the bug report.


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

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