#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include "dpll.h"

int num_vars_;
int num_clauses_;
int clause_length_;
static char *clause_values_;
int max_depth_;

int main(int argc, char *argv[])
{
	int i, j;
	char **clauses;
	char bracket;
	char *assignment, ret_value;

	scanf("%d", &num_vars_);
	scanf("%d", &num_clauses_);
	scanf("%d", &clause_length_);

	clauses = (char**)malloc(num_clauses_ * sizeof(char*));
	clause_values_ = (char*)malloc(num_clauses_ * sizeof(char));
	for (i = 0; i < num_clauses_; ++i)
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
	assignment = (char*)malloc(num_vars_ * sizeof(char));
	for (i = 0; i < num_vars_; ++i)
		assignment[i] = UNASSIGNED;

	for (i = 0; i < num_clauses_; ++i)
	{
		int var_index;
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
		for (j = 0; j < num_vars_; ++j)
			clauses[i][j] = UNASSIGNED;
		scanf("%c", &bracket);
		scanf("%c", &bracket);
		for (j = 0; j < clause_length_; ++j)
		{
			scanf("%d", &var_index);
			if (var_index > 0)
				clauses[i][var_index - 1] = TRUE;
			else
			{
				var_index *= -1;
				clauses[i][var_index - 1] = FALSE;
			}
		}
		scanf("%c", &bracket);
		scanf("%c", &bracket);
	}

	max_depth_ = 0;
	ret_value = dpll(clauses, assignment, 0);
	if (ret_value == TRUE)
	{
		for (i = 0; i < num_vars_; ++i)
		{
			if (assignment[i] == TRUE)
				printf(" %d", i + 1);
			else if (assignment[i] == FALSE)
				printf(" -%d", i + 1);
			else
				printf(" %d", i + 1);
		}
		printf("\n");
	}
	else
		printf("Unsatisfiable\n");
	//printf("%d\n", max_depth_);

	return 0;
}

char dpll(char **clauses, char *assignment, int depth)
{
	int i;
	int min_index, var_index;
	char ret_value;
	
	if (depth > max_depth_)
	{
		max_depth_ = depth;
	}

	if (check_if_all_clauses_true(clauses, assignment))
	{
//		fprintf(stderr, "All clauses are true!\n");
		return TRUE;
	}

	if (check_if_any_clause_false(clauses, assignment))
	{
//		fprintf(stderr, "Some clause is false!\n");
		return FALSE;
	}

	min_index = -1;
	while (1)
	{
		if ((var_index = find_pure_symbol(clauses, assignment, min_index)) != 0 )
		{
//			fprintf(stderr, "Picking pure symbol: %d\n", var_index);
			extend(assignment, var_index);
			ret_value = dpll(clauses, assignment, depth + 1);
			if (ret_value == TRUE)
				return TRUE;
			unassign(assignment, var_index);
			return FALSE;
			min_index = var_index > 0 ? var_index : -var_index;
//			continue;
		}
		break;
	}

	min_index = -1;
	while (1)
	{
		if ((var_index = find_unit_clause(clauses, assignment, min_index)) != 0)
		{
			extend(assignment, var_index);
			ret_value = dpll(clauses, assignment, depth + 1);
			if (ret_value == TRUE)
				return TRUE;
			unassign(assignment, var_index);
			return FALSE;
			min_index = var_index > 0 ? var_index : -var_index;
//			continue;
		}
		break;
	}

	var_index = pick_unassigned_symbol(clauses, assignment);
	extend(assignment, var_index);
	ret_value = dpll(clauses, assignment, depth + 1);
	if (ret_value == TRUE)
		return TRUE;
	unassign(assignment, var_index);

	var_index *= -1;
	extend(assignment, var_index);
	ret_value = dpll(clauses, assignment, depth + 1);
	if (ret_value == TRUE)
		return TRUE;
	unassign(assignment, var_index);
	return FALSE;
}

int num_satisfied(char **clauses, char *assignment)
{
	int i, j;
	int num_sat_clauses;

	num_sat_clauses = 0;
	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
				break;
		}
		if (j != num_vars_)
			++num_sat_clauses;
	}

	return num_sat_clauses;
}

int pick_unassigned_symbol(char **clauses, char *assignment)
{
	int k;
	int var_index;
	int num_sat_clauses;
	int max_sat_clauses = -1, var_index_with_max = -1;

	for (k = 0; k < num_vars_; ++k)
	{
		if (assignment[k] == UNASSIGNED)
		{
			return (k + 1);			// Comment out for optimized DPLL
			var_index = k + 1;
			extend(assignment, var_index);
			num_sat_clauses = num_satisfied(clauses, assignment);
			if (num_sat_clauses > max_sat_clauses)
			{
				max_sat_clauses = num_sat_clauses;
				var_index_with_max = var_index;
			}
			unassign(assignment, var_index);

			var_index *= -1;
			extend(assignment, var_index);
			num_sat_clauses = num_satisfied(clauses, assignment);
			if (num_sat_clauses > max_sat_clauses)
			{
				max_sat_clauses = num_sat_clauses;
				var_index_with_max = var_index;
			}
			unassign(assignment, var_index);
		}
	}

	return var_index_with_max;
}

int check_if_all_clauses_true(char **clauses, char *assignment)
{
	int i, j;

	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
				break;
		}
		if (j == num_vars_)
			return 0;
	}

	return 1;
}

int check_if_any_clause_false(char **clauses, char *assignment)
{
	int i, j;

	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && (((clauses[i][j] ^ assignment[j]) == 0) || (assignment[j] == UNASSIGNED)))
				break;
		}
		if (j == num_vars_)
		{
//			fprintf(stderr, "Clause %d is false!\n", i + 1);
			return 1;
		}
	}

	return 0;
}

int find_pure_symbol(char **clauses, char *assignment, int min_index)
{
	int i, j;
	char prev_value;

	for (i = 0; i < num_clauses_; ++i)
	{
		clause_values_[i] = FALSE;
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
			{
				clause_values_[i] = TRUE;
				break;
			}
		}
	}
	for (j = min_index + 1; j < num_vars_; ++j)
	{
		if (assignment[j] != UNASSIGNED)
			continue;
		prev_value = UNASSIGNED;
		for (i = 0; i < num_clauses_; ++i)
		{
			if (clause_values_[i] == FALSE && clauses[i][j] != 0)
			{
				if (prev_value == UNASSIGNED)
					prev_value = clauses[i][j];
				else if (clauses[i][j] != prev_value)
					break;
			}
		}
		if (i == num_clauses_)
		{
			if (prev_value == TRUE)
				return (j + 1);
			else if (prev_value == FALSE)
				return -(j + 1);
		}
	}

	return 0;
}

int find_unit_clause(char **clauses, char *assignment, int min_index)
{
	int i, j, index;
	char value;
	
	for (i = 0; i < num_clauses_; ++i)
	{
		value = FALSE;
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0)
			{
				if ((clauses[i][j] ^ assignment[j]) == 0)
					break;
				else if (assignment[j] == UNASSIGNED)
				{
					if (value == TRUE)
						break;
					else
					{
						index = (j + 1) * clauses[i][j];
						value = TRUE;
					}
				}
			}
		}
		if (j == num_vars_ && value == TRUE && index > min_index)
			return index;
	}

	return 0;
}