Add binary numbers

General
1

I’m trying to do a bit of SAT solving as part of a AoC problem. I’ve written out what I think should be a CLP(B) compatible binary adder, which should be of the form add(+,+,+,+) and work in every direction. Note that it assumes the inputs are reversed and the output is given in reverse for problem specific convenience.

:- use_module(library(clpb)).

add([], [], [Carry], Carry).
add([X|Xs], [Y|Ys], [Z|Zs], CarryIn) :-
    sat(Z =:= (X # Y # CarryIn)),
    sat(CarryOut =:= ((X * Y) + (X * CarryIn) + (Y * CarryIn))),
    add(Xs, Ys, Zs, CarryOut).

It works well enough for concrete inputs, and you can write add([A,B,C], [D,E,F], Out, 0), and it will write out the SAT constraints for the output Out. Trouble is that it will blow the stack when the inputs get a bit bigger like this:

add([A,B,C,D,E],[F,G,H,I,J],Out,0).

Is this reasonable behaviour? How do I write the predicate I want?

2

I think I’ve answered this question. From here:

By default, CLP(B) residual goals appear in (approximately)
algebraic normal form (ANF). This projection is often
computationally expensive. We can set the Prolog flag
clpb_residuals to the value bdd to see the BDD
representation of all constraints.

Setting :- set_prolog_flag(clpb_residuals, bdd). fixes it.

1 Like