Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • sat4j sat4j
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 57
    • Issues 57
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SAT4J
  • sat4jsat4j
  • Issues
  • #126

Closed
Open
Created Feb 24, 2015 by Ghost User@ghost

How do I do an industry standard export for Partial Weighted MaxSat problems?

I have filed this as question, but it might result in a change request:

I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constraints. If I do not want to convert them to CNF constraints, I cannot export a wcnf file but must export something other. I think the .opb format is suitable for that case. Am I right? I tried to create .opb output using the OPBStringSolver or the LPStringSolver. Both have the same problem: The WeightedMaxSatDecorator calls the method "registerLiteral(int p)" on the decorated solver. Since both the OPBStringSolver and the LPStringSolver extend the DimacsStringSolver, the method DimacsStringSolver.registerLiteral(int p) is called, which throws an UnsupportedOperationException.

So, if one of these StringSolvers is suitable for my problem: Would it be a solution to override the method in that suitable solver so that it does not do anything?

An, if none of these StringSolvers is suitable: Is there another way of exporting all input that the WeightedMaxSatDecorator got into a standard file format?

Assignee
Assign to
Time tracking