param m, integer;# number of clauses
param n, integer;# number of variables(2n is thenumber ofliterals)
set M:= 1..m;
set N:= 1..n;
# phi[i,j]= 1 i fx_j appears in clausei
# = -1 if bar{x}_j appears in clause i
# = 0 otherwise
param phi{M,N} integer, default 0;
param k >=0 integer; # number of clauses you aim to satisfy
var x{N} binary;
param y{M} binary, default 0;  # 1 means satisfied

data max2sat_m9_n3.dat;

param fstar integer,>= 0, default 0;
param xstar{N} binary, default 0;
param ii integer;
param jj integer;
param l integer,default 1;
param ll integer,default 1;
param satisf integer, default 0;
param changedv{M,N} binary, default 0; # tell us if we have already changed the value of this variable n in the clause m 
param flag binary, default 0; # exit condition to avoid checking all variable: when one variable is 1 then the clause is one
param termination binary, default 0;
param iter integer, default 0;
param maxiter integer, default 100;

let k:= m-1;

# start with a random generated assignments
for {i in 1..n} {
	if (Uniform01()<= 0.5 ) then {
		let x[i]:=0;
	} else{
		let x[i] :=1;
	}
}

repeat while (termination=0) {
	
	# check if the current assignment satisfies the clauses
	for {i in 1..m}{  # for alla clauses
		let y[i] :=0;
		let flag :=0;
		let jj := 1;
		repeat while (jj <= n and flag =0) {
			if (phi[i,jj]<> 0)then {
				if ((phi[i,jj]=1 and x[jj]= 1) or (phi[i,jj]=-1 and x[jj]= 0) ) then {
					let y[i] := 1;  # clause i is satisfied
					let flag := 1;  # exit condition to avoid checking all variable: when one variable is 1 then the clause is one
				}
			}
		let jj :=jj+1;
		}
	}
		
	# count the number of satisfied clauses
	let satisf := 0;
	for{i in 1..m}{
		if(y[i] = 1)then {
			let satisf:= satisf+ 1;
		}
	}
	if (satisf< k) then {
		# choose the unsatisfied clause to be changed
		let ii :=1;
		let flag :=0;
		repeat while(ii <= m and flag= 0) {
				if (y[ii]= 0) then{
					let l := ii;
					let flag := 1; #when i find un unsatisfied clause, I exit the loop 
				}
		let ii :=ii+1;
		}
		# here l is the unsatisfied clause to change, thus...
		# change the clause l
		let flag :=0;
		let jj :=1;
		# I look for a not previously changed variable
		repeat while(jj <= n and flag= 0) {
			if (phi[l,jj]<> 0 and changedv[l,jj]=0) then {
				let ll := jj;
				let flag := 1;
				let changedv[l,jj]:= 1; 
			}
			let jj :=jj+1;
		}

		# change the value of variable ll
		if(x[ll] =0) then {
			let x[ll]:=1;
		} else {
			let x[ll]:=0;
		}
	} else{
		print "problemsolved";
		let termination:= 1;
	}
	let iter := iter+1;
	if(iter> maxiter)then {
		print "iteration limit reached";
		let termination:= 1;
	}
} #endwhile


for {i in 1..n}{
	let xstar[i]:= x[i];
}
printf "iterations= %d\n",iter-1;
printf "satisfied clauses =%d\n", satisf;
display xstar;