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 53
    • Issues 53
    • 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
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • SAT4J
  • sat4jsat4j
  • Issues
  • #124

Closed
Open
Opened Jan 03, 2015 by Daniel Le Berre@leberreOwner

Lexico-Optimization does not work with ManyCore (parallel) solvers.

During the LION 9 challenge, two versions of Sat4j was used.

That challenge is about solving multi-objective boolean functions, in that case lexicographic one.

The pure resolution based one worked fine while the one using the parallel solver Both answered sub-optimal solutions.

The parallel solver has been used successfully for years on PB benchmarks.

The main issue with lexicographic optimization is that an UNSAT answer is not final contrariwise to the mono-objective optimization.

Initial investigation of the problem shows that the parallel solvers always answer UNSAT after a while.

Assignee
Assign to
2.3.6
Milestone
2.3.6 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: sat4j/sat4j#124