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

Closed
Open
Created Sep 07, 2011 by Daniel Le Berre@leberreOwner

Make sure that all solvers return a unit clause in addClause

In many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.

However, especially in the simple SAT case, that behavior is not enforced for all DataStructureFactory.

We thus need to make sure that all DSF do return a UnitClause object instead of null when a unit clause is detected.

Assignee
Assign to
2.3.1
Milestone
2.3.1 (Past due)
Assign milestone
Time tracking
None
Due date
None