Программирование в ограничениях

Санкт-Петербургский Государственный Политехнический Университет

Факультет Технической Кибернетики

Кафедра Компьютерных Систем и Программных Технологий

Курсовой проект по «Математической логике»

на тему

«Программирование в ограничениях»

Работу выполнил группы:

3081/4

Преподаватель:

Санкт-Петербург

2012

1.Постановка задачи.

Решить задачу Эйнштейна при помощи бинарных решающих диаграмм (библиотека BuDDy). Для этого необходимо:

1)  Выбрать систему из N объектов, которые обладают M свойствами, принимающими N различных значений;

2)  Придумать n1 ограничений типа 1, n2 ограничений типа 2, n3 ограничений типа 3 и n4 ограничений типа 4;

3)  Найти все возможные решения и придумать физическую интерпретацию задачи.

4)  Добавить, убрать или изменить некоторые ограничения так, чтобы задача имела единственное решение, если она имеет несколько решений или не имеет их совсем.

Для выполнения задания необходимо написать программу на языке C++ с использованием библиотеки BuDDy.

1) Вариант 1: N = 4, M = 4, n1 = 3, n2 = 2, n3 = 5, n4 = 5

2.Описание системы.

Для кодирования одного параметра системы требуются 2 булевы переменные. У нас параметров системы 4, следовательно, для описания всего пространства, необходимо 32 переменных.

Объекты – это автомобили. Они имеют 4 параметра по 4 значения каждый:

·  Марка автомобиля = (BMW, Jaguar, Bentley,  Honda);

·  Цвет = (Черный, Зеленый, Синий, Красный);

·  Страна сборки = (Германия, США, Англия, Япония);

·  Тип кузова = (Универсал, Седан, Хэтчбек, Лимузин)

·   

Заданы ограничения:

1.BMW стоит на первой позиции.

2.Автомобиль, собранный в США, стоит на второй позиции.

3.На четвертом месте стоит автомобиль с кузовом хэтчбек.

4.Автомобиль синего цвета собран в Англии.

5.BMW черного цвета.

6.BMW стоит слева от зеленого автомобиля.

7.Автомобиль, собранный в США, стоит слева от лимузина.

8. Автомобиль, собранный в Англии, стоит слева от Honda.

9. Автомобиль, собранный в Японии, стоит слева от автомобиля синего цвета.

10.Jaguar стоит справа от автомобиля, собранного в Германии.

11. Автомобиль, собранный в Германии, стоит рядом с зеленым автомобилем.

12.Зеленый автомобиль стоит рядом с Bentley.

13.Синий автомобиль стоит рядом с автомобилем, собранным в Японии.

14.Honda стоит рядом с лимузином.

15.Jaguar стоит рядом с седаном.

Листинг программы:

#pragma comment(lib, "bdd.lib")    // Использование библиотеки BuDDy

#include <fstream>

#include <string>

#include "bdd.h"

#define N_VAR 32  // число булевых переменных

#define N 4             // число объектов

#define M 4             // число свойств

#define LOG_N 2

using namespace std;

char        var[N_VAR];

ofstream    out;

void print(void);

void build(char* varset, unsigned n, unsigned I);

// функция, используемая для вывода решений

void fun(char* varset, int size);

int main(void) {

// инициализация

bdd_init(10000, 1000); // Вызов функции для задачи малой размерности

bdd_setvarnum(N_VAR);  // Число булевых переменных

// ->--- вводим функцию p(k, i, j) следующим образом ( pk[i][j] ):

// Каждый признак представляется булевой функцией

bdd p1[N][N], p2[N][N], p3[N][N], p4[N][N];

unsigned I = 0;

for (unsigned i = 0; i < N; i++) {

for (unsigned j = 0; j < N; j++) {

p1[i][j] = bddtrue;

for (unsigned k = 0; k < LOG_N; k++)

p1[i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + k) : bdd_nithvar(I + k) ;

p2[i][j] = bddtrue;

for (unsigned k = 0; k < LOG_N; k++)

p2[i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + LOG_N + k) : bdd_nithvar(I + LOG_N + k) ;

p3[i][j] = bddtrue;

for (unsigned k = 0; k < LOG_N; k++)

p3[i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + LOG_N*2 + k) : bdd_nithvar(I + LOG_N*2 + k) ;

p4[i][j] = bddtrue;

for (unsigned k = 0; k < LOG_N; k++)

p4[i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + LOG_N*3 + k) : bdd_nithvar(I + LOG_N*3 + k) ;

}

I += LOG_N*M;

}

// -<--/*    булева функция, определяющая решение, начальное значение функции - true        */

bdd task = bddtrue;

// ->--- ограничение по-умолчанию 6

// Параметры принимают значения только из заданных множеств.

for (unsigned i = 0; i < N; i++) {

bdd temp1 = bddfalse;

bdd temp2 = bddfalse;

bdd temp3 = bddfalse;

bdd temp4 = bddfalse;

for (unsigned j = 0; j < N; j++) {

temp1 |= p1[i][j];

temp2 |= p2[i][j];

temp3 |= p3[i][j];

temp4 |= p4[i][j];

}

task &= temp1 & temp2 & temp3 & temp4;

}

// -<--// ->--- ограничение типа 1

// Ограничение, устанавливающее свойству k1 конкретного объекта i1 значение j1