ADDED: CLP(B) port for SICStus Prolog with benchmarks and samples.

clpb/benchmarks/README

@@ -0,0 +1,34 @@
+This directory contains the benchmarks, shell scripts and data
+formatting to let you verify all results.
+
+Each benchmark file F must provide the predicate F(+N, -Sats), where N
+is the instance size and Sats is the list of clauses.
+
+The benchmark instances are specified in the file "instances".
+
+Run the following to gather all statistics:
+
+    $ ./run_swi.sh ; ./run_sicstus.sh
+
+You obtain Prolog facts that describe all results. For example:
+
+      % start: Sun May 22 09:35:21 CEST 2016
+      % langford 6
+      instance_attributes(swi, langford, 6, num_vars_clauses(45, 18)).
+      failed(swi, langford, 6, sat/1).
+      timing(swi, langford, 6, sat, time(826)).
+      failed(swi, langford, 6, maplist/2).
+      timing(swi, langford, 6, sats, time(823)).
+      tautology(swi, langford, 6, 0).
+      timing(swi, langford, 6, taut, time(829)).
+      % end: Sun May 22 09:35:24 CEST 2016
+
+Copy all these facts into facts.pl and run:
+
+    $ swipl -g latex_table -t halt bench.pl facts.pl
+
+This gives you LaTeX table rows that you can embed in your document.
+
+You can also view an ASCII table on the system terminal with:
+
+    $ swipl -g ascii_table -t halt bench.pl facts.pl

clpb/benchmarks/bench.pl

