%%  Three Satisfiability Example
% This example uses the convex-concave procedure to solve the 3-
% Satisfiability problem. That is, find a Boolean assignment such that a set
% of expressions consisting of three disjunctions and possibly negations
% evaluate to true.  Details can be found in section 5.1 of 
% <http://www.stanford.edu/~boyd/papers/cvx_ccv Variations and Extension of
% the Convex-Concave Procedure>.
%
% This code allows for initialization with an LP relaxation, as well as
% repeted random initialization.
%
% This example uses CVX, which is available <http://www.cvxr.com/cvx/ here>.
% You can download the code <tsat_example.m>, along with the two
% subroutines <generate_3sat.m> and <boollp_cvxccv.m>.

%%
close all force
clear all

%% Problem generation parameters
rand('state',0);
n = 40; % number of variables
m = 150; % number of expressions
trials = 5; % number of initializations to use at each size
[A b] = generate_3sat(m,n);


%% Algorithm Parameters
iterations = 100;% maximum number of iterations to be run, this number will almost never be hit1
tol = 1e-3;% tolerance to use as a stopping criteria
lp_relax = 1; %attempt to solve initializing from the LP relaxation 

%% Solve 3-SAT using an LP relaxation initialization
if(lp_relax)
    %solve the lp relaxation for initialization
    cvx_begin quiet
    variable x_0(n)
    minimize sum(abs(x_0-.5))
    subject to
    0 <= x_0;
    x_0 <= 1;
    A*x_0 <= b;
    cvx_end
    [x_lp_relax violation_lp] = boollp_cvxccv(x_0,A,b,tol,iterations);
end
            
%% Solve 3-SAT using a random initialization
violation = inf;
trial = 0;
while(trial < trials && violation ~=0)
    x_0 = rand(n,1);%generate an initial random starting configuration
    [x_new violation_new] = boollp_cvxccv(x_0,A,b,tol,iterations);
    if(violation_new < violation)
        violation = violation_new;
        x = x_new;
    end
    trial = trial+1;
end

fprintf('The LP relaxation initialization had %d violations.\n',violation_lp);
fprintf('After %d random initializations, a solution with %d violations was found.\n',trial, violation);