Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
sat4j
sat4j
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 56
    • Issues 56
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 1
    • Merge Requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SAT4J
  • sat4jsat4j
  • Issues
  • #136

Closed
Open
Created Jan 17, 2016 by Anitha@anithag

Incorrect answer with PB Solver

I am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101

Attached are 2 opb files: min-nonbuggy.opb and min.opb

Differences between the files: Both files differ from line 18 onwards. "min.opb" is an extension of min-nonbuggy.opb. Note that both files have same objective function that needs to be minimized.

The first file ("min-nonbuggy.opb") returns correct answer with optimum value as "4" with x12=0, x14 = 0 and x17=0. I agree with this answer. I also verified this by manually solving the constraints and objective function.

The second file ("min.opb") returns answer with optimum value as "5" with x12=1, x14=0 and x17=0. I think this is wrong.

(I am interested in values that appear in objective function only)

This is quite surprising given that - no additional constraint involving "x12" appears in "min.opb". So x12 should be 0 regardless of value of x17. Isn't it? Why is the answer returned as x12=1?

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None