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

Closed
Open
Created Jan 15, 2019 by Miguel Neves@miguelterraneves

Bug when mixing constraint removal and constraints satisfied by unit propagation

Hi Daniel,

I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation. In particular, the bug is triggered by the following sequence of operations:

  • add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
  • check satisfiability: formula is SAT, as expected
  • remove (x1 + x2 >= 2)
  • add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
  • check satisfiability: formula should be UNSAT, but SAT is returned instead

I have attached a small Java program that follows this sequence of operations, triggering the bug.

Best regards,

Miguel Neves

SatByUnitBug.java

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