search

jgraley / inferno-cpp2v

2 stars 0 forks source link

General push to symbolic #430

Closed jgraley closed 2 years ago

jgraley commented 2 years ago

CSP Solver should begin taking hints from these expressions

jgraley commented 2 years ago

There is a problem. While distributive clutch creates a conjunctive form, allowing for constraint splitting (which will happen after the above is done), the clauses are | operators. A typical 2-op might be 

ItemSingular<4>([keyer_plink]) == [plink 4 from plan] & 
[#43->Stuff<Node>#X97-4] != #0->MMAX#-0 &
[#64->Delta<Node>#X97-1] != #0->MMAX#-0 &
KindOf<Node>([#43->Stuff<Node>#X97-4]) 
|
[#43->Stuff<Node>#X97-4] == #0->MMAX#-0 &
[#64->Delta<Node>#X97-1] == #0->MMAX#-0`

The Colocated node could use the trick of a==MM and b==MM => a==b etc - other agents will have difficulty, due in this case to the ItemSingular<4>( ). So we're going to spot the pattern in the solver. Look for clauses in the OR operand expressions that force an exclusive OR.

Terminology

the bi are expressions that may or may not depend on variable x. x: bi means solve for x such that bi is satisfied and should only be written when it's known that bi depends on x. There will usually be other restrictions on solvability.

Controlling clause

b1 != b2 == !(b1 == b2) (!b1 & b2) | (b1 & b3) => b1 ? b3 : b2 If b1 is known and b2 and b3 can each be solved for x then x = (x: b1 ? b3 : b2) is x = b1 ? x: b3 : x: b2 so solve both b2 and b3 and hang them on a ternary controlled by eval(b1)

The determination of which sub-clause is b1 as opposed to b2 or b3 seems to be opportunistic. b1 should not depend on the solve-for x; b2 and b3 should.

Note: a correct outcome allows for MMAX, i.e. should be like x = (xk==MMAX) ? MMAX : f(xk)

jgraley commented 2 years ago

Ticket has fuzzy scope. One not-yet-done item moved to own ticket #445. Other stuff either done or has own ticket.

jgraley commented 2 years ago

Distributing early

Better: distributivity in logic works both ways. So

(!b1 & !b2 & b3) | (b1 & b2) becomes ((!b1 & !b2 & b3) | b1) & ((!b1 & !b2 & b3) | b2) and then (!b1 | b1) & (!b1 | b2) & (!b2 | b1) & (!b2 | b2) & (b3 | b1) & (b3 | b2) remove tautologous clauses (!b1 | b2) & (!b2 | b1) & (b3 | b1) & (b3 | b2) Which literals are expected to be evaluatable (that is, which ones don't depend on x) - say { b1 } wlog do implies based on b1 (b1 ⇒ b2) & (!b1 ⇒ !b2) & (!b1 ⇒ b3) & (b3 | b2) Now we suspect b3 and b2 both depend on target so b3 | b2 is hard to evaluate (b1 ⇒ b2) & (!b1 ⇒ !b2) & (!b1 ⇒ b3) distributing back over implies: (b1 ⇒ b2) & (!b1 ⇒ (!b2 & b3)) or b1 ? b2 : (!b2 & b3) which solves for x as x = b1 ? (x: b2) : (x: (!b2 & b3)) Solves on conjunctions can simply pick the easiest one x = b1 ? (x: b2) : ((x: !b2) otherwise (x: b3)) We won't be able to solve !b2 for x (it's really !(x==MMAX)) so try to solve b3 so we'll end up with x = b1 ? (x: b2) : (x: b3)

jgraley commented 2 years ago

Early otherwise and tabulation

We could probably pick up from (b1 ⇒ b2) & (!b1 ⇒ !b2) & (!b1 ⇒ b3) & (b3 | b2) and immediately involve x as follows: x = (x: b2 if b1) otherwise (x: !b2 if !b1) otherwise (x: b3 if !b1) otherwise hard and we drop the hard clause

Now this looks like a tabulated by-cases thing eg

    { x: b2  if b1
x = { x: !b2 if !b1
    { x: b3 if !b1

Except of course that a condition was repeated leading to 

x = { x: b2  if b1
    { (x: !b2) otherwise (x: b3)  if !b1

and because (x: !b2) is hard,

x = { x: b2  if b1
    { x: b3  if !b1

Tabulation doesn't seem to have much advantage and is unwieldy. Also for evaluatable solution expressions, we want to lock-in complete coverage of cases, this the repeated appearance of b1 (i..e if b but also if !b1) looks like unwanted redundancy.

jgraley commented 2 years ago

More about ?:

Generally: a ? b : c === (a ⇒ b) & (!a ⇒ c) a ⇒ b === a ? b : TRUE (TRUE follows from false-implies-anything)

We're assuming that x : (a ? b : c) Assume a does not depend on x, then x : (a ? b[x: b] : c[x: c]) solves to (note: ?: switches from bool to symbol here) x = (a ? (x: b) : (x: c))

Can't really break that deduction into smaller steps, but looks safe.

jgraley commented 2 years ago

Alternative default MMAX expression

What if we began with (b1 == b2) & (!b2 ⇒ b3) (note: chosen as harder case)

Identifying b1 as not dependent on x we try to substitute b1 for equivalent expressions: We have: b1 indep x; b2 cannot be solved for x. We thus try and solve for b2 and get b1. (b1 == b2) & (!b1 ⇒ b3)

Switching to b1-implies we get (!b1 ⇒ !b2) & (b1 ⇒ b2) & (b1 ⇒ b3) b1 ? b2 : !b2 & b3

But... the initial form is a conjunction and will be split into two constraints. Fixed: see #461

Example constraint after #461 and adding == and ⇒:

R041 }}P Consistency expression:
([#0->StandardAgent<Expression>#B-782] != #0->MMAX#-0 ⇒ 
   Item<Case@0:sing>([#0->StandardAgent<Case>#B-775]) == [#0->StandardAgent<Expression>#B-782]) &
([#0->StandardAgent<Expression>#B-782] == #0->MMAX#-0) == 
   ([#0->StandardAgent<Case>#B-775] == #0->MMAX#-0)
jgraley commented 2 years ago

How I did it:

Relevant #463 #464 #476 #465