#!/usr/bin/env python3
# -*- coding: utf-8 -*-

import re, sys

def read_text_file (fname):
    with open(fname) as f:
        content = f.readlines()
    return [x.strip() for x in content]

def read_DIMACS (fname):
    content=read_text_file(fname)

    header=content[0].split(" ")

    assert header[0]=="p" and header[1]=="cnf"
    variables_total, clauses_total = int(header[2]), int(header[3])

    # term can be negative signed integer
    clauses=[]
    for c in content[1:]:
        if c.startswith ("c "):
            continue
        clause=[]
        for var_s in c.split(" "):
            if len(var_s)>0:
                var=int(var_s)
                if var!=0:
                    clause.append(var)
        if len(clause)>0:
            clauses.append(clause)

    return variables_total, clauses_total, clauses

variables_total, clauses_total, clauses = read_DIMACS(sys.argv[1])

s="x"*variables_total+";"+"x,"*clauses_total
print ("string="+s)
pat="^"
for var in range(variables_total):
    pat=pat+"(?P<a_"+str(var+1)+">x?)"
pat=pat+".*;"

def term_to_regex (term):
    if term<0:
        return "(?P=a_"+str(abs(term))+")x"
    else:
        return "(?P=a_"+str(term)+")"

for clause in clauses:
    pat=pat+"(?:"
    pat=pat+"|".join(list(map(term_to_regex, clause)))
    pat=pat+"),"

print ("pattern="+pat)
regex=re.compile(pat)
res=regex.match(s)
if res==None:
    print ("UNSAT")
    exit(0)
print ("SAT")
out=""
for var in range(variables_total):
    result=res[var+1]
    if result=="x":
        out=out+str(var+1)+" "
    else:
        out=out+str(-(var+1))+" "

print (out)