Backend Request Inconsistencies

I'm trying to figure out why the constraints in this example render the formula UNSAT. Without the NoMoreThanKInARow constraint, the formula is SAT. Additionally, it's only UNSAT when using 3 levels for text and color. The example using only two colors is SAT with the constraint. (But unigen doesn't like it because there are too few solutions.)

I decided to make sure my assumptions about how the low-level requests are interpreted were correct before going any further. In doing so, I discovered that the behavior seems to be inconsistent. To facilitate this, I used a small helper script to take a JSON request to the backend, and output a satisfying assignment for the corresponding CNF formula:

#!/usr/bin/env bash

curl -Ss -d @"$1" localhost:8080/experiments/build-cnf > "$1.cnf"
minisat "$1.cnf" "$1.sol" > /dev/null
cat "$1.sol"
rm "$1.cnf" "$1.sol"

To start with, I did a few tests with EQ requests, as I believe those are working correctly.

`EQ` Tests

eq-0.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3]],
  "requests": [
    {"equalityType": "EQ", "k": 0, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh eq-0.json
UNSAT

eq-1.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3]],
  "requests": [
    {"equalityType": "EQ", "k": 1, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh eq-1.json
SAT
-1 2 -3 ...

eq-2.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3]],
  "requests": [
    {"equalityType": "EQ", "k": 2, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh eq-2.json
SAT
-1 2 3 ...

eq-3.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3]],
  "requests": [
    {"equalityType": "EQ", "k": 3, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh eq-3.json
SAT
1 2 3 ...

All those look good. The EQ request correctly constrains the right number of variables to be true.

`LT` Tests

lt-0.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3]],
  "requests": [
    {"equalityType": "LT", "k": 0, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-0.json 
UNSAT

As expected, this one is clearly unsatisfiable.

The next question I had was whether or not LT means <, or <=. So to answer that, I did this test:

lt-1.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3], [1]],
  "requests": [
    {"equalityType": "LT", "k": 1, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-1.json
SAT
1 -2 -3 ...

Interesting, apparently it means <=? (Whether intentionally or not, I can't say.)

So if that's the case, then I should also be able to force 1 2 -3 as a solution like this:

lt-2.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3], [1], [2]],
  "requests": [
    {"equalityType": "LT", "k": 2, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-2.json
UNSAT

Yet for some reason, that is unsatisfiable. How about if I only require one variable to be true?

lt-2-1.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3], [1]],
  "requests": [
    {"equalityType": "LT", "k": 2, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-2-1.json
SAT
1 -2 -3 ...

Works. Interesting. So is it that LT means <= when k = 1, but < when k > 1? Does that hold true when k = 3?

lt-3.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3], [1], [2], [3]],
  "requests": [
    {"equalityType": "LT", "k": 3, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-3.json
SAT
1 2 3 ...

Apparently not, since LT meant <= here.

Can I force a solution with only two true variables then?

lt-3-2.json:

{
  "fresh": 3,
  "cnfs": [[1, 2, 3], [1], [2], [-3]],
  "requests": [
    {"equalityType": "LT", "k": 3, "booleanValues": [1, 2, 3]}
  ],
  "unigen": {"support": 3}
}

➜ ./run-test.sh lt-3-2.json 
UNSAT

Apparently not. It's like it wants to treat the LT like EQ in this case.

I'm not sure how this relates to the example yet, since that one only uses LT with k = 1, but it's unsettling all the same.

anniecherk / sweetpea-core