CODEWITHSUNDEEP
constraintssolversmt
jandek
jandek

Reputation: 66

Can a constraint solver handle constraints that are nested logical clauses?

I have a typical constraint problem:

For 10 variables x_1,x_2,... x_10 find an assignment of values to variables, where values come from the domain [1,2...1000].

However, my constraints are nested logical expressions of the following form: (x_1 = 4 AND x_2 = 5) OR (x_1 = 2 AND x_2 = 7) OR ... (x_1 = 22 AND x_3 = 1)

Essentially, every pair of variables has some set of possible assignments. The same goes for all triples of variables, and 4-tuples.

My question is: what kind of constraint solver should I use here? Is there a more efficient way to solve this kind of assignment problem? I'm concerned that the number of AND clauses will be very large, and the solver won't be able to take advantage of any numerical properties of the variables, since there really aren't any. Thanks!

Upvotes: 0

Views: 32

Answers (1)

Michal
Michal

Reputation: 405

Probably the easiest way to implement your problem would be by using OR-Tools CP-SAT solver. I wouldn't worry about amount of constrains. This solver handles large-scale problems with ease.

Upvotes: 1

Related Questions