Generating lists of satisfying values for a set of constraints

Question

Given a set of constraints, I would like to efficiently generate the set of values.

Suppose I have a few constraints on my Thungus[1]:

goodThungus(X) :-
               X > 100,
               X < 1000.
               sin(X) = 0.

Now, I can check a Thungus by asking:

goodThungus(500).

I would like to generate all good Thungi. I'm not sure how to do that; I'm really not sure about how to do it efficiently.

Note: this of course has to be a computable generation.

[1] Arbitrary object selected for this example.

Answer 1

What you are asking for can't be done in the full general case: imagine doing f(X) = 0 where f is a function for which the roots cannot be analytically determined, for example. Or suppose f(X) is the function "does the program X halt?". No computer is going to solve that for you.

Your options are basically to either:

• Limit the set of constraints to things that you can reason about. e.g. inequalities are good because you can identify ranges, then do intersections and unions on ranges efficiently etc.

• Limit the set of values to a small enough number that you can test them individually against each of the constraints

UPDATE: For the kind of constraints stated in the question (ranges of real values and real-valued functions that can be analytically solved and have a finite number of solutions within any range) I would suggest the following approach:

• Write a generating function that can iteratively return solutions for you function within a given range... this will need to be done analytically e.g. exploiting the fact that sin(X)=0 implies X=n*pi where n is any integer.
• Do interval arithmetic and bounding on your range constraints to work out the range(s) that need to be scanned (in the example you would want the range 100 < X < 1000)
• Apply your generating function to each of the target ranges in order to create all of the possible solutions.

Answer 2

He is searching any X in [100..1000] for that sin(x) = 0. But this is a pure mathematical problem, and not meant for relational logical deduction / backtracking. simple Prolog is not suited for this?

Answer 3

I'll preface my suggestion by stating that I'm no expert in using numerical constraint logic programming systems, but here goes...

On the surface, I'd think that solving this kind of problem in PROLOG would be best suited to a numerical constraint logic programming system, perhaps such as CLP(R) (for reals) in SWI-PROLOG; unfortunately, the specific problem you've asked for is seeking to solve for a set of constraints including a non-linear constraint, which seems to be not well or widely supported amongst PROLOG implementations; instead, they seem to deal mainly with linear constraints and often have limited support for non-linear constraints such as X = sin(Y), for example.

Take SWI-PROLOG's CLP(R) library, and the following example program:

:- use_module(library(clpr)).

report_xsq_zeros :-
    findall(X, {0 = (X * X) - 10}, Results),
    write_ln(Results).

report_sin_zeros :-
    findall(X, {0 = sin(X)}, Results),
    write_ln(Results).

Now, executing report_xsq_zeros gives us:

 ?- report_xsq_zeros.
[3.16228, -3.16228]
true.

Here, the system correctly computed the zeros of the quadratic x^2 - 10, which are indeed approximately 3.16228 and -3.16228, where the range of X was unbounded. However, when we execute report_sin_zeros, we get:

 ?- report_sin_zeros.
[0.0]
true.

We see that the system only computed a single zero of the function sin(X), even though the range of X was indeed also unbounded. Perhaps this is because it is recognized that there are an infinite number of solutions here (though I'm only guessing...). If we were to program what you've asked for:

report_sin_zeros :-
    findall(X, {X > 100, X < 1000, 0 = sin(X)}, Results),
    write_ln(Results).

We get no results, as the underlying system only computed a single zero for sin(X) as shown earlier (i.e., binding X to 0.0 which lies outside the stated range):

 ?- report_sin_zeros.
[]
true.

I conclude that I've either not demonstrated proper usage of SWI-PL CLP(R) (I suggest you look into it yourself), or it won't solve your specific (non-linear) problem. Other CLP(R) implementations may behave differently to SWI-PROLOG CLP(R), but I don't have them installed so I can't check, but you could try SICSTUS CLP(R) or others; the syntax looks similar.