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 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 here. You can download the code tsat_example.m, along with the two subroutines generate_3sat.m and boollp_cvxccv.m.

Contents

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);

The LP relaxation initialization had 0 violations.
After 4 random initializations, a solution with 0 violations was found.

Published with MATLAB® 7.10