Prolog query with constraint returns false, but there are answers

Question

I am trying to write a prolog program that works out which course I can choose in the university course catalog. Each course has a unique code like cs180 and each course may have some prerequisite courses, which means the required courses must be finished before registering for this course.

Assuming that there's no circular dependency of courses, all courses in the university form a directed graph with no loops.

req(ma262, [ma261,ma182,ma174,ma271,ma27101,ma172,ma263]).
req(ma351, [ma174,ma172,ma182,ma261,ma271,ma27101,ma263]).
req(ma366, [ma351,ma265]).
req(ma341, [ma174,ma172,ma182,ma261]).
req(ma440, [ma35301]).
req(ma35301, [ma265,ma351]).
req(cs314, [ma262,ma265,ma350,ma351]).
req(cs314, [cs180,cs158,cs177,cs159]).
ok(ma172).
ok(cs180).

In this program, req(A,B) indicates that: to register for class A, I must complete at least one course from the list of classes B. If there's multiple statements of requirement, then all of the requirements must be met. For example, to register for cs314, I need to complete one course from both lists. ok/1 indicates that I've already completed the course.

Then I define a valid scheme as a list of courses such that each class in the list is either

1. completed, or
2. some other classes in the list fulfills its requirement.

For example, [ma172] is a valid scheme as it's completed. [ma172,ma262] is a valid scheme since the requirement of ma262 can be met with ma172.

Here's my code.

valid(Cs):-
    is_set(Cs), /*Cs is distinct*/
    maplist({Cs}/[C]>>( /*for each class in Cs*/
                      ok(C); /*either completed, or meets requirements*/
                      (setof(P,req(C,P),Ps), /*get all requirements*/
                       maplist({Cs}/[L]>>( /*check all requirements*/
                                         member(X,L),
                                         (member(X,Cs);ok(X))
                                         
                                         ),Ps)
                      )),Cs).

When I query ?- valid(N) , prolog simply returns [] and then false. However, these examples hold true:

?- valid([ma366,ma351])
   true
?- valid([ma366,ma351,ma172])
   true

I don't know why the solver doesn't work correctly. If my code breaks the monotonicity, would you like to point out where? And how should I change my code to get it to work?

Answer 1

Based on context I'm assuming you're using SWI-Prolog. SWI's is_set/1 predicate is not very logical:

?- Set = [a, b, c], is_set(Set).
Set = [a, b, c].

?- is_set(Set), Set = [a, b, c].
false.

And this is the main problem with your code, since calling valid(Cs) will call is_set(Cs) with a free variable Cs, which will fail:

?- is_set(Cs).
false.

A simple way to work around this is to accept that is_set/1 is not logical and to move the call to the end of your definition. Operationally, this means that your big maplist goal will generate lots of non-sets which you then test and throw away.

A nicer way is to exploit the logical behavior of dif/2 constraints.

We can define:

nonmember_of(_X, []).
nonmember_of(X, [Y | Ys]) :-
    dif(X, Y),
    nonmember_of(X, Ys).

which behaves like:

?- nonmember_of(X, [A, B, C]).
dif(X, C),
dif(X, B),
dif(X, A).

and based on this:

alldif([]).
alldif([X | Ys]) :-
    nonmember_of(X, Ys),
    alldif(Ys).

which acts as a nicer replacement for is_set/1:

?- alldif([A, B, C]).
dif(A, C),
dif(A, B),
dif(B, C).

?- Set = [a, b, c], alldif(Set).
Set = [a, b, c] ;
false.

?- alldif(Set), Set = [a, b, c].
Set = [a, b, c] ;
% nontermination, but it's better than nothing

and can also be used with a completely free argument:

?- alldif(Xs).
Xs = [] ;
Xs = [_2154] ;
Xs = [_2604, _2610],
dif(_2604, _2610) ;
Xs = [_2902, _2908, _2914],
dif(_2902, _2914),
dif(_2902, _2908),
dif(_2908, _2914) ;
Xs = [_3320, _3326, _3332, _3338],
dif(_3320, _3338),
dif(_3320, _3332),
dif(_3320, _3326),
dif(_3332, _3338),
dif(_3326, _3332),
dif(_3326, _3338) ;

Given this you can use alldif as a drop-in replacement for is_set in your original definition, and you will be able to generate answers:

?- valid(Courses).
Courses = [] ;
Courses = [ma172] ;
Courses = [cs180] ;
Courses = [ma262] ;
Courses = [ma341] ;
Courses = [ma351] ;
Courses = [ma172, cs180] ;
Courses = [ma172, ma262] ;
Courses = [ma172, ma262] ;
Courses = [ma172, ma341] .

?- length(Courses, 5), valid(Courses).
Courses = [ma172, cs180, cs314, ma262, ma341] ;
Courses = [ma172, cs180, cs314, ma262, ma341] ;
Courses = [ma172, cs180, cs314, ma262, ma351] ;
Courses = [ma172, cs180, cs314, ma262, ma351] .

Note that there are some duplicates here. Also note that, if you were to enumerate all the finitely many solutions, the predicate would not terminate because alldif would try to enumerate longer and longer lists. You can avoid that by bounding the length of the list by the total number of courses.

Edit: To demonstrate that implementing this using dif isn't just an exercise in "making things pure out of academic interest", but actually a very practical issue, consider the performance of the variant with dif:

?- length(Cs, 7), time(valid(Cs)).
% 96,569 inferences, 0.012 CPU in 0.012 seconds (100% CPU, 7886094 Lips)
Cs = [ma172, cs180, cs314, ma262, ma341, ma351, ma35301] .

?- length(Cs, 8), time(valid(Cs)).
% 804,129 inferences, 0.053 CPU in 0.053 seconds (100% CPU, 15080361 Lips)
Cs = [ma172, cs180, cs314, ma262, ma341, ma351, ma35301, ma366] .

?- length(Cs, 9), time(valid(Cs)).
% 6,204,344 inferences, 0.394 CPU in 0.394 seconds (100% CPU, 15766728 Lips)
Cs = [ma172, cs180, cs314, ma262, ma341, ma351, ma35301, ma366, ma440] .

In contrast, generate-and-test with is_set at the end of the predicate definition does not scale well at all:

?- length(Cs, 7), time(valid(Cs)).
% 84,099,589 inferences, 11.362 CPU in 11.362 seconds (100% CPU, 7402118 Lips)
Cs = [ma172, cs180, cs314, ma262, ma341, ma351, ma35301] .

?- length(Cs, 8), time(valid(Cs)).
% more than 3 minutes, didn't want to wait longer

This is because generate-and-test generates an exponential number of non-sets that must be rejected afterwards. Using dif the corresponding constraints reject non-sets much earlier, as soon as the search procedure tries to construct even a partial non-set.