import java.io.IOException;
import java.io.BufferedReader;
import java.io.FileReader;
import java.io.PrintStream;
import java.io.FileOutputStream;

class Formule {
    int nbClauses;
    int nbVars;
    int[][] formule;
    int[][] vars;

    Formule(Formule f) {
        this(f.nbClauses, f.nbVars);

        for (int i = 0; i < nbClauses; i++)
            for (int j = 0; j < nbVars+1; j++)
                setVar(i, j, f.formule[i][j]);
    }
    
    Formule(int nbClauses, int nbVars) {
        this.nbClauses = nbClauses;
        this.nbVars = nbVars;

        /* La derniere case de chaque ligne contient le nombre de
	 * tautologies trouvees dans la clause apres lecture de la
	 * formule. */
        formule = new int[nbClauses][nbVars + 1];

	/* vars[i][1] contient le nombre d'occurrences de la i-eme
	 * variable dans la formule et vars[i][0] designe le nombre
	 * d'occurrences de son complement (utile pour l'heuristique). */
	vars = new int[nbVars][2];
    }

    Formule(String fichier) throws IOException {
	BufferedReader in
	    = new BufferedReader(new FileReader(fichier));

	nbClauses = Integer.parseInt(in.readLine());
	nbVars = Integer.parseInt(in.readLine());
	formule = new int[nbClauses][nbVars + 1];
	vars = new int[nbVars][2];

	String ligne;

	int i = 0;
	while ((ligne = in.readLine()) != null) {
	    if (ligne.equals(""))
		continue;

	    String[] clause = ligne.split(" ");
	    for (int j = 0; j < clause.length; j++) {
		int var = Integer.parseInt(clause[j]);
		int b = var < 0 ? -1 : 1;
		var = b*var - 1;

		setVar(i, var, b);
	    }

	    i++;
	}

	in.close();
    }

    void setVar(int clause, int var, int b) {
	if (var == nbVars) {
	    formule[clause][var] = b;
	    return;
	}

	if (b != 0) {
	    int l = b < 0 ? 0 : 1;

	    /* Si la clause contient une tautologie. */
	    if (formule[clause][var] == -b) {
		formule[clause][nbVars]++;
		l = b < 0 ? 1 : 0;
		vars[var][l]--;
		b = 0;
	    } else {
		vars[var][l] = vars[var][l] + (formule[clause][var] == 0 ? 1 : 0);
	    }
	} else {
	    int l = formule[clause][var] < 0 ? 0 : 1;

	    vars[var][l] = vars[var][l] + (formule[clause][var] != 0 ? -1 : 0);
	}

	formule[clause][var] = b;
    }

    void rawPrint() {
	rawPrint(System.out);
    }

    void rawPrint(PrintStream out) {
	for (int i = 0; i < nbClauses; i++) {
	    for (int j = 0; j < nbVars; j++) {
		out.print(formule[i][j] + " ");
	    }
	    out.println();
	}
    }

    void print() {
	print(System.out);
    }

    void print(PrintStream out) {
	out.println(nbClauses);
	out.println(nbVars);
	out.println();

	for (int i = 0; i < nbClauses; i++) {
	    for (int j = 0; j < nbVars; j++) {
                if (formule[i][j] != 0) {
		    out.print((j+1)*formule[i][j] + " ");
                }
	    }
	    out.println();
	}
    }

    void save(String fichier) throws IOException {
	print(new PrintStream(new FileOutputStream(fichier)));
    }

    boolean estVide() {
	return nbClauses == 0;
    }

    boolean clauseVide() {
	for (int i = 0; i < nbClauses; i++)
	    if (clauseVide(i))
		return true;

	return false;
    }

    boolean clauseVide(int i) {
	for (int j = 0; j < nbVars; j++)
	    if (formule[i][j] != 0)
		return false;

	return true;
    }

    boolean contientTautologie() {
	for (int i = 0; i < nbClauses; i++)
	    if (contientTautologie(i))
		return true;

	return false;
    }

    boolean contientTautologie(int i) {
	return formule[i][nbVars] != 0;
    }

