Links und Funktionen
Sprachumschaltung

Navigationspfad
You are here: Home / Teaching / Winter 2015/16 / SAT Solving / Solutions / Practical 1


Inhaltsbereich

Practical 1

Plain Text icon u01p01.txt — Plain Text, 2 KB (3052 bytes)

File contents

/*
  Practical Exercise 1:

  The goal of the puzzle ``Unruly'' (by Adolfo Zanellati) is to paint
  a $n \times n$ matrix in black and white color, such that the following
  conditions are satisfied:
  (1) No row or column may contain three consecutive squares of the same color.
  (2) Each row and column must contain the same number of black and white fields.
  
  In below puzzles, the gray fields are to be determined.
  Write a program to generate a DIMACS CNF file corresponding
  to the Unruly puzzle, and then solve it using PicoSAT.
*/

#include <stdint.h>
#include <stdio.h>

#define B +1
#define W -1
#define _  0

#ifdef PROBLEM1

#define SIZE 8
int problem[SIZE][SIZE] = {
	{_,_,_,_,B,B,_,_},
	{_,W,W,_,_,_,_,_},
	{_,_,_,_,_,B,_,_},
	{W,_,B,_,_,_,_,_},
	{_,_,_,W,_,_,_,_},
	{_,W,_,W,_,B,_,W},
	{B,_,B,_,_,B,_,_},
	{_,_,_,_,_,_,_,_},
};

#else

#define SIZE 14
int problem[SIZE][SIZE] = {
	{_,B,_,W,B,_,W,_,_,B,_,_,_,_},
	{W,_,_,W,_,_,_,_,_,B,_,_,_,W},
	{_,W,_,_,B,_,_,_,_,_,_,_,_,_},
	{_,_,_,W,W,_,_,_,W,_,_,_,_,_},
	{B,_,_,_,_,_,W,_,_,B,_,_,_,W},
	{_,W,_,B,_,_,_,_,_,_,_,_,_,W},
	{B,_,_,_,_,B,_,_,_,_,_,B,_,_},
	{_,_,_,_,_,_,_,_,B,B,_,_,_,_},
	{_,_,_,_,_,W,_,_,_,_,W,_,_,_},
	{_,B,_,_,_,W,_,_,_,_,_,_,_,_},
	{_,_,B,_,_,_,_,_,W,_,W,_,_,_},
	{_,_,_,_,_,B,_,_,_,B,_,_,W,_},
	{_,_,_,_,_,_,B,_,_,_,_,_,_,_},
	{_,B,B,_,W,_,_,_,_,_,_,_,_,B},
};

#endif

/* bijection: [0..SIZE-1] * [0..SIZE-1] -> [1..SIZE*SIZE] */
int
field(int x, int y)
{
	return SIZE*x + y + 1;
}

uint32_t
bit_count (uint32_t i) {
	/* educational version, use __builtin_popcount for real code.  */
	int c;
	for (c = 0; i > 0; i >>= 1)
		if (i & 1)
			c++;
	return c;
}

int
main() {
	printf("p cnf 1 1\n");

	/* print given configuration. */
	for (int i = 0; i < SIZE; i++)
		for (int j = 0; j < SIZE; j++)
			if (problem[i][j])
				printf("%d 0\n", problem[i][j] * field(i,j));
	
	/* linewise constraints: */
	for (int i = 0; i < SIZE; i++) {
		/* no three equal */
		for (int j = 0; j < SIZE-2; j++) {
			printf("%d %d %d 0\n",
			    -field(i,j), -field(i,j+1), -field(i,j+2));
			printf("%d %d %d 0\n",
			    field(i,j),  field(i,j+1),  field(i,j+2));
		}
		/* same number of black/white */
		for (int n = 0; n < (1<<SIZE); n++) {
			if (bit_count(n) != SIZE/2) {
				for (int l = 0, m = n; l < SIZE; l++, m >>= 1)
					printf("%d ",
					    ((m&1) ? -1 : +1) * field(i, l));
				printf("0\n");
			}
		}
	}

	/* columnwise constraints: */
	for (int j = 0; j < SIZE; j++) {
		/* no three equal */
		for (int i = 0; i < SIZE-2; i++) {
			printf("%d %d %d 0\n",
			    -field(i,j), -field(i+1,j), -field(i+2,j));
			printf("%d %d %d 0\n",
			    field(i,j),  field(i+1,j),  field(i+2,j));
		}
		/* same number of black/white */
		for (int n = 0; n < (1<<SIZE); n++) {
			if (bit_count(n) != SIZE/2) {
				for (int l = 0, m = n; l < SIZE; l++, m >>= 1)
					printf("%d ",
					    ((m&1) ? -1 : +1) * field(l, j));
				printf("0\n");
			}
		}
	}
}

Document Actions


Funktionsleiste