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.

Sign up for GitHub

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

Jump to bottom

Add partial evaluator and improved boolean support #363

Merged
merged 9 commits into from
Oct 15, 2024
Merged

Add partial evaluator and improved boolean support #363

merged 9 commits into from
Oct 15, 2024

Conversation

niklasdewally
Copy link
Contributor

@niklasdewally niklasdewally commented Oct 11, 2024 •
edited
Loading

This PR adds a partial evaluator, and several changes discovered in the testing thereof.

Details can be found in individual commit messages.

Changelog

  • fix: empty or([]) being parsed as nothing
  • fix: add test case for soph's non-terminating min problem
  • change rule priorities to run simplifiers first; add reify
  • add broken complex partial evaluator test (arithmetic, nesting, min)
  • implement not(x) ~> w-lit(x,0)
  • add test for partial evaluation of or, and
  • add w-lit constraint, enabling support for variables in and/or clauses
  • parser: add alldiff
  • parser: add boolean constants
  • add partial evaluator

@niklasdewally niklasdewally force-pushed the feat/add-partial-evaluator branch 3 times, most recently from c6ac9c4 to 3993b8a Compare October 11, 2024 18:29
@ozgurakgun
Copy link
Contributor

looking good so far!

@niklasdewally niklasdewally force-pushed the feat/add-partial-evaluator branch 16 times, most recently from b4e9089 to fc3a730 Compare October 12, 2024 10:59
@niklasdewally niklasdewally changed the title Add partial evaluator and watched literal constraint Add partial evaluator and improved boolean support Oct 12, 2024
@niklasdewally niklasdewally force-pushed the feat/add-partial-evaluator branch 2 times, most recently from 3a8b452 to b25c3bb Compare October 12, 2024 12:27
ChrisJefferson
ChrisJefferson reviewed Oct 14, 2024
View reviewed changes
COMMITMSG Outdated Show resolved Hide resolved
@niklasdewally
Copy link
Contributor Author

@ozgurakgun apart from the outstanding comments, and that failing test, is there anything else I need to do before this is ready to merge?

@ozgurakgun
Copy link
Contributor

looks good to me!

@niklasdewally niklasdewally marked this pull request as ready for review October 14, 2024 15:38
@niklasdewally niklasdewally self-assigned this Oct 14, 2024
@ozgurakgun
Copy link
Contributor

trivial looking conflicts now that other PRs are merged

@niklasdewally niklasdewally marked this pull request as draft October 15, 2024 07:10
@niklasdewally
Copy link
Contributor Author

niklasdewally commented Oct 15, 2024 •
edited
Loading

Before merge:

  • needs test for the second model in An empty 'or' should be false #366, min([]) = 2
  • add Minion native true/false constraints to replace my use of 1=1 and 1=2
  • rebase in new max constraint changes, and add max to the partial evaluator

@ChrisJefferson
Copy link
Contributor

This looks OK to me.

However, it's also grown far too large to review, and has quite a lot of different things going on!

In future, I'd try to break this kind of thing up into smaller bits -- sometimes I find that means doing things like the renumbering as a PR, getting it merged, then rebasing my other work on top of it, just to keep things reasonably reviewable and mergable :) I realise this can slow one down when deep into coding, but helps with reviewing, as some PRs end up big, but fairly mechanical, while others are smaller but need more careful review.

@niklasdewally
Copy link
Contributor Author

niklasdewally commented Oct 15, 2024 •
edited
Loading

In future, I'd try to break this kind of thing up into smaller bits -- sometimes I find that means doing things like the renumbering as a PR, getting it merged, then rebasing my other work on top of it, just to keep things reasonably reviewable and mergable :) I realise this can slow one down when deep into coding, but helps with reviewing, as some PRs end up big, but fairly mechanical, while others are smaller but need more careful review.

Apologies for this! I usually try to stack PRs, so I don't know why I didn't here...

niklasdewally and others added 9 commits October 15, 2024 12:31
@niklasdewally
add partial evaluator
3394b92 
For expressions containing both constants and nested expressions, the partial
evaluator collapses constant values into a single value. For example, x + 1 + y
+ 2 + 3 ~> x + y + 6.

In some cases, the partial evaluator replaces the constraint with a truth
value. Currently, this is done when two identical constants are in an
all-different constraint, and for the boolean clauses ` M or true` and `M and
false`.

