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
  • #22

Closed
Open
Created May 09, 2011 by Daniel Le Berre@leberreOwner

DependencyHelper (the solvers in general) behave differently when units are set first or set last

The DependencyHelper behavior can look strange to newcomer since its behavior depends of the order of the constraints.

SAT power users use that order to let the solver perform as much simplification as possible.

Here, we receive an exception when the constraints are simplified.

Several options are available:

  • do not fix, its a feature, not a bug
  • fix be ignoring simplified constraints => no more control of what's going on in the helper, might be error prone
  • fix by delegating unit to be the last thing added to the solver: the helper acts as a proxy here. => no more power user control of the helper.

Need to think about it.

Assignee
Assign to
Time tracking