krr / IDP / issues / #487 - !x: q(x) & ~q(x) does not derive unsat early with lifted unit propagation — Bitbucket

Issue #487 new

Broes De Cat created an issue 2013-07-27

No description provided.

Comments (2)

Bart Bogaerts
LUP does not derive unsat?

Or LUP does not derive unsat for infinite domain?

If I'm not mistaken, applying propagation to structure will not finish as soon as the structure is inconsistent, which might be a possible optimisation...
- 2013-07-27T12:24:03+00:00
Broes De Cat reporter
It does not stop soon enough (after the first inconsistent element is added). But in this case, couldn't we even stop before generating any elements?
- 2013-07-27T12:56:34+00:00
Log in to comment

Assignee: –

Type: bug

Priority: major

Status: new

Component: –

Version: –

Votes: 0

Watchers: 1

Jira: the preferred issue tracker for Bitbucket. Join the team!