package satk;

import java.util.*;
import java.text.*;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.lang.*;

public class sat extends Applet
  implements ItemListener,ActionListener{

public class Clauses{
  int n;
  char[][] c;
public Clauses(int num){
  n=num;
  c=new char[n][3];}
}


boolean x;

Panel Apan=new Panel();
Panel Xpan=new Panel();
Panel Lpan=new Panel();
Panel Span=new Panel();
Thread timer = null;
CheckboxGroup gentyp = new CheckboxGroup();
Checkbox rndcb=new Checkbox("Random",gentyp,true);
Checkbox solcb=new Checkbox("soluble",gentyp,false);
Button but1=new Button("Solve");
Button but2=new Button("Generate");
Checkbox alph[]=new Checkbox[26];
Label lab[]=new Label[100];
Label lab1=new Label(" ");
Clauses cl=new Clauses(100);
Random R=new Random();
int ct,depth;
int dn=0;
boolean gs=false;
boolean[] solution=new boolean[26];

public sat() {}

double sqr(double x){return x*x;}
double strToD(String s){return Double.valueOf(s).doubleValue();}

public Clauses reduce(Clauses cl,char l){
int ct,i,j;boolean flg;char x;
Clauses clr=new Clauses(cl.n);
char nl=(char)(l^32);clr.n=0;
alph[l%32-1].setState(l<95);
for (i=0;i<cl.n;i++){
  for (j=0;j<3;j++){
    x=cl.c[i][j];
    if (nl==x)x='.';
    else if (l==x) {clr.n--;break;}
    clr.c[clr.n][j]=x;}
  clr.n++;}
return clr;
}

public boolean solve(Clauses cl){
int i,j,t,s,k,m;char x;
char[] l=new char[3];
int[] score=new int[26];
ct++;
for (i=0;i<26;i++)score[i]=0;
setColours();
try {Thread.sleep(100);} catch (InterruptedException e){}
lab1.setText(Integer.toString(ct));
if (cl.n==0) return true;
for (i=0;i<cl.n;i++){
  t=0;s=10;
  for (j=0;j<3;j++){
    x=cl.c[i][j];
    if (x!='.')l[t++]=x;}
  switch (t){
  case 0: return false;
  case 1: return solve(reduce(cl,l[0]));
  case 3: {score[(l[2]%32)-1]++;s=1;}//wot no break?
  case 2: {score[(l[0]%32)-1]+=s;score[(l[1]%32)-1]+=s;}}}
s=0;x=l[0];
for (i=0;i<26;i++) if (score[i]>s){s=score[i];x=(char)(i+'A');}
if (solve(reduce(cl,x))) return true;
else return solve(reduce(cl,(char)(x+32)));
}

public void dlets(char[] l){
int j;
do
for (j=0;j<3;j++) l[j]=(char)('A'+(Math.abs(R.nextInt())%26));
while ((l[0]==l[1])|(l[0]==l[2])|(l[1]==l[2]));
}

public void generate(Clauses cl){
int i,j,c1,c2,d,off;
char x;boolean ok;
char [] l=new char[3];
for (i=0;i<26;i++){
  solution[i]=(R.nextInt()%2==0);
  alph[i].setState(false);}
for (i=0;i<100-26*dn;i++){
  do{
    ok=false;
    dlets(l);
    for (j=0;j<3;j++) {
      if (R.nextInt()%2==0)l[j]=(char)(l[j]+32);
      if (l[j]<95==solution[l[j]%32-1]) ok=true;}
  }while (gs&!ok);
  for (j=0;j<3;j++) cl.c[i][j]=l[j];}
for (d=0;d<dn;d++){
  off=100-26*(d+1);
  for (i=0;i<26;i++){
    dlets(l);
    for (j=0;j<3;j++) if (solution[l[j]%32-1]) l[j]=(char)(l[j]+32);
    x=(char)('A'+i);
    if (!solution[i]) x=(char)(x+32);
    l[Math.abs(R.nextInt())%3]=x;
    for (j=0;j<3;j++) cl.c[off+i][j]=l[j];}}
for (i=0;i<250;i++){  //jumble
  c1=Math.abs(R.nextInt())%100;
  c2=Math.abs(R.nextInt())%100;
  for (j=0;j<3;j++) {
    l[j]=cl.c[c1][j];cl.c[c1][j]=cl.c[c2][j];cl.c[c2][j]=l[j];}}
for (i=0;i<100;i++) lab[i].setText(new String(cl.c[i]));
setColours();
lab1.setText("                             ");
}

public void init() {
Font f=new Font("Courier",Font.PLAIN,14);
int i;
setLayout(null);
Xpan.setBounds(10,0,580,30);
Apan.setBounds(10,50,580,50);
Lpan.setBounds(10,120,580,300);
Span.setBounds(10,435,580,30);
setBackground(new Color(255,255,220));
add(Xpan);add(Apan);add(Lpan);add(Span);
Apan.setLayout(new GridLayout(2,13,5,5));
for (i=0;i<26;i++){
  alph[i]=new Checkbox(String.valueOf((char)('A'+i)),null,false);
  Apan.add(alph[i]);
  alph[i].addItemListener(this);}
Lpan.setLayout(new GridLayout(10,10,5,5));
for (i=0;i<100;i++){
  lab[i]=new Label("",Label.CENTER);
  Lpan.add(lab[i]);
  lab[i].setFont(f);}
generate(cl);
Span.add(but1);but1.addActionListener(this);
Xpan.add(but2);but2.addActionListener(this);
Xpan.add(rndcb);Xpan.add(solcb);
Span.add(lab1);
}

void setColours(){
boolean valid;char c; int i,j;
for (i=0;i<100;i++){
  valid=false;
  for (j=0;j<3;j++){
    c=cl.c[i][j];
    if ((c<'a')==(alph[c%32-1].getState())) valid=true;}
  lab[i].setBackground(valid?Color.cyan:Color.red);}}

String threadInfo(){
int act=Thread.activeCount();
String result=Integer.toString(act)+"\n";
Thread[] tarr=new Thread[act];
Thread.enumerate(tarr);
for (int i=0;i<act;i++) result=result+tarr[i].toString()+"\n";
return result;
}

public void itemStateChanged(ItemEvent e){
setColours();
}

public void actionPerformed(ActionEvent e){
String act=e.getActionCommand();
if (act.equals("Solve")){
  ct=0;lab1.setText(solve(cl)?"Solved "+Integer.toString(ct)+" Steps":"Insoluble");
  setColours();}
else if (act.equals("Generate")){
  if (rndcb.getState()){dn=0;gs=false;}else {dn=1;gs=true;}
  generate(cl);}
}
public String getAppletInfo() {return "SAT program";}

public String[][] getParameterInfo() {return null;}

}