davidkuna/graphsat

Graph problems solver

GraphSAT

Graph problems solver

Autor: David Kuna (KUN0036)

Řešené problémy:

1. Graph coloring
	- Jsou vytvořeny proměnné pro všechny kombinace vrcholů a barev
	- Formule se skládá z omezení pro vrcholy (musí platit právě jedna barva pro každý vrchol) a z omezení pro hrany (vrcholy spojené hranou nesmí být stejné barvy)
	- Výsledné ohodnocení je vypsáno ve větě sdělující číslo barvy náležící danému vrcholu.
	- Spuštění: java -jar GraphSAT.jar cesta/ke/zdroji.txt 1 k

2. Independet set
	- Jsou vytvořeny proměnné pro jednotlivé vrcholy (Vi) a pro kombinaci všech vrcholů a velikosti množiny k (Xi,j). Tato pomocná matice umožní sestavit formuli omezení přiřazující jednotlivým vrcholům přesnou pozici v hledané množině.
	- Formule se skádá z omezení pro hrany, sloupce matice (maximálně jedna 1 ve sloupci), řádky matice (právě jedna 1 na řádku)
	- Výsledek je zapsán jako množina indexů nezávislých vrcholů.
	- Spuštění: java -jar GraphSAT.jar cesta/ke/zdroji.txt 2 k

3. Hamilton circle
	- Jsou vytvořeny proměnné pro všechny kombinace vrcholů a jejich pozic. Tedy n^2 proměnných.
	- Formule obsahuje omezení pro samostatné vrcholy (každý vrchol zastupuje právě jednu pozici v HC), omezení pro všechny kombinace proměnných zajišťující, že každá pozice bude obsazena právě jednou a omezení pro všechny dvojice vrcholů, které nejsou spojeny hranou (nemůžou být na pozicích vedle sebe)
	- Výsledný kruh je znázorněn směrem průchodu přes jednotlivé vrcholy.
	- Spuštění: java -jar GraphSAT.jar cesta/ke/zdroji.txt 3

Externí zdroje: - Program využívá externí knihovnu Sat4j umístěnou v lib/org.sat4j.core-2.2.3.jar - http://www.sat4j.org/doc.php

Kompilace: Balík obsahuje projekt vývojového prostředí NetBeans v7.4