@@ -0,0 +1,174 @@
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   Definitions for benchmarking.
+
+   bench(+System, +B, +N, +Goal) produces the output for benchmark B(N),
+   where Goal is either sat, sats or taut.
+
+   latex_table/0 generates the table from the collected facts.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+:- use_module(library(clpb)).
+:- use_module(library(lists)).
+:- use_module(library(clpfd)).
+
+is_swi :- catch(current_prolog_flag(dialect, swi), _, fail).
+
+:- if(is_swi).
+:- set_prolog_flag(double_quotes, codes).
+:- else.
+:- use_module(library(between)).
+pairs_keys_values(Ps, Ks, Vs) :-
+        keys_and_values(Ps, Ks, Vs).
+:- endif.
+
+list_conj([], 1).
+list_conj([L|Ls], L*Goal) :- list_conj(Ls, Goal).
+
+bench(System, What, N, Goal) :-
+        call(What, N, Sats),
+        length(Sats, NumClauses),
+        term_variables(Sats, Vars),
+        length(Vars, NumVars),
+        (   Goal == sat ->
+            format("% ~w ~w\n", [What,N]),
+            portray_clause(instance_attributes(System, What, N, num_vars_clauses(NumVars, NumClauses)))
+        ;   true
+        ),
+        bench_(Goal, System, What, N, Sats, Time),
+        portray_clause(timing(System, What, N, Goal, Time)),
+        halt.
+
+bench_(sat, System, What, N, Sats, Time) :-
+        list_conj(Sats, Sat),
+        goal_time(System, What, N, sat(Sat), Time).
+bench_(sats, System, What, N, Sats, Time) :-
+        goal_time(System, What, N, maplist(sat, Sats), Time).
+bench_(taut, System, What, N, Sats, Time) :-
+        list_conj(Sats, Sat),
+        goal_time(System, What, N, taut(Sat, T), Time),
+        (   nonvar(T) ->
+            portray_clause(tautology(System, What, N, T))
+        ;   true
+        ).
+
+%?- list_goal([5,3], G).
+
+:- if(current_predicate(b_getval/2)).
+
+num_nodes :-
+        b_getval('$clpb_next_node', N0),
+        N #= N0 - 1,
+        format('num nodes: ~w\n', [N]).
+
+:- else.
+num_nodes.
+:- endif.
+
+goal_time(System, What, N, Goal, Time) :-
+        statistics(runtime, [T0,_]),
+        (   catch(Goal, error(resource_error(memory), _), E = memory) ->
+            true
+        ;   functor(Goal, F, A),
+            portray_clause(failed(System, What, N, F/A))
+        ),
+        statistics(runtime, [T1,_]),
+        T #= T1 - T0,
+        (   nonvar(E) ->
+            Time = exception(E, T)
+        ;   Time = time(T)
+        ).
+
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   Generating tables from collected results.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+instances(INs) :-
+        setof(I-N, V^C^instance(I,N,V,C), INs).
+
+instance(I, N, V, C) :-
+        instance_attributes(swi, I, N, num_vars_clauses(V,C)).
+
+timing_(System, What, N, Goal, T) :-
+        (   timing(System, What, N, Goal, T) -> true
+        ;   T = na
+        ).
+
+time0_time(time(T0), T) :-
+        Seconds is T0 / 1000,
+        (   Seconds > 1000 ->
+            T1 is round(Seconds),
+            T = integer(T1)
+        ;   T = float(Seconds)
+        ).
+time0_time(exception(_,_), exception).
+time0_time(na, na).
+
+%?- instances(Is), maplist(writeln, Is).
+
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   LaTeX
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+latex_table :-
+        instances(Is),
+        maplist(latex_instance, Is).
+
+latex_instance(I-N) :-
+        instance(I, N, V, C),
+        format("\\texttt{~w~w} & ~w & ~w & ", [I,N,V,C]),
+        maplist(timing_(swi, I, N), [sat,sats,taut], SWIs),
+        maplist(timing_(sicstus, I, N), [sat,sats,taut], SICSs),
+        append(SWIs, SICSs, Times0),
+        maplist(time0_time, Times0, Times1),
+        times_separators(Times1, Cols),
+        maplist(latex_col, Cols),
+        format("\\\\\n").
+
+latex_col(sep)        :- format(" & ").
+latex_col(integer(T)) :- format("$~w$", [T]).
+latex_col(float(T))   :- format("$~2f$", [T]).
+latex_col(na)         :- format("NA").
+latex_col(exception)  :- format("--").
+
+times_separators([], []).
+times_separators([T], [T]).
+times_separators([T1,T2|Ts0], [T1,sep|Ts]) :-
+        times_separators([T2|Ts0], Ts).
+
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   ASCII table
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+ascii_table :-
+        format("~t~30|~tSWI~t~30+~tSICStus~t~30+\n"),
+        format("~t~30|~tsat~t~10+~tsats~t~10+~ttaut~t~10+~tsat~t~10+~tsats~t~10+~ttaut~t~10+\n"),
+        instances(Is),
+        maplist(ascii_instance, Is).
+
+ascii_instance(I-N) :-
+        instance(I, N, V, C),
+        maplist(timing_(swi, I, N), [sat,sats,taut], SWIs),
+        maplist(timing_(sicstus, I, N), [sat,sats,taut], SICSs),
+        append(SWIs, SICSs, Times0),
+        maplist(time0_time, Times0, Times1),
+        maplist(time_ascii, Times1, As),
+        phrase(times_format(Times1), Cols),
+        format("~w~w~15|~t~w~5+~t~w~5+", [I,N,V,C]),
+        append("~30|", Cols, Format),
+        format(Format, As),
+        nl.
+
+time_ascii(float(F), F).
+time_ascii(integer(I), I).
+time_ascii(exception, exception).
+time_ascii(na, na).
+
+times_format([]) --> [].
+times_format([T|Ts]) -->
+        time_format(T),
+        times_format(Ts).
+
+time_format(integer(_)) --> "~t~w~10+".
+time_format(float(_))   --> "~t~2f~10+".
+time_format(na)         --> "~tna~i~10+".
+time_format(exception)  --> "~t--~i~10+".

clpb/benchmarks/instances

@@ -0,0 +1,23 @@
+# These are the instances that are used for benchmarking. This is
+# valid BASH syntax, so it can simply be run if the function "bench"
+# is suitably defined.
+
+bench pigeon 8
+bench pigeon 9
+bench pigeon 10
+
+bench schur 13
+bench schur 14
+bench schur 15
+
+bench langford 6
+bench langford 7
+bench langford 8
+
+bench queens 6
+bench queens 7
+bench queens 8
+
+bench triominoes 5
+bench triominoes 6
+bench triominoes 7

clpb/benchmarks/langford.pl

