test_cemcmc_satA.m

%
%  Test  for the SAT solver by a Botev-Kroeze (BK) optimization algorithm
%  see http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html for database



clear, clc, close all hidden

database          = {'uf20-01' , 'uf20-010' , 'uf20-0100' , 'uf50-01' ,'uf75-01', 'aim-50-1_6-yes1-1','aim-100-1_6-yes1-1'  , 'aim-100-2_0-yes1-1','aim-200-2_0-yes1-3','g125_17' , '2bitcomp_5' , '2bitmax_6'  };

numbase           = 4;

database{numbase}


load(database{numbase}); 

n                 = size(A , 2);

option.N          = 2000;
option.rho        = 0.5;
option.b          = 10*n;
option.winjec     = 10;
option.nbinjec    = 0;
option.Kgamma     = 1/200;
option.Kb         = 2/10;
option.Krho       = 1/50;
option.rhomax     = 0.7;
option.KN         = 1*1/10;
option.T_max      = 10000;


tic,out           = cemcmc_satA(A , option);,toc

disp(sprintf('\n Pourcentage of Satisfied clauses = %5.2f%% (%d/%d), card(X) = %d' , 100*(out.S_opt/S_opt) , out.S_opt , S_opt , size(out.X , 2)))


figure(1)
plot(1:length(out.gammat) , out.gammat , 1:length(out.gammat) , repmat(size(A , 1) , 1 , length(out.gammat)) , 'r' , 'linewidth' , 2)
grid on
xlabel('Iterations')
title(sprintf('\n   Satisfied clauses = %5.2f%% (%d/%d), #(X) = %d' , 100*(out.S_opt/S_opt) , out.S_opt , S_opt , size(out.X , 2)) , 'fontsize' , 13)