1
$\begingroup$

I have an interesting little problem that I believe can be formulated in terms of optimization or constraint programming. I have a few dozen variables $a$, $b$, $c$ ... and a set of constraints that establish relations between them, such as $a < b$. Some of these constraints are "turned on" by binary indicator variables: $b < c\:|\:(ind_x = True)$. We know the value of some of these binary variables, but not all of them. The goal here is to solve the system such that we can quickly answer questions about the relations between pairs of non-binary variables ("What is the relation between $a$ and $c$?"). Answers could be:

  • $a < c$
  • $a = c$
  • $ a > c$
  • the relationship between $a$ and $c$ cannot be determined with the information available.

My first instinct was to formulate this as a constraint satisfaction problem. I defined the domain of each non-binary variable to be the set of positive nonzero integers, encoded conditional constraints as $b * ind_x < c$ (always true if the indicator is 0, and if the indicator is 1, only true if $b<c$), and provided unconditional constraints ($ a<b$) as-is. Then I would take one of the feasible solutions, for example:

PROBLEM:
a < b
b < c
a < d

SOLUTION:
a = 0
b = 1 
c = 2
d = 1

This works great for answering some questions -- for example, if we ask for the relation between $a$ and $c$, we can conclude from $a=0$ and $c=1$ that $a < c$.

But if we ask for the relationship between $b$ and $d$, the fact that $b = d = 1$ is misleading, because the following is also a viable solution:

a = 0
b = 1 
c = 2
d = 99

In fact, the relationship between $b$ and $d$ is impossible to determine given the available information. We could iterate over all the feasible solutions of this CSP, and check the relationship between $b$ and $d$ in each one, but this is too slow. We could also try adding constraint $b < d$ and solving for feasibility, then doing the same for $b > d$, etc., but this seems cumbersome as well.

Is there a more elegant way to formulate this problem that I am not aware of? Any ideas or suggestions would be much appreciated. Thank you!

$\endgroup$

1 Answer 1

2
$\begingroup$

You should have a look at Satisfiability Modulo Theories or SMT for short. A huge number of problems can be thought of as instances of SMT for a particular theory. For example, correctly designing certain types of integrated circuits can be phrased as an SMT problem. The problem you're describing fits under the theory of quantifier-free linear integer arithmetic. There are also theories of real arithmetic and many others. As you've pointed out, many of these problems have more than one answer. Most SMT solvers will tell you that either (1) a formula is unsatisfiable or (2) it is satisfiable and give you one particular answer.

If you're looking for a software tool that can solve SMT problems, I'd recommend Z3. Regardless of which tool you do go with, there's a standardized domain-specific language for expressing SMT problems called SMT-LIB. If you want to learn about how tools like Z3 work under the hood, you should read about the Davis-Putnam-Logeman-Lowell or DPLL algorithm.

Questions about SMT solvers and the like might get more answers on the CS stack exchange, it's maybe a little bit more their bailiwick.

$\endgroup$
3
  • $\begingroup$ Awesome, thank you for the answer, and especially for the links to those resources. These techniques are a bit outside my research area, so the background reading will be very useful for me. I'll report back here if I get this working (and maybe head over to the CS stack exchange too) $\endgroup$ Commented Oct 11, 2020 at 21:07
  • $\begingroup$ It's so cool every time I see a question I have no idea about, and someone shows up who really knows their stuff and provides exactly the right references to the literature! $\endgroup$ Commented Oct 12, 2020 at 23:45
  • $\begingroup$ In case you are curious -- I did some reading, narrowed down the question a bit, and posted the result on the CS stack exchange: cs.stackexchange.com/questions/132387/… $\endgroup$ Commented Nov 18, 2020 at 14:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.