如何处理合取范式可满足性的问题

老师出了个题目，判断给出的合取范式是否为可满足的，他给了很多个文本文件，要求从文本文件读取数据，例如一个文本中的内容是4 41 -2 -3-1 -44-2 -3 4，也就是我要输出
4
4
1 -2 -3
-1 -4
4
-2 -3 4
第一个4代表合取范式中有4个变量
第二个4表示合取范式中有4个析取式
下面的四行代表着4个析取式，数字表示第几个变量，负号代表“非”。
1.我想知道如何把文件中的这一行存到数组中，能输出成下面的6行？
2.假设我已经把数据保存成上面6行的形式，应该如何确定四个变量的真值，如何判断该合取范式是可满足的?