Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Counter-example or Solution Cache #1205

Open
feliam opened this issue Oct 21, 2018 · 0 comments
Open

Implement Counter-example or Solution Cache #1205

feliam opened this issue Oct 21, 2018 · 0 comments

Comments

@feliam
Copy link
Contributor

feliam commented Oct 21, 2018

The counter-example cache maps sets of constraints to a variable assignments that solves it, or flag it as no sat. By storing the cache in this fashion, the solutions cache gains three additional ways to eliminate queries.

1- When a subset of a constraint set has no solution, then neither does the original constraint set. Adding constraints to an unsatisfiable constraint set cannot make it satisfiable.

2- When a superset of a constraint set has a solution, that solution also satisfies the original constraint set. Dropping constraints from a constraint set does not invalidate a solution to that set.

3- When a subset of a constraint set has a solution, it is likely that this is also a solution for the original set. Checking a potential solution is cheap.

Research, implement and add tests for it.
Defining a new CounterExampleConstraintSet class may be the way to go.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants