Question about SAT solver

[stef...@aylonvalue.com]

Trying to migrate from the constraint solver to SAT. I need to know what is the replacement of the MakeCount call, if anyone can help. (C#)

[Laurent Perron]

The idea would be to create literals equal to x == i, then sum them.

See https://github.com/google/or-tools/blob/master/ortools/sat/doc/channeling.md

Now, for modeling purposes, SAT is much closer to MIP that to CP. And you could ask the question if you really need integer variables, or just boolean variables.

You can also use AddMapDomain() that maps an integer variable onto a list of boolean literals. It is implemented using a the same ideas as in the channeling document.

I hope this helps.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

Le mer. 8 août 2018 à 02:08, <stef...@aylonvalue.com> a écrit :

Trying to migrate from the constraint solver to SAT. I need to know what is the replacement of the MakeCount call, if anyone can help. (C#)

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.