mbuit82 commented 6 months ago

Good news is that, before editing anything, I'm not getting the error for N > 4, at least for cf_excl_mid.py. (for poss_strenght.py I got it at N=6, but not N=5). More good news is that cf_excl_mid.py seems to work for indefinitely high values of N (up to 17—after that it started taking long and I was lazy). Bad news is that I'm getting an odd pattern. Here's all the states for N=15:

States:

b000000000000000 = □ (possible)

b000000000000001 = a (world)

b000000000000010 = b (impossible)

b000000000000011 = a.b (impossible)

b000000000000100 = c (world)

b000000000000101 = a.c (impossible)

b000000000000110 = b.c (impossible)

b000000000000111 = a.b.c (impossible)

b000000000001000 = d (impossible)

b000000000001001 = a.d (impossible)

b000000000001010 = b.d (impossible)

b000000000001011 = a.b.d (impossible)

b000000000001100 = c.d (impossible)

b000000000001101 = a.c.d (impossible)

b000000000001110 = b.c.d (impossible)

b000000000001111 = a.b.c.d (impossible)

b000000000010000 = e (world)

b000000000010001 = a.e (impossible)

b000000000010010 = b.e (impossible)

b000000000010011 = a.b.e (impossible)

b000000000010100 = c.e (impossible)

b000000000010101 = a.c.e (impossible)

b000000000010110 = b.c.e (impossible)

b000000000010111 = a.b.c.e (impossible)

b000000000011000 = d.e (impossible)

b000000000011001 = a.d.e (impossible)

b000000000011010 = b.d.e (impossible)

b000000000011011 = a.b.d.e (impossible)

b000000000011100 = c.d.e (impossible)

b000000000011101 = a.c.d.e (impossible)

b000000000011110 = b.c.d.e (impossible)

b000000000011111 = a.b.c.d.e (impossible)

It looks like it always (this held for all other N values) just calls atomic states worlds, the null state possible, and every other state impossible. I'm not sure if this is trivial, but I thought I'd let you know. The same seems to be true for poss_strength.py.

It also looks like it's not printing the entire state space (see all the trailing 0s). This pattern isn't regular—for example, it printed more states for N=9 (and N=17) than it did for N=15. This might be because it found model before needing to set the farther out states to a number (so in a sense those farther states were never in the model—at least I think this, because the print_states function finds the max bitvec value in the model).

Speaking of N=17, it took a while for N=17 (for cf_excl_mid.py), but it worked. Very similar result, but it didn't seem to find as trivial a model this time, only in the sense that it had less trailing zeroes—the possible/world/impossible picture looked the same. This was the last state printed:

b00111111111111111 = a.b.c.d.e.f.g.h.i.j.k.l.m.n.o (impossible)

Which means it printed \sum_{i=0}^{14}{2^i} states, which comes out to 32,767 states. It took a while (maybe a minute? three minutes? And it actually took longer than a second to print (probably about 2), it was kind of cool seeing the difference between the sheer size of this model and the ones it finds with smaller N values).

But the issue stands—it the world/possible/impossible distribution is always the same, even across different countermodels (for cf_excl_mid.py and poss_strength.py)

mbuit82 commented 6 months ago

Update: I think I fixed the as_long() issue. You were right; it was an issue with the definition is_bitvector. And on the weird world/possible/impossible pattern noted above, poss_strength.py with N=6 (a case that previously didn't work, idk if that's relevant) gave the following output. Note state c (#b000100) is possible, not a world, breaking the pattern:

There is a model of: A => C ~(A => ~B) ~(A & B => C)

States:

b000000 = □ (possible)

b000001 = a (world)

b000010 = b (world)

b000011 = a.b (impossible)

b000100 = c (possible)

b000101 = a.c (impossible)

b000110 = b.c (impossible)

b000111 = a.b.c (impossible)

b001000 = d (impossible)

b001001 = a.d (impossible)

b001010 = b.d (impossible)

b001011 = a.b.d (impossible)

b001100 = c.d (impossible)

b001101 = a.c.d (impossible)

b001110 = b.c.d (impossible)

b001111 = a.b.c.d (impossible)

b010000 = e (impossible)

b010001 = a.e (impossible)

b010010 = b.e (impossible)

b010011 = a.b.e (impossible)

b010100 = c.e (impossible)

b010101 = a.c.e (impossible)

b010110 = b.c.e (impossible)

b010111 = a.b.c.e (impossible)

b011000 = d.e (impossible)

b011001 = a.d.e (impossible)

b011010 = b.d.e (impossible)

b011011 = a.b.d.e (impossible)

b011100 = c.d.e (impossible)

b011101 = a.c.d.e (impossible)

b011110 = b.c.d.e (impossible)

b011111 = a.b.c.d.e (impossible)

b100000 = f (world)

b100001 = a.f (impossible)

b100010 = b.f (impossible)

b100011 = a.b.f (impossible)

b100100 = c.f (impossible)

b100101 = a.c.f (impossible)

b100110 = b.c.f (impossible)

b100111 = a.b.c.f (impossible)

b101000 = d.f (impossible)

b101001 = a.d.f (impossible)

b101010 = b.d.f (impossible)

b101011 = a.b.d.f (impossible)

b101100 = c.d.f (impossible)

b101101 = a.c.d.f (impossible)

b101110 = b.c.d.f (impossible)

b101111 = a.b.c.d.f (impossible)

b110000 = e.f (impossible)

b110001 = a.e.f (impossible)

b110010 = b.e.f (impossible)

b110011 = a.b.e.f (impossible)

b110100 = c.e.f (impossible)

b110101 = a.c.e.f (impossible)

b110110 = b.c.e.f (impossible)

b110111 = a.b.c.e.f (impossible)

b111000 = d.e.f (impossible)

b111001 = a.d.e.f (impossible)

b111010 = b.d.e.f (impossible)

b111011 = a.b.d.e.f (impossible)

b111100 = c.d.e.f (impossible)

b111101 = a.c.d.e.f (impossible)

b111110 = b.c.d.e.f (impossible)

b111111 = a.b.c.d.e.f (impossible)

The evaluation world is b: A, B, C (not true in b)

Propositions: |A| = < ∅, ∅ > There are no A-alternatives to b

|B| = < ∅, ∅ > There are no B-alternatives to b

|C| = < ∅, ∅ > There are no C-alternatives to b

benbrastmckie commented 6 months ago

N>4 seems to work, but N=4m for any nonzero value of m doesn't. So that must be a separate issue (I'll open one).

