Skip to content
This repository has been archived by the owner on Dec 2, 2021. It is now read-only.

"unsatisfiable constraint" error puts solver into an inconsistent state #31

Open
earthlyreason opened this issue Nov 26, 2020 · 3 comments

Comments

@earthlyreason
Copy link

Hi, thanks for this project. It is small and easy to work with.

I have found what appears to be a bug in the handling of certain state changes.

As far as I can tell, the only way to know whether a new constraint will lead to a feasible solution is to try adding it and trap the "unsatisfiable constraint" error.

In such cases, the new constraint is not added to the solver.

However, the solver no longer behaves as expected at that point. Specifically, if a previously-existing constraint is then removed and re-added to the solver, it is then reported as unsatisfiable, even though it had already been confirmed.

The following script reproduces the issue:

const { Le, Ge } = kiwi.Operator;
const { required, strong } = kiwi.Strength;

const solver = new kiwi.Solver();

console.log(`Add variable x`);
const x = new kiwi.Variable("x");
solver.addEditVariable(x, strong);

console.log(`Add constraint x >= 2 [required]`);
const xge2 = new kiwi.Constraint(x, Ge, 2);
solver.addConstraint(xge2, required);

// Show that you can remove and restore existing constraints with no problem
console.log(`Remove constraint x >= 2 [required]`);
solver.removeConstraint(xge2);
console.log(`Restore constraint x >= 2 [required]`);
solver.addConstraint(xge2);

// Now let's add an unsatisfiable constraint
console.log(`Add constraint x <= 1 [required]`);
const xle1 = new kiwi.Constraint(x, Le, 1);
try {
  solver.addConstraint(xle1, required);
} catch (error) {
  if (error.message === "unsatisfiable constraint") {
    console.log(`Constraint was unsatisfiable, as expected`);
  } else throw error;
}

// Some sanity checks, which pass
console.log(
  `Does solver have constraint x >= 2?`,
  solver.hasConstraint(xge2) ? "yes" : "no"
);
console.log(
  `Does solver have constraint x <= 1?`,
  solver.hasConstraint(xle1) ? "yes" : "no"
);
console.log(
  `Does solver have variable x?`,
  solver.hasEditVariable(x) ? "yes" : "no"
);

console.log(`Remove constraint x >= 2 [required]`);
solver.removeConstraint(xge2);
// Solver should have no constraints at this point
console.log(`Restore constraint x >= 2 [required]`);
try {
  solver.addConstraint(xge2);
} catch (error) {
  if (error.message === "unsatisfiable constraint") {
    // This is unexpected, because the constraint was just in the solver...
    // and is now the only constraint, in any case, so must be satisfiable
    console.log(`Constraint was unsatisfiable!!`);
  } else throw error;
}

I have tried other things at this point. For example, you can add effectively the same constraint using a new variable:

console.log(`Create new ‘x’ variable instance`);
// Name can be "x" or anything else
const x_b = new kiwi.Variable("x");

// Doesn't seem to matter whether you do this
// solver.addEditVariable(x_b, strong);
console.log(`Create new constraint x >= 2`);
const xge2_b = new kiwi.Constraint(x_b, Ge, 2);

console.log(
  `Does solver have variable new x?`,
  solver.hasEditVariable(x_b) ? "yes" : "no"
);

solver.addConstraint(xge2_b, required);

All in all, the signs point to a possible issue with the internal management of variables in the Solver.addConstraint method, particularly:

        // Creating a row causes symbols to be reserved for the variables
        // in the constraint. If this method exits with an exception,
        // then its possible those variables will linger in the var map.
        // Since its likely that those variables will be used in other
        // constraints and since exceptional conditions are uncommon,
        // i'm not too worried about aggressive cleanup of the var map.
        let data = this._createRow( constraint );
        let row = data.row;
        let tag = data.tag;
        let subject = this._chooseSubject( row, tag );

I hate to file a bug on a holiday, but I thought it might be useful to have for reference. I will dig into this further myself and report back.

@IjzerenHein
Copy link
Owner

That's great investigative work Gavin, thank you for filling this! I don't have any bandwidth to address this problem any time soon, but if you provide a PR I will try to verify and merge it quickly.
Cheers!

@earthlyreason
Copy link
Author

Sure thing. I should say, that since I did not understand the Simplex algorithm very well to begin with, I ended up reading the literature and writing my own basic implementation in order to learn it. I am currently working through the Cassowary papers and am quite impressed how you got so much into such a compact program. However, I'm not 100% sure I'm going to come out of this yak shave.

@IjzerenHein
Copy link
Owner

Well, frankly you probably already know more than me in this area 😅
This project was originally written by Chris Colbert and based on the algorithms of the kiwi C++ constraint solver (https://github.com/nucleic/kiwi). I found it useful and used it in https://github.com/IjzerenHein/autolayout.js and after a couple years of laying dormant decide to publish it, as I felt it could be useful to other folks as well. That being said, I don't really actively use kiwi.js in any of my work right now. Feel free to post a PR though, I'll review it 👍

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

No branches or pull requests

2 participants