import java.util.*;
import techniques.PL.*;

public class GuessSAT {
  private Conjunction cnf;
  private Interpretation interp;

  public GuessSAT(int numClauses) {
    // Generate random 3-SAT instance with specified number of clauses
    String sentence = CNF.randInstance(numClauses);

    // Parse sentence
    cnf = CNF.parse(sentence);

    // Print out parsed CNF sentence
    System.out.println(cnf.toString());

    // Extract all variables
    Set vars = cnf.getVariables();

    // Generate random interpretation
    interp = new Interpretation();
    Iterator i = vars.iterator();
    while (i.hasNext())
      if (CNF.coinFlip())
        interp.put(i.next(), Boolean.TRUE);
      else
        interp.put(i.next(), Boolean.FALSE);

    // Print out interpretation
    System.out.println(interp.toString());

    // Is our sentence satisfied under our interpretation?
    if (cnf.isSatisfied(interp) == Boolean.TRUE)
      System.out.println("Bingo!");
    else
      System.out.println("Doh!  Try again.");
  }
}