%
% Test for the SAT solver by a Cross-Entropy (CE) 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-50-1_6-yes1-2','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 = 5;
database{numbase}
load(database{numbase});
n = size(A , 2);
option.N = 100000;
option.rho = 0.1;
option.alpha = 0.9;
option.d = 50;
option.T_max = 1000;
option.theta_min = 0.05;
option.theta_max = 0.99;
tic,out = ce_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.St) , out.St , 1:length(out.St) , repmat(size(A , 1) , 1 , length(out.St)) , 'r' , 'linewidth' , 2)
grid on
xlabel('Iterations')
title(sprintf('\n Satisfied clauses = %5.2f%% (%d/%d), #(X) = %d' , 100*(out.S_opt/size(A , 1)) , out.S_opt , size(A , 1) ,size(out.X , 2)) , 'fontsize' , 13)