    boolean contientUnitaire() {
	for (int i = 0; i < nbClauses; i++)
	    if (contientUnitaire(i))
		return true;

	return false;
    }

    boolean contientUnitaire(int i) {
	boolean unitaire = false;

	for (int j = 0; j < nbVars; j++) {
	    if (unitaire)
		return false;

	    if (formule[i][j] != 0)
		unitaire = true;
	}

	return unitaire;
    }

    boolean comp(int i, int[] clause) {
	for (int j = 0; j < nbVars; j++)
	    if (formule[i][j] != clause[j])
		return false;

	return true;
    }

    boolean membre(int[] clause) {
	for (int i = 0; i < nbClauses; i++)
	    if (comp(i, clause))
		return true;

	return false;
    }

    Formule supprimerClause(int clause) {
        Formule f = new Formule(nbClauses-1, nbVars);

        for (int i = 0; i < clause; i++)
            for (int j = 0; j < nbVars+1; j++)
                f.setVar(i, j, formule[i][j]);

        for (int i = clause+1; i < nbClauses; i++)
            for (int j = 0; j < nbVars+1; j++)
                f.setVar(i-1, j, formule[i][j]);
        
        return f;
    }

    boolean verif(int[] a) {
        for (int i = 0; i < nbClauses; i++) {
            if (contientTautologie(i))
                continue;
            
            int j;
            for (j = 0; j < nbVars; j++) {
                if (a[j] == 0 && formule[i][j] < 0
                    || a[j] == 1 && formule[i][j] > 0)
                    break;
            }

            if (j == nbVars)
                return false;
        }

        return true;
    }

    Formule substitution(int var, int b) {
        Formule f = new Formule(this);

        int i = 0;
        while (i < f.nbClauses) {
            if ((b == 1 && f.formule[i][var] > 0)
                || (b == 0 && f.formule[i][var] < 0)) {
                f = f.supprimerClause(i);
                continue;
            } else {
                f.setVar(i, var, 0);
            }

            i++;
        }

        return f;
    }

    boolean DP(int[] a) {
        return DP(new Formule(this), a);
    }

    /* Avec heuristique. */
    boolean DP(Formule f, int[] a) {
        if (f.estVide())
            return true;

        if (f.clauseVide())
            return false;

        for (int i = 0; i < f.nbClauses; i++) {
            if (f.contientTautologie(i))
                return DP(f.supprimerClause(i), a);
        }

	/* Recherche en priorite une clause unitaire. */
	for (int i = 0; i < f.nbClauses; i++) {
	    int var = 0;
	    boolean unitaire = false;
	    
	    for (int j = 0; j < f.nbVars; j++) {
		if (unitaire) {
		    unitaire = false;
		    break;
		}
		
		if (f.formule[i][j] != 0) {
		    unitaire = true;
		    var = j;
		}
	    }

	    if (unitaire) {
		int b = f.formule[i][var] == 1 ? 1 : 0;
		
		if (DP(f.substitution(var, b), a)) {
		    a[var] = b;
		    return true;
		} else {
		    return false;
		}
	    }
	}

	int max = 0;
	int var = 0;
	for (int i = 0; i < f.nbVars; i++) {
	    if (max < f.vars[i][0] * f.vars[i][1]) {
		max = f.vars[i][0] * f.vars[i][1];
		var = i;
	    }
	}

	/* Si "max == 0", on n'a pas change la valeur de "var" qui
	 * peut alors designer une variable absente dans la
	 * formule. */
	if (max == 0) {
	    /* On choisit la premiere variable presente pour la
	     * substitution. */
	    for (int i = 0; i < f.nbClauses; i++) {
		for (int j = 0; j < f.nbVars; j++) {
		    if (f.formule[i][j] != 0) {
			var = j;
		    }
		}
	    }
	}


	int b = f.vars[var][0] < f.vars[var][1] ? 1 : 0;
	int nb = b == 0 ? 1 : 0;
	if (DP(f.substitution(var, b), a)) {
	    a[var] = b;
	    return true;
	} else if (DP(f.substitution(var, nb), a)) {
	    a[var] = nb;
	    return true;
	}

        return false;
    }

