krr / IDP / issues / #799 - Simplifier breaks propagation — Bitbucket

Issue #799 invalid

Bart Bogaerts created an issue 2014-08-27

This is an issue in MinisatID.

However, one IDP test is disabled because of this issue.

Please close this issue and put the test back as soon as the corresponding issue

https://bitbucket.org/krr/minisatid/issue/56/simplifier-breaks-propagation

is fixed.

Comments (3)

Bart Bogaerts reporter
Removed unsatsolvertest

see ~~#799~~

→ <<cset 60df43bbe3cc>>
- 2014-08-27T14:40:09+00:00
Bart Bogaerts reporter
Extra uitleg.

De simplifier werkt momenteel als volgt: cache alle input voor de solver. Zodra hij signaal krijgt dat de grounding klaar is, vereenvoudig theorie en geef hem door naar propagatoren etcetera.

Dit is niet compatibel met het idee om unsat al snel naar de grounder toe te propageren zodat hij snel kan stoppen
- 2014-08-27T15:09:45+00:00
Bart Bogaerts reporter
- changed status to invalid
This is the expected behaviour of the simplifier
- 2014-11-19T18:18:51+00:00
Log in to comment

Assignee: –

Type: bug

Priority: major

Status: invalid

Component: –

Version: –

Votes: 0

Watchers: 1

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