Too large an expression?

[CrashBurnRepeat]

Hi @ztangent,

I was recently trying to put together a demonstration of logical programming using the 4 color theorem to color a map of the US. Although the code is relatively simple, the logical expressions are quite large; they're show below:

color_pairs = @julog [
    n(red, green)<<=true,
    n(green, red)<<=true,
    n(blue, red)<<=true,
    n(yellow, red)<<=true,
    n(red, blue)<<=true,
    n(green, blue)<<=true,
    n(blue, green)<<=true,
    n(yellow, green)<<=true,
    n(red, yellow)<<=true,
    n(green, yellow)<<=true,
    n(blue, yellow)<<=true,
    n(yellow, blue)<<=true
]

map_layout_all = @julog colors(AK, AL, AR, AZ, CA, CO, CT, DC, DE, FL, GA, HI, IA, ID, IL, IN, KS, KY, LA, MA, MD, ME, MI, MN, MO, MS, MT, NC, ND, NE, NH, NJ, NM, NV, OH, OK, OR, PA, RI, SC, SD, TN, TX, UT, VA, VT, WA, WI, WV, WY)<<=
    n(AL, FL) & n(AL, GA) & n(AL, MS) & n(AL, TN) &
    n(AR, LA) & n(AR, MS) & n(AR, MO) & n(AR, OK) & n(AR, TN) & n(AR, TX) &
    n(AZ, CA) & n(AZ, NM) & n(AZ, NV) & n(AZ, UT) &
    n(CA, OR) & n(CA, NV) &
    n(CO, KS) & n(CO, NE) & n(CO, NM) & n(CO, OK) & n(CO, UT) & n(CO, WY) &
    n(CT, MA) & n(CT, NY) & n(CT, RI) &
    n(DE, MD) & n(DE, NJ) & n(DE, PA) &
    n(FL, GA) &
    n(GA, NC) & n(GA, SC) & n(GA, TN) &
    n(ID, MT) & n(ID, NV) & n(ID, OR) & n(ID, UT) & n(ID, WA) & n(ID, WY) &
    n(IL, IA) & n(IL, IN) & n(IL, KY) & n(IL, MO) & n(IL, WI) &
    n(IN, KY) & n(IN, MI) & n(IN, OH) &
    n(IA, MN) & n(IA, MO) & n(IA, NE) & n(IA, SD) & n(IA, WI) &
    n(KS, MO) & n(KS, NE) & n(KS, OK) &
    n(KY, MO) & n(KY, OH) & n(KY, TN) & n(KY, VA) & n(KY, WV) &
    n(LA, MS) & n(LA, TX) &
    n(ME, NH) &
    n(MD, PA) & n(MD, VA) & n(MD, WV) &
    n(MA, NH) & n(MA, NY) & n(MA, RI) & n(MA, VT) &
    n(MI, OH) & n(MI, WI) & n(MI, MN) & #MI and MN share a water border
    n(MN, ND) & n(MN, SD) & n(MN, WI) &
    n(MS, TN) &
    n(MO, NE) & n(MO, OK) & n(MO, TN) &
    n(MT, ND) & n(MT, SD) & n(MT, WY) &
    n(NE, SD) & n(NE, WY) &
    n(NV, OR) & n(NV, UT) &
    n(NH, VT) &
    n(NJ, NY) & n(NJ, PA) &
    n(NM, OK) & n(NM, TX) &
    n(NY, PA) & n(NY, VT) & n(NY, RI) & #NY and RI share a water border 
    n(NC, SC) & n(NC, TN) & n(NC, VA) &
    n(ND, SD) &
    n(OH, PA) & n(OH, WV) &
    n(OK, TX) &
    n(OR, WA) &
    n(PA, WV) &
    n(SD, WY) &
    n(TN, VA) &
    n(UT, WY) &
    n(VA, WV) &
    n(DC, VA) & n(DC, MD)

goal_all = @julog colors(AK, AL, AR, AZ, CA, CO, CT, DC, DE, FL, GA, HI, IA, ID, IL, IN, KS, KY, LA, MA, MD, ME, MI, MN, MO, MS, MT, NC, ND, NE, NH, NJ, NM, NV, OH, OK, OR, PA, RI, SC, SD, TN, TX, UT, VA, VT, WA, WI, WV, WY)
map_soln_all = resolve(goal_all, vcat(color_pairs, map_layout_all), mode=:any, search=:dfs)

When I first ran this without any options set in resolve, the solver failed to finish after about an hour, and considering the size of the search space (~4^51 I believe) this didn't seem unreasonable. I then hoped that setting mode=:any and search=:dfs would solve in a reasonable amount of time for a single solution, but I also had to halt the solver after a half an hour had passed.

I wanted to see if this second attempt (trying to find any solution via depth-first search) is one you would have expected to finish in a "reasonable" amount of time, or if this is simply too large a problem even for those options.

Also as a side note, it seems like there's no validity check with the resolve options, and any invalid option choice will just "fail" silently by using the default settings. Am I reading the code correctly for these cases?

Thanks as always!

[ztangent]

Hey @CrashBurnRepeat! Yes, I believe this is too large a problem instance to solve without using more specialized search techniques that implement constraint propagation. The standard SLD resolution algorithm doesn't do any of that constraint propagation, so it generally won't be able to solve problems of this size in a reasonable time. (In addition, based on my benchmarks, Julog is still considerably slower than SWI-Prolog, despite my recent performance improvements.) I believe it should still work if you give it a smaller problem to solve though -- maybe just color all the territories / provinces in Canada instead?

Also as a side note, it seems like there's no validity check with the resolve options, and any invalid option choice will just "fail" silently by using the default settings. Am I reading the code correctly for these cases?

Yes, invalid option names currently fail silently -- thanks for noticing. If you could file a separate issue for that, that'd be great!

[ztangent]

Note that most modern variants of Prolog actually have support for constraint propagation via specialized libraries. E.g. the 4-color problem would typically be solved with the help of the clpfd library in Prolog:

https://www.swi-prolog.org/pldoc/man?section=clp

[CrashBurnRepeat]

I believe it should still work if you give it a smaller problem to solve though -- maybe just color all the territories / provinces in Canada instead?

Yes, I ended up using the Midwest (plus Kentucky, just to add a few more interesting constraints). I even made a GIF of some of the solutions!

Thanks for the links for constraint satisfaction, and I'll go make a separate issue about options checking.

[ztangent]

Nice GIF! :D Glad it worked there. Thanks for opening the other issue - will close this one.