[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 16:58

Message:
Logged In: YES 
user_id=13911

Note that I'm running on windows xp.

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

Comment By: Pascal Rapicault (pascal)
Date: 2007-11-14 16:44

Message:
Logged In: YES 
user_id=13911

After a successful build, my attempt at running the solver
on the attached bug.opb file failed.
When I run:
  java -jar sat4j-core.jar d:/tmp/bug.opb
I get:
java.io.IOException: DIMACS non valide (nombre de Literaux
non valide)
        at
org.sat4j.reader.LecteurDimacs.parseInstance(Unknown Source)
        at org.sat4j.reader.Reader.parseInstance(Unknown Source)
        at
org.sat4j.reader.InstanceReader.parseInstance(Unknown Source)

When I run with:
 java -jar sat4j-core.jar org.sat4j.LanceurPseudo2007
d:/tmp/bug.opb

I get:
Exception in thread "main"
java.lang.ArrayIndexOutOfBoundsException: 1
        at org.sat4j.Lanceur.configureSolver(Unknown Source)
        at org.sat4j.AbstractLauncher.run(Unknown Source)
        at org.sat4j.Lanceur.main(Unknown Source)

I will try to investigate and report on my findings here if any.

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

Comment By: Pascal Rapicault (pascal)
Date: 2007-11-14 16:29

Message:
Logged In: YES 
user_id=13911

In fact I was just struggling with that! Thx!

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

Comment By: Daniel Le Berre (leberre)
Date: 2007-11-14 15:59

Message:
connecté 
user_id=4369

Pascale,

I found a problem in the PB07 Reader.

The min: instruction could be ignored in some cases.

I committed a fix to CVS.

Please find attached to this bug report an ant build file
that build sat4j from OW2 anonymous CVS.

just type:

ant -f build-2.0.xml pseudo

to build a ready-to-run PB solver based on SAT4J CVS:

java -jar sat4j-pb.jar /tmp/bug.opb

Please be sure that the solver is outputting an "OPTIMIZING"
message.

If not, it means that the solver has some trouble to read
your file.

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

Comment By: Daniel Le Berre (leberre)
Date: 2007-11-14 12:26

Message:
connecté 
user_id=4369

Pascal,

BTW, for pb optimization, you need to use the following
launcher:

java -cp sat4j-1.7.jar org.sat4j.LanceurPseudo2007 pbfile

More details at:
http://www.sat4j.org/howto.php

--Daniel

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

Comment By: Daniel Le Berre (leberre)
Date: 2007-11-14 12:10

Message:
connecté 
user_id=4369

Pascal,

Here is an updated opb file that works fine.

Here is the output of the solver:

c #vars     4
c #constraints  6
c SATISFIABLE
c OPTIMIZING...
c Got one! Elapsed wall clock time (in seconds):0.03
o 14
c starts                : 1
c conflicts             : 0
c decisions             : 1
c propagations          : 7
c inspects              : 15
c learnt literals       : 0
c learnt binary clauses : 0
c learnt ternary clauses        : 0
c learnt clauses        : 0
c root simplifications  : 0
c removed literals (reason simplification)      : 0
c reason swapping (by a shorter reason) : 0
c Calls to reduceDB     : 0
c speed (decisions/second)      : 1000.0
c non guided choices    0
s OPTIMUM FOUND
v x1 -x2 x3 x4 
c objective function=14




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

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