一万年太久
只争朝夕
----首题
算法的世界，是个优雅的世界。人常说，数学是思维的体操；数学之美，是智慧之美。算法与之有同功之妙。数学有丰实的血肉肌体，又有抽象的思维灵魂：
e.g.1 (1) 自然数：0，1，2，4，5……，n，n+1，……
自然数运算：+ 定义为 1=0+1，2=1+1，3=2+1，4=3+1，……
(2) 加法群：<A,+> （群相关定义暂略，后面用到是再简述）
而算法，不仅有数学的渊源；她更是计算机世界的核心之一，有着与计算机相关的生生气息：
e.g.2 求自然数前n项和
输入参数：n，若合法
(1) sum:=0;
(2) For i:=0 To n-1 Do
sum:=sum+i;
(3) End
输出结果：sum
算法是个以视效率为生命的人；她是精确与速度的复合体，常在矛盾中忍受煎熬，却又在时间与空间的脉搏里取得一点一点的进步：
……O(2^n),……,O(n^3),O(n^2),O(n*log(n)),O(log(n)),O(1)
算法是个美丽而骄傲的人；人人都青睐她，她却昂起高高的额头……虽然如此，无数的人仍然都受到女神的幸临。人人也都知道，这条道路，只有勤奋的人才可能受到女神的信赖……所以，我们总能看到，一代又一代深入算法世界的开拓者，与大师……
我很高兴，将和您共同走一程，来到她的领域……
毫无疑问，我是她的追随者；凭着胸中的激情，请允许我来做一次向导，咱们缓缓的，领略她的奇特魅力。或许，我的心底，常常会流漏出一丝的无奈，在算法的世界里，总是充斥着矛盾，充斥着不可理解，但仍然的，更多的火焰将会蓬勃而出，如果您终于也情不自禁了，请也与我一起燃烧……
为了使您可以和她更好的交流，我将每次在最后留下个有趣的算法题目，供您探讨。当然，作为向导，我不能不加入进来，分享我部分的经验；但更多的时候，我将把这末尾的题目，寄希望于您……
本帖的题目：
SAT问题：
逻辑变量，如x0，是只能取TRUE和FALSE的变量，而对于逻辑变量的运算，本题目中用到：
非运算（-）：-（TRUE）=FALSE，-（FALSE）=TRUE
析取运算（V）：（TRUE）V（TRUE）=TRUE，（FALSE）V（TRUE）=（TRUE）V（FALSE）=TRUE，（FALSE）V（FALSE）=FALSE
子句的定义为：逻辑变量（或其非）经过有限次析取运算而得到的串表达式，如：
C0 : -x0 V -x8 V x13 V x15 V -x18
C1 : -x1 V -x3 V x5 V -x6 V x7 V x10 V -x13
C2 : -x5 V x10 V x11 V -x12
问题：是否可以判定一个 子句的集合，能给出逻辑变量的一组值，使得该子句集的所有子句都取值为TRUE ？
