package cnf;

import java.io.FileReader;
import java.io.IOException;
import java.util.Iterator;

/**
 * Translates CNF's to 3SAT form.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class To3SAT {

    private To3SAT() {}
    
    public static CNF to3SAT(CNF cnf) {
        CNF sat3 = new CNF();
        int maxVar = cnf.numVariables();
        
        for (Iterator/*<Clause>*/ i = cnf.clauses().iterator(); i.hasNext();) {
            Clause clause = (Clause)i.next();
            int n = clause.numLiterals();
            
            switch(n) {
            
            case 3:
            	// {x1 x2 x3} => {x1 x2 x3}
                sat3.addClause(clause);
                break;
                
            case 2:
                // {x1 x2} => {x1 x2 v1} {x1 x2 -v1}
                int fresh = ++maxVar;
                addClausePlus(sat3, clause,  fresh);
                addClausePlus(sat3, clause, -fresh);
                break;
                
            case 1:
                // {x} => {x v1 v2} {x -v1 v2} {x v1 -v2} {x -v1 -v2}
                int fresh1 = ++maxVar;
                int fresh2 = ++maxVar;
                addClausePlus(sat3, clause,  fresh1,  fresh2);
                addClausePlus(sat3, clause, -fresh1,  fresh2);
                addClausePlus(sat3, clause,  fresh1, -fresh2);
                addClausePlus(sat3, clause, -fresh1, -fresh2);
                break;
                
            default:
                // {x1 ... xn}, n > 3 =>
                // {x1 x2 v1} {-v1, v2 x3} {-v2, v3, x4} ... {-vn-4 vn-3 xn-2} {-vn-3 xn-1 xn}
                Iterator/*<Literal>*/ j = clause.literals().iterator();
                
            	// add the first clause
            	Clause currClause = new Clause();		                
            	currClause.addLiteral((Literal)j.next()); 	
            	currClause.addLiteral((Literal)j.next());
            	currClause.addLiteral(Literal.getLiteral(++maxVar));
            	sat3.addClause(currClause);
            	
            	// add n-4 middle clauses
            	for (int k = 0; k < n-4; k++) {
            	    currClause = new Clause();
            	    currClause.addLiteral(Literal.getLiteral(-maxVar));
            	    currClause.addLiteral(Literal.getLiteral(++maxVar));
            	    currClause.addLiteral((Literal)j.next());
            	    sat3.addClause(currClause);
            	}
            	
            	// add the last clause
            	currClause = new Clause();
            	currClause.addLiteral(Literal.getLiteral(-maxVar));
            	currClause.addLiteral((Literal)j.next());
            	currClause.addLiteral((Literal)j.next());
            	sat3.addClause(currClause);
                break;
            }
        }
        
        assert maxVar == sat3.numVariables();
        return sat3;
    }
    
    private static void addClausePlus(CNF cnf, Clause clause, int lit) {
        Clause copy = new Clause(clause);
        copy.addLiteral(Literal.getLiteral(lit));
        cnf.addClause(copy);
    }
    
    private static void addClausePlus(CNF cnf, Clause clause, int lit1, int lit2) {
        Clause copy = new Clause(clause);
        copy.addLiteral(Literal.getLiteral(lit1));
        copy.addLiteral(Literal.getLiteral(lit2));
        cnf.addClause(copy);
    }

}