[sat4j-dev] [ sat4j-Bugs-308276 ] objective function displayed is incorrect when wcnf contains weighted unit literals

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Bugs item #308276, was opened at 17/01/2008 23:06
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=308276&group_id=228

Category: maxsat
Group: ongoing version (cvs)
Status: Open
Resolution: None
Priority: 9
Submitted By: Daniel Le Berre (leberre)
Assigned to: Daniel Le Berre (leberre)
Summary: objective function displayed is incorrect when wcnf contains 
weighted unit literals

Initial Comment:
When a formula contains weighted unit literals, the negation of those 
literals,
with the same weight, are added to the objective function.

The idea is to replace a weighted max sat problem by a binate covering 
problem.

I guess that the issue can be fixed by allowing max and min optimization
problems instead of just minimization problems are for now.

It will be fixed BEFORE 2.0 final ships.

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

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