b,i,j,k,s,n,a[99][99];main(c,v){for(;!scanf("p cnf%d%*d",&v);)gets(a);for(;scanf("%d",&j)>0;k=!j?!++b:k)a[b][k++]=j;for(c=b;i<1<<v&&(s=s<c);++i)for(s=j=0;j<c;b&&++s,++j)for(b=k=0;(n=a[j][k++])&&!b;)b=i&1<<v-abs(n)?n<0:n>0;printf("s %sSATISFIABLE%s",s?"UN":"",s?"":"\nv");for(--i,k=0;!s&&k<v;)printf(" %d",i&1<<v-++k?-k:k);}
Note that non-ascii characters in the above source code will be escaped (such as \x9f).