@@ -0,0 +1,70 @@
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   Langford Sequence of order N: sequence of numbers 1,1,2,2,...,N,N
+   such that the two occurrences of all k in 1..N are k units apart.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+:- include(bench).
+
+langford(N, Sats) :-
+        langford(N, _, Sats, _).
+
+%?- satsn(5).
+
+%?- length(_, N), langford(N, Vs, Sats, Conj), portray_clause(N), time(sat(Conj)), false.
+%@ 0.
+%@ % 100 inferences, 0.000 CPU in 0.000 seconds (91% CPU, 1538462 Lips)
+%@ 1.
+%@ % 35 inferences, 0.000 CPU in 0.000 seconds (77% CPU, 2500000 Lips)
+%@ 2.
+%@ % 3,890 inferences, 0.001 CPU in 0.001 seconds (88% CPU, 4814356 Lips)
+%@ 3.
+%@ % 126,913 inferences, 0.017 CPU in 0.018 seconds (98% CPU, 7263378 Lips)
+%@ 4.
+%@ % 1,115,458 inferences, 0.163 CPU in 0.164 seconds (99% CPU, 6862245 Lips)
+%@ 5.
+%@ % 3,298,303 inferences, 0.477 CPU in 0.481 seconds (99% CPU, 6918743 Lips)
+%@ 6.
+%@ % 7,755,915 inferences, 1.035 CPU in 1.046 seconds (99% CPU, 7495296 Lips)
+%@ 7.
+%@ % 31,545,100 inferences, 4.288 CPU in 4.326 seconds (99% CPU, 7357065 Lips)
+%@ 8.
+%@ % 112,305,689 inferences, 17.373 CPU in 17.519 seconds (99% CPU, 6464445 Lips)
+%@ 9.
+
+langford(N, Vs, Sats, Conj) :-
+        Len #= 3*N,
+        length(Row, Len),
+        findall(Row, (between(1,N,K), phrase(row(N,K), Row)), Matrix0),
+        sort(Matrix0, Matrix),
+        transpose(Matrix, TMatrix),
+        phrase(sats(TMatrix, Vs), Sats),
+        list_conj(Sats, Conj).
+
+sats([], _) --> [].
+sats([Col|Cols], Vs0) -->
+        { phrase(column_selection(Col, Vs0), Vs) },
+        [card([1],Vs)],
+        sats(Cols, Vs0).
+
+column_selection([], []) --> [].
+column_selection([C|Cs], [V|Vs]) -->
+        (   { C =:= 1 } -> [V]
+        ;   []
+        ),
+        column_selection(Cs, Vs).
+
+row(N, K) -->
+        n_zeros(_), [1], n_zeros(K), [1], n_zeros(_), % langford sequence
+        { Prefix #= K - 1,                            % rest: represent K
+          Suffix #= N - K },
+        n_zeros(Prefix),
+        [1],
+        n_zeros(Suffix).
+
+n_zeros(0)  --> [].
+n_zeros(K0) --> [0], { K0 #> 0, K #= K0 - 1 }, n_zeros(K).
+
+%?- length(Ls, 10), phrase(row(4, 3), Ls).
+%@ Ls = [1, 0, 0, 0, 1, 0, 0, 0, 1, 0] ;
+%@ Ls = [0, 1, 0, 0, 0, 1, 0, 0, 1, 0] ;
+%@ false.

clpb/benchmarks/pigeon.pl

@@ -0,0 +1,23 @@
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   pigeon N: place N+1 pigeons into N holes, such that each hole
+   holds at most one pigeon.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+:- include(bench).
+
+pigeon(N, Sats) :-
+        N1 #= N + 1,
+        pigeon(N, N1, _, Sats).
+
+pigeon(I, J, Rows, Ls) :-
+        length(Rows, J),
+        maplist(length_list(I), Rows),
+        transpose(Rows, TRows),
+        phrase((all_card1(Rows),all_max1(TRows)), Ls).
+
+length_list(N, Ls) :- length(Ls, N).
+
+all_card1([]) --> [].
+all_card1([Ls|Lss]) --> [card([1],Ls)], all_card1(Lss).
+
+all_max1([]) --> [].
+all_max1([Ls|Lss]) --> [card([0,1],Ls)], all_max1(Lss).