prolog & SAT Solver & n-clique problem

[Scheriff]

bunlar hakkında fikri olan varsa bi ses etsin lütfen bişeyler sorucam
yoksa uzun uzun yazmiim boşuna:)

ek:propositional logic kullanarak göstermem gerekiyor n-clique i

[riglous]

Anlat bakalim, elimizden geldigince... 2 sene once kullanmistim prolog.

[Scheriff]

şöyle ki
şimdi n-clique i propositional logicte gösterdim. clause'ların içinde or ve her clause arasında and olacak şekilde. ama constraint olarak bir şeyler yazmam gerekiyor. 2 vertex arasında edge olmalı dışında başka bir constraint yazamıyorum.
bunlar ne olabilir?

sat solver dediğimiz şey input olarak sadece şu dimacs formatında alıyor

	p cnf 2 3

	1 -2 0

	-1 2 0

	..

	

bu durumda mesela herhangi bir graph'ı 3-clique var mı diye kontrol ederken graph'a ait bilgileri nası giricem ben sat solver'a?

pek prolog sorusu olmadı bu gerçi. prolog'da sat solver yazmam gerekiyor ama o şimdilik rafta

[riglous]

Bunu biraz daha duzgun anlatman lazim, tam olarak anlayamadim cunku.

Anladigim kadariyla verilen bir graph'ta cozum var mi yok mu diye bakacaksin ve bunun nasil programda gosterilecegi hakkinda soruyorsun. Bu mudur? Yoksa o kismini cozdun de baska bir sey icin mi yardim ariyorsun (verilen graph'ta 3 baglantisi olan vertex var mi yok mu gibi)?