<p>I have encountered a constraint problem and I would like to know if there exists a name and implemented solvers for this type of constraint problem.</p>

<p>My constraints are of the forms.</p>

<p>1) $CONSTANT \in S$</p>

<p>Constant can be either a number, or a term f(a,b),a,f(f(a)),...
S is a finite set of objects(numbers or terms without variables)</p>

<p>Example: $1 \in \{3,4,5,a\}$</p>

<p>2) $VARIABLE \in S$</p>

<p>Example: $X \in \{a,b,c\}$</p>

<p>3) $ARITHMETIC\_EXPRESSION(VAR_1,VAR_2,\ldots VAR_N) \in S$</p>

<p>Example: $X^5-Y^4+1 \in \{1,2,4\}$</p>

<p>4) $TERM_1 \odot TERM_2$,</p>

<p>where $\odot$ is relation (&lt;,>,=,!=) and $TERM_1$ and $TERM_2$ are either variables or terms.
I assume that relations are partially defined on numbers and TERMS without variables.</p>

<p>5) $Constraint \diamond Constraint$ ,where $\diamond$ is logical operator (or, and,etc).</p>

<p>6) $\neg Constraint$</p>

<p>Solution to the constraint problem is assignment of constants <strong>from given finite set of integers and terms</strong> to variables which turns it to true. </p>

<p>Example problem:</p>

<p>$X\in \{a,b,c\} \land Y \not \in \{c,d,e\} \land X&lt;Y$</p>

<p>Given finite set: $\{a,b,e\}$</p>

<p>Solution is, for example $X=a, Y=e$.</p>

<p>I want to know </p>

<ol>
<li><p>What is the name of this type of constraint problem.</p></li>
<li><p>which algorithms should I use to solve the problem and </p></li>
<li><p>If there exist an implementation (preferable in Java language) to solve it.</p></li>
</ol>

<p>Notice that the case that we need to find a solution from a finite set is crucial (otherwise the problem is unsolvable, since only arithmetic constraint are Diophantus systems)</p>

CC BY-SA 3.0
2013-04-17T07:24:05.273Z
This problem is at the very least NP-hard, e.g. by arithmetization of SAT. You can probably also reduce it to SAT, and use a SAT-solver.
Shaull
CC BY-SA 3.0
2013-04-17T13:05:37.200Z
The constraints you list are supported by any SMT solver, and most constraint solvers.  But I am confused by the first one: matching terms can be _very_ hard, could you give more details?
András Salamon
CC BY-SA 3.0
2013-04-17T17:27:15.487Z
The first one is just check if given term is in the set. Both term and the set are ground (constants). For example, $f(a)\in \{a,b,c,d,f(g)\}$ There is nothing to do with matching terms. I could actually drop the first one without any loss. And thank you for mentioning SMT solver, I will check them!
Evgenii.Balai
<csp>
Constraint problem
Evgenii.Balai
# Constraint problem

(Asked by: username_0 on 2013-04-17)

I have encountered a constraint problem and I would like to know if there exists a name and implemented solvers for this type of constraint problem.

My constraints are of the forms.

1) $CONSTANT \in S$

Constant can be either a number, or a term f(a,b),a,f(f(a)),...
S is a finite set of objects(numbers or terms without variables)

Example: $1 \in \{3,4,5,a\}$

2) $VARIABLE \in S$

Example: $X \in \{a,b,c\}$

3) $ARITHMETIC\\_EXPRESSION(VAR\_1,VAR\_2,\ldots VAR\_N) \in S$

Example: $X^5-Y^4+1 \in \{1,2,4\}$

4) $TERM\_1 \odot TERM\_2$,

where $\odot$ is relation (<,>,=,!=) and $TERM\_1$ and $TERM\_2$ are either variables or terms.
I assume that relations are partially defined on numbers and TERMS without variables.

5) $Constraint \diamond Constraint$ ,where $\diamond$ is logical operator (or, and,etc).

6) $\neg Constraint$

Solution to the constraint problem is assignment of constants **from given finite set of integers and terms** to variables which turns it to true.

Example problem:

$X\in \{a,b,c\} \land Y \not \in \{c,d,e\} \land X

Given finite set: $\{a,b,e\}$

Solution is, for example $X=a, Y=e$.

I want to know

1. What is the name of this type of constraint problem.
2. which algorithms should I use to solve the problem and
3. If there exist an implementation (preferable in Java language) to solve it.

Notice that the case that we need to find a solution from a finite set is crucial (otherwise the problem is unsolvable, since only arithmetic constraint are Diophantus systems)

**Tags:** csp

> **Comments:**
> **username_1**: This problem is at the very least NP-hard, e.g. by arithmetization of SAT. You can probably also reduce it to SAT, and use a SAT-solver.  
> **username_2**: The constraints you list are supported by any SMT solver, and most constraint solvers.  But I am confused by the first one: matching terms can be _very_ hard, could you give more details?  
> **username_0**: The first one is just check if given term is in the set. Both term and the set are ground (constants). For example, $f(a)\in \{a,b,c,d,f(g)\}$ There is nothing to do with matching terms. I could actually drop the first one without any loss. And thank you for mentioning SMT solver, I will check them!  

---

## 0 answers