I fixed the error which was making the extensions of sentence letters empty and created the file mereology.py two build complex worlds. I also defined non_null_verify and non_null_falsify since these will often be useful in building realistic models. I was tempted to always use them, and we may want to do this in the constraint generator functions, but figured I'd leave both definitions for now.

As for the printouts, it seems to be going in the wrong order somehow even when it gets all of the states. Here is an example:

States:
  #b000 = □ (possible)
  #b001 = a (world)
  #b010 = b (possible)
  #b011 = a.b (impossible)
  #b100 = c (world)
  #b101 = a.c (impossible)
  #b110 = b.c (world)
  #b111 = a.b.c (impossible)
  #b000 = □ (possible)
  #b001 = a (world)
  #b010 = b (possible)
  #b011 = a.b (impossible)

The evaluation world is b.c:
  A, B  (true in b.c)

Propositions:
  |A| = < {a, b}, ∅ >
  There are no A-alternatives to b.c

  |B| = < {a, b.c, c}, ∅ >
  There are no B-alternatives to b.c

Certain states occur multiple times, and 111 (a.b.c) is not last. I also noticed for N=5 and other bigger values that it will typically include later states even when this is unnecessary. For instance:

States:
  #b00000 = □ (possible)
  #b00001 = a (impossible)
  #b00010 = b (world)
  #b00011 = a.b (impossible)
  #b00100 = c (possible)
  #b00101 = a.c (impossible)
  #b00110 = b.c (impossible)
  #b00111 = a.b.c (impossible)
  #b01000 = d (world)
  #b01001 = a.d (impossible)
  #b01010 = b.d (impossible)
  #b01011 = a.b.d (impossible)
  #b01100 = c.d (world)
  #b01101 = a.c.d (impossible)
  #b01110 = b.c.d (impossible)
  #b01111 = a.b.c.d (impossible)
  #b10000 = e (impossible)
  #b10001 = a.e (impossible)
  #b10010 = b.e (impossible)
  #b10011 = a.b.e (impossible)
  #b10100 = c.e (impossible)
  #b10101 = a.c.e (impossible)
  #b10110 = b.c.e (impossible)
  #b10111 = a.b.c.e (impossible)

The evaluation world is c.d:
  A, B  (true in c.d)

Propositions:
  |A| = < {b, c}, ∅ >
  There are no A-alternatives to c.d

  |B| = < {b, c.d, d}, ∅ >
  There are no B-alternatives to c.d

I'm not sure there is any way to control which models and states Z3 finds and it might be hard to label the states that Z3 finds in any other way, but what we can control is how big N is. The only trouble is that if N is too small, then it gives strange results instead of saying that there is no model. Here is what I got for N=2:

States:
  #b00 = □ (possible)
  #b01 = a (possible)
  #b10 = b (world)
  #b11 = a.b (world)
  #b00 = □ (possible)
  #b01 = a (possible)

The evaluation world is a.b:
  A, B  (true in a.b)

Propositions:
  |A| = < {a, a.b}, ∅ >
  There are no A-alternatives to a.b

  |B| = < {b}, ∅ >
  There are no B-alternatives to a.b

Notice that both b and a.b are worlds. But that doesn't make any sense. It seems to avoid this when it is able to, but in the case of mereology.py, there shouldn't be a model. Not sure how we might avoid this.