eyeprolog

Integer partitions

In how many ways can a number be written as a sum?

The number 4 can be written as 4, 3+1, 2+2, 2+1+1 and 1+1+1+1: five partitions, where order does not matter. Counting them by brute force explodes quickly. This example counts them with a two-branch recursion and lets tabling remember every subproblem, a dynamic program written as logic.

Run it in the playground · Source

The question

How many partitions do 12 and 15 have? How many partitions of 16 use parts no larger than 5? And what is the total number of partitions of 1 through 8?

The recursion

partitions(N, K, Count) counts the partitions of N into parts no larger than K. Every such partition either uses a part of size K or it doesn’t:

partitions(N, K, Count) :-
  (N > 0),
  (K > 0),
  (K =< N),
  (Remainder is N - K),
  partitions(Remainder, K, Withk),
  (K1 is K - 1),
  partitions(N, K1, Withoutk),
  (Count is Withk + Withoutk).

Using a K leaves N - K to partition with parts up to K; not using it leaves N with parts up to K - 1. Base cases: zero has exactly one partition (the empty sum), and a positive number with no parts allowed has none.

Remembering subproblems

:- table partitions/3.

The two branches reach the same (N, K) pairs again and again. The table stores each answer the first time it is computed and reuses it afterwards, turning an exponential search into a fast computation. The relation means the same with or without the table; only the work changes.

The answer

eyeprolog examples/integer-partitions.pl

partition_answer(p_12, 77).
partition_answer(p_15, 176).
partition_answer(p_16_using_parts_at_most_5, 101).
partition_answer(cumulative_p_1_to_8, 66).

p(12) = 77 and p(15) = 176, matching the published values of the partition function.

The reason

eyeprolog --proof examples/integer-partitions.pl

step(partition_answer(p_12, 77), rule(7), ['Count' = 77], [partition_count(12, 77)]).
step(partition_count(12, 77), rule(6), ['N' = 12, 'Count' = 77], [partitions(12, 12, 77)]).

p(12) = 77 because partitions(12, 12, 77) holds. That step splits into Withk = 1 (the partition “12” itself) and Withoutk = 76 (all partitions using parts up to 11), and so on down to the base cases. Because each conclusion gets one step, a shared subproblem is proved once and cited wherever it is used; the whole proof has 476 steps.

The check

condition('C1', resolution, ok, 168).
condition('C5', re_decision, ok, 307).
obligation(builtin, theory_scoped, sumall(A, (between(1, 8, B), partition_count(B, A)), 66)).
verdict(checked_with_obligations).

168 rule steps replay and 307 arithmetic steps are recomputed. One step is an obligation: the sumall/3 total of 66 depends on the program’s own partition_count/2, so the checker cannot recompute it in isolation and records it as a trusted boundary. Everything else is checked.

Try it

Add partition_answer(p_5, C) :- partition_count(5, C). and check the answer, 7, by listing the partitions of 5 by hand.
Ask for p(100). With the table it answers 190569292 in well under a second; remove :- table partitions/3. and see how far you get.
Count partitions into distinct parts by changing one recursive call.

Learn more in The Art of EyeProlog, Chapter 13.

This site is open source. Improve this page.