/* 3SAT instance generator G2(n,m)	*/
/* created by M.Motoki */

#include	<stdio.h>
#include	<stdlib.h>
#include	<sys/types.h>

void	gen_unique_instance(int, int);	/* generate 3CNF with at least 1 solution t*/
void	sat_alloc(int n, int m, int k);
void	write_sat(FILE *fp, int n, int m, int k);
void	shuffle_sat(int m, int k);

int	**v;	/* variable number in each clause */
int	**lit;	/* literal type in each clause */
int	*clause_size;	/* size of clause */
int	*t;	/* solution for formula generator */

int	main(int argc, char	*argv[])
{
	int	n;	/* # of variables */
	int	m;	/* # of clauses */
	int	i, h;	/* loop counter */
	time_t	ts;

	if(argc == 3)
	{
		n = atoi(argv[1]);
		m = atoi(argv[2]);
	}
	else
	{
		fprintf(stderr, "%s n m\n", argv[0]);
		exit(0);
	}
	
	ts = time(NULL);
	srand((int)ts);
	
	sat_alloc(n, m, 3);
	
	for(i = 0; i < n; i++)
	{
		t[i] = rand() % 2;
	}
	
	gen_unique_instance(n, m-n);
	for(i = m-n; i < m; i++)
	{
		clause_size[i] = 3;
		do
		{
			for(h = 0; h < 3; h++)
			{
				v[i][h] = rand() % n;
				lit[i][h] = !t[v[i][h]];
			}
			h = rand() % 3;
			v[i][h] = i - m + n;
			lit[i][h] = t[i - m + n];
		}while((v[i][0] == v[i][1]) || (v[i][1] == v[i][2]) || (v[i][2] == v[i][0]));
	}
	shuffle_sat(m, 3);
	
	fprintf(stdout, "# instance by G2\n# solution = ");
	for(i = 0; i < n; i ++)
		fprintf(stdout, "%d%", t[i]);
	fprintf(stdout, "\n");
	write_sat(stdout, n, m, 3);
	
	return;
}

/* memory allocation to matrixes s.t. n variables m clauses with at most size k */
void	sat_alloc(int n, int m, int k)
{
	int i;
	
	v = malloc(m * k * sizeof(int));
	if(v == NULL)
	{
		fprintf(stderr,"not enough memory\n");
		exit(1);
	}
	for(i = 0; i < m; i++)
	{
		v[i] = malloc(k * sizeof(int));
		if(v[i] == NULL)
		{
			fprintf(stderr,"not enough memory\n");
			exit(1);  
		}
	}

	lit = malloc(m * k * sizeof(int));
	if(lit == NULL)
	{
		fprintf(stderr,"not enough memory\n");
		exit(1);
	}
	for(i = 0; i < m; i++)
	{
		lit[i] = malloc(k * sizeof(int));
		if(lit[i] == NULL)
		{
			fprintf(stderr,"not enough memory\n");
			exit(1);  
		}
	}
	
	clause_size = malloc(m * sizeof(int));
	if(clause_size == NULL)
	{
		fprintf(stderr,"not enough memory\n");
		exit(1);
	}
	
	
	t = malloc(n * sizeof(int));
	if(t == NULL)
	{
		fprintf(stderr,"not enough memory\n");
		exit(1);
	}
	
	return;
}

/* generate 3CNF with at least 1 solution (1^n) */
void	gen_unique_instance(int n, int m)
{
	int	i, h;	/* loop counter */
	int	dup;	/* flag for repetation of variables */
	
	for(i = 0; i < m; i++)
	{
		clause_size[i] = 3;
		do
		{
			for(h = 0; h < 3; h++)
			{
				v[i][h] = rand() % n;
				lit[i][h] = rand() % 2;
			}
		}while((v[i][0] == v[i][1]) || (v[i][1] == v[i][2]) || (v[i][2] == v[i][0]) || (lit[i][0] != t[v[i][0]] && lit[i][1] != t[v[i][1]] && lit[i][2] != t[v[i][2]]) );
	}
	return;
}

void	write_sat(FILE *fp, int n, int m, int k)
{
	int	i, j, h; /* loop counter */
	
	fprintf(fp, "%d %d %d\n", n, m, k);
	for(j = 0; j < m; j++)
	{
		for(h = 0; h < clause_size[j]; h++)
		{
			if(!lit[j][h])
				fprintf(fp, "-");
			fprintf(fp, "%d ", v[j][h]+1);
		}
		fprintf(fp, "\n");
	}
	return;
}

void	shuffle_sat(int m, int k)
{
	int	tmp_clause_size;
	int	tmp_v;
	int	tmp_lit;
	int	tmp;
	int	j, h;
	
	for(j = m-1; j > 0; j--)
	{
		tmp = rand() % (j+1);
		tmp_clause_size = clause_size[j];
		clause_size[j] = clause_size[tmp];
		clause_size[tmp] = tmp_clause_size;
		for(h = 0; h < k; h++)
		{
			tmp_v = v[j][h];
			tmp_lit = lit[j][h];
			v[j][h] = v[tmp][h];
			lit[j][h] = lit[tmp][h];
			v[tmp][h] = tmp_v;
			lit[tmp][h] = tmp_lit;
		}
	}
	return;
}