    boolean DP2(int[] a) {
        return DP2(new Formule(this), a);
    }

    /* Sans heuristique. */
    boolean DP2(Formule f, int[] a) {
        if (f.estVide())
            return true;

        if (f.clauseVide())
            return false;

        for (int i = 0; i < f.nbClauses; i++) {
            if (f.contientTautologie(i))
                return DP(f.supprimerClause(i), a);
        }

	for (int i = 0; i < f.nbClauses; i++) {
	    int var = 0;
	    boolean unitaire = false;
	    
	    for (int j = 0; j < f.nbVars; j++) {
		if (unitaire) {
		    unitaire = false;
		    break;
		}
		
		if (f.formule[i][j] != 0) {
		    unitaire = true;
		    var = j;
		}
	    }

	    if (unitaire) {
		int b = f.formule[i][var] == 1 ? 1 : 0;
		
		if (DP(f.substitution(var, b), a)) {
		    a[var] = b;
		    return true;
		} else {
		    return false;
		}
	    }
	}

        for (int i = 0; i < f.nbClauses; i++) {
            for (int j = 0; j < f.nbVars; j++) {
                if (f.formule[i][j] != 0) {
                    if (DP(f.substitution(j, 1), a)) {
                        a[j] = 1;
                        return true;
                    } else if (DP(f.substitution(j, 0), a)) {
                        a[j] = 0;
                        return true;
                    } else {
                        return false;
                    }
                }
            }
        }

        return false;
    }

    static Formule gen(int n, int m, double p) {
	Formule f = new Formule(n, m);

	for (int i = 0; i < n; i++) {
	    for (int j = 0; j < m; j++) {
		double x = Math.random();
		if (x < p/2) {
		    f.setVar(i, j, 1);
		} else if (x < p) {
		    f.setVar(i, j, -1);
		} else {
		    f.setVar(i, j, 0);
		}
	    }
	}

	return f;
    }
    
    public static void main(String[] args) throws IOException {
	/*
      	Formule f = gen(50, 50, 0.1);
	
	Formule f = new Formule("f.cnf");
	

	System.out.println("Format brut :");
	f.rawPrint();

        System.out.println();
        
        System.out.println("Formule :");
	f.print();
        
        System.out.println();

        int[] a = new int[f.nbVars];

	boolean sat = f.DP(a);

        System.out.println("Satisfiable ?");
        System.out.println(sat);

        if (sat) {
            System.out.println();
        
            System.out.println("Affectation satisfaisant la formule :");
            System.out.print("(");
            for (int i = 0; i < a.length; i++)
                System.out.print(a[i] + (i < a.length-1 ? ", " : ""));
            System.out.println(")");
        }
	*/

	/*
	for (double p = 0.1; p <= 1; p += 0.1) {
	    for (int i = 1; i <= 20; i++) {
		for (int j = 1; j <= 20; j++) {		    
		    int s = 0;
		    int ns = 0;

		    for (int k = 0; k < 100; k++) {
			Formule f = gen(i, j, p);
			int[] a = new int[f.nbVars];

			if (f.DP(a)) {
			    s++;
			} else {
			    ns++;
			}
		    }

		    System.out.println("(n, m, p) = (" + i + ", " + j + ", " + p + "): "
				       + "sat: " + s + ", non-sat: " + ns);
		}
	    }
	}
	*/

	//Formule f = gen(10, 10, 0.5);
	//f.save("f.cnf");
	Formule f = new Formule("f.cnf");

	/*
        System.out.println("Formule :");
	System.out.println("----------");
	f.print();
	System.out.println("----------");
        
        System.out.println();
	*/

        int[] a = new int[f.nbVars];

	boolean sat = f.DP(a);

        System.out.println("Satisfiable ?");
        System.out.println(sat);

        if (sat) {
            System.out.println();
        
            System.out.println("Affectation satisfaisant la formule :");
            System.out.print("(");
            for (int i = 0; i < a.length; i++)
                System.out.print(a[i] + (i < a.length-1 ? ", " : ""));
            System.out.println(")");
        }
    }
}