The difference between this and the existing evaluator is that the latter only
evaluates expressions made entirely of constants. Having both is useful: the
total evaluator is useful for solutions checking (amongst other things), and
the partial evaluator for model Optimisation.
@niklasdewally
parser: add boolean constants
4c2e1d7
@niklasdewally
add w-lit constraint, enabling support for variables in and/or clauses
40ce5a9 
 - Add w-lit constraint, allowing variables to be found at the top level of and
   and or clauses.

  `And` and `or` convert to the watched-and and watched-or Minion constraints.
  These only take constraints as arguments, not variables. W-lit(x,1) is
  SAT iff x is true; using this fact, variables can be converted to
  constraints, solving this limitation.

  Conjure Oxide's W-lit expression is more strongly typed than other
  expressions. My intention is for this to be a low-level, Minion-specific
  expression that is only used at the end of the rewriting process. As far as I
  can see, it doesn't have any modelling uses, and is only useful to allow the
  use of variables in watched-or / watched-and.
@niklasdewally
add test for partial evaluation of or, and
9773972
@niklasdewally
implement not(x) ~> w-lit(x,0)
1460788
@niklasdewally
add broken complex partial evaluator test (arithmetic, nesting, min)
0333550 
Add more complex test case for the partial evaluator. This currently
never terminates, so has been disabled.
@niklasdewally
change rule priorities to run simplifiers first; add reify
6c6d511 
Create a rule priority taxonomy, and refactor rules to follow this new
convention. In particular, ensure that partial and total evaluation and
simplification rules happen before representation changes and solver
specific rules.

DESCRIPTION

Simplifying a model before applying representation changes should ensure
that nested sums do not get propagated across the model. For example,
the transformation for min turns it into many binary constraints. If
simplification was not done first, simplification steps would have to be
ran on each of these binary constraints, instead of just on the input
model.

Ensuring that everything is always in canonical forms should stop rules
looping, and help with pattern matching. The implementation of
canonical forms is incomplete and outside the scope of this patch.

These rule changes caused basic-div-04 to fail. To fix this, this patch
also does the following:

- add reify constraint (reify(X,1) if constraint X is SAT, reify(X,0) if
  constraint X is UNSAT)

- add rule not(X) ~> reify(X,0) (where X is a constraint), allowing
  negated constraints to be passed to Minion.

MOTIVATION

The commit c2b7460 (add broken complex partial evaluator test
(arithmetic, nesting, min), 2024-10-12) added a test case for the
partial evaluator that never terminated.

Simplification steps should be ran before the decomposition of the min
constraint and the conversion of expressions into more specialised /
solver specific forms (such as ineq, sumgeq, etc); however, this was not
the case in this test. In this test, ineq / sumgeq were being applied
before the sums had been flattened.

After this refactor, this test now terminates with failure. A flattening
rule for ineq is needed before this test passes and will be added
in a later commit.
@niklasdewally @Soph1514
fix: add test case for soph's non-terminating min problem
9f326e4 
Soph (sm600) reported that the added model never terminated. Recent
changes to the rule system (likely b25c3bb (change rule priorities to
run simplifiers first; add reify, 2024-10-12)) has fixed this.

Co-authored-by: Soph <[email protected]>
@niklasdewally
fix: empty or([]) being parsed as nothing
a9b71f1 
Constant matrices inside operations were not recognised by our parser,
so were ignored. This includes expressions like or([]) and
min([1,2,3]).

- Add parsing support for constant matrices inside operations.

- Add support for top level "false" and "true" with Minion. Ideally,
  these models would never get passed to the solver; however, this would
  require solution evaluation and a refactor of our tester, so I have
  left this for future work.

Fixes conjure-cp#366.
@niklasdewally niklasdewally marked this pull request as ready for review October 15, 2024 11:38
@niklasdewally
Copy link
Contributor Author

@ozgurakgun ready for review!

@ozgurakgun ozgurakgun merged commit dc7f98b into conjure-cp:main Oct 15, 2024
8 checks passed
@niklasdewally niklasdewally deleted the feat/add-partial-evaluator branch October 15, 2024 18:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ozgurakgun ozgurakgun ozgurakgun approved these changes

@ChrisJefferson ChrisJefferson Awaiting requested review from ChrisJefferson

Assignees

@niklasdewally niklasdewally

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@niklasdewally @ozgurakgun @ChrisJefferson