Translation from Conjure-Oxide Model to CNF KissSAT

[gskorokhod]

No description provided.

[niklasdewally]

From in-person review of the tests with @gskorokhod:

Test cases sometimes fail due to variables being assigned numbers in CNF arbitrarily.

We need some way of storing ordering of variables so we can test this, and we can convert solutions back from CNF to Model.

@gskorokhod suggested doing a sort over the string and integers inside Name, but we would appreciate any ideas @ozgurakgun @lixitrixi .

[niklasdewally]

I think this needs to be represented inside the SymbolTable / AST somehow - I imagine having a cannonical ordering of variables would help with other things too, and should be solver independant?

[ozgurakgun]

I think this needs to be represented inside the SymbolTable / AST somehow - I imagine having a cannonical ordering of variables would help with other things too?

Absolutely. The variables have to be called 1..n, so a central function which generates the next name in order makes sense. When we generate the, say, direct encoding for an integer variable we should remember the variables used for this and avoid regenerating the same x=1 sat variables again and again.

How are the variables assigned to numbers at the moment?

[ozgurakgun]

One way of structuring this in the code could be giving variables a method to return their direct encoding sat-variable-numbers (creating them if necessary).

Example: When converting x<=y for find x,y:int(1..3). We want to say !(x=2 /\ y=1), !(x=3 /\ y=1), !(x=3 /\ y=2)`. (Sometimes it's easier to think about what's not allowed, since negation-of-and after de morgan is a disjunction.)

Also: we can simplify the above to !(x=2 /\ y=1), !(x=3 /\ y!=3)

De Morgan x!=2 \/ y!=1), x!=3 \/ y=3

CNF-like !x_2 \/ !y_1), !x_3 \/ y_3

In pseudo-rust:

• Or([ Not(x.directEncoding(2)), Not(y.directEncoding(1) ])
• Or([ Not(x.directEncoding(3)), y.directEncoding(3) ])

And directEncoding will modify the a symbol table in the model to remember what number corresponds to x=1 etc.

Does this make sense?

[gskorokhod]

I should have a working implementation now, but there's no documentation yet and no proper error types

[gskorokhod]

I have also implemented converting from CNF back to an expression - idk if this is actually needed

[ChrisJefferson]

I think this looks reasonable -- obviously things to overhaul (like the error types), but none of that stops a MVP merge.

Should probably remove the '.idea' directories (and maybe add to .gitignore, to avoid them in future?)

[ozgurakgun]

hi @gskorokhod - if you remove the unnecessary files we can merge this.

[gskorokhod]

removed the .idea directory!
By the way, do we need .vscode?
It may be useful to have project configuration, but also it's user specific

[niklasdewally]

removed the .idea directory! By the way, do we need .vscode? It may be useful to have project configuration, but also it's user specific

We should keep any editor config that is in .gitignore, and remove the rest.

[gskorokhod]

@ChrisJefferson @ozgurakgun I think this should be ready to merge now!

[ozgurakgun]

We should add parsing of !, /\, \/ (should be trivial from the astjson) and we can add some integration test cases that are already cnf, but in essence syntax.

Something like:

find x, y, z : bool
such that x \/ !y, !x \/ z

With the following solutions:

[
  {
    "x": false,
    "y": false,
    "z": false
  },
  {
    "x": false,
    "y": false,
    "z": true
  },
  {
    "x": true,
    "y": false,
    "z": true
  },
  {
    "x": true,
    "y": true,
    "z": true
  }
]

Maybe we shouldn't block this PR, but do this in another PR?

[niklasdewally]

We should add parsing of !, /\, \/ (should be trivial from the astjson) and we can add some integration test cases that are already cnf, but in essence syntax.

Something like:

find x, y, z : bool
such that x \/ !y, !x \/ z

With the following solutions:

[
  {
    "x": false,
    "y": false,
    "z": false
  },
  {
    "x": false,
    "y": false,
    "z": true
  },
  {
    "x": true,
    "y": false,
    "z": true
  },
  {
    "x": true,
    "y": true,
    "z": true
  }
]

Maybe we shouldn't block this PR, but do this in another PR?

I would appreciate it if you could stick this in an issue and tag it with the milestone - I might end up doing a little bit on this inter-semester.

@ozgurakgun should be ready to merge if you're happy?

[ozgurakgun]

Needs refactoring.

Refactored the PR in line with new changes, so this is probably no longer relevant

[gskorokhod]

@ozgurakgun @niklasdewally

Should be ready to merge! I've refactored my code to work with the new structure (mostly fixing imports, etc)
It all builds fine and the tests pass

[gskorokhod]

I've also added Display traits for Names and Expressions, which should help with printing errors

[niklasdewally]

LGTM 🚀