// this is D.Knuth's sat0w.c from sat0w.w reworked by me

#define show_basics 1
#define show_choices 2
#define show_details 4

#define vars_per_vchunk 341
#define cells_per_chunk 511

#define hack_in(q,t) (struct tmp_var*) (t|(size_t) q)
#define hack_out(q) (((size_t) q) & 0x3) 
#define hack_clean(q) ((struct tmp_var*) ((size_t) q & -4) )

#include <assert.h> 
#include <stdio.h> 
#include <stdint.h> 
#include <stdlib.h> 
#include <string.h> 

struct tmp_var
{
	uint64_t name;
	uint32_t serial;
	int stamp;
	struct tmp_var* next;
};

struct vchunk
{
	struct vchunk* prev;
	struct tmp_var var[vars_per_vchunk];
};

struct chunk
{
	struct chunk* prev;
	struct tmp_var* cell[cells_per_chunk];
};

typedef struct
{
	uint32_t litno;
} cell;

typedef struct
{
	uint32_t start;
	uint32_t wlink;
} clause;

typedef struct
{
	uint64_t name;
} variable;

int random_seed=0;
int verbose=show_basics;
int show_choices_max=1000000;
int hbits=8;
int buf_size=1024;
uint64_t bytes;
uint64_t nodes;
uint64_t thresh=0;
uint64_t delta=0;
uint64_t timeout=0x1fffffffffffffff;

char* buf;
struct tmp_var** hash;
uint32_t hash_bits[93][8];
struct vchunk* cur_vchunk;
struct tmp_var* cur_tmp_var;
struct tmp_var* bad_tmp_var;
struct chunk* cur_chunk;
struct tmp_var** cur_cell;
struct tmp_var** bad_cell;
uint64_t vars;
uint64_t clauses;
uint64_t nullclauses;
uint64_t cells;

cell* mem;
clause* cmem;
uint32_t nonspec;
variable* vmem;
char* move;

void print_clause(uint32_t c)
{
	uint32_t k,l;
	printf("%d:",c);
	for(k=cmem[c].start; k<cmem[c-1].start; k++)
	{
		l=mem[k].litno;
		printf(" %s%.8s", l&1?"~":"", (char*)&vmem[l>>1].name);
	}
	printf("\n");
}

void print_clauses_watching(int l)
{
	uint32_t p;
	for(p= cmem[l].wlink;p;p= cmem[p].wlink)
		print_clause(p);
}

void print_state(int l)
{
	int k;
	fprintf(stderr,"move: ");
	for(k=1; k<=l; k++)
		fprintf(stderr,"%c",move[k]+'0');
	fprintf(stderr,"\n");
	fflush(stderr);
}

int main(int argc, char*argv[])
{
	uint32_t c,h,i,j,k,l,p,q,level,parity;

	for(j=argc-1,k=0; j; j--)
		switch(argv[j][0])
		{
			case'v': k|=(sscanf(argv[j]+1,"%d",&verbose)-1); break;
			case'c': k|=(sscanf(argv[j]+1,"%d",&show_choices_max)-1); break;
			case'h': k|=(sscanf(argv[j]+1,"%d",&hbits)-1); break;
			case'b': k|=(sscanf(argv[j]+1,"%d",&buf_size)-1); break;
			case's': k|=(sscanf(argv[j]+1,"%d",&random_seed)-1); break;
			case'd': k|=(sscanf(argv[j]+1,"%lld",&delta)-1);thresh=delta; break;
			case'T': k|=(sscanf(argv[j]+1,"%lld",&timeout)-1); break;
			default: k=1;
		}
	if(k || hbits<0 || hbits> 30 || buf_size<=0)
	{
		fprintf(stderr, "Usage: %s [v<n>] [c<n>] [h<n>] [b<n>] [s<n>] [d<n>] [T<n>] < foo.sat\n",argv[0]);
		exit(-1);
	}

	srand(random_seed);
	buf= (char*)malloc(buf_size*sizeof(char));
	assert(buf);
	hash= (struct tmp_var**)malloc(sizeof(struct tmp_var) << hbits);
	assert(hash);
	for(h=0; h<1<<hbits; h++)
		hash[h]=NULL;

	for(j=92; j; j--)
		for(k= 0;k<8;k++)
			hash_bits[j][k]=rand();

	while(1)
	{
		if(!fgets(buf,buf_size,stdin))
			break;
		clauses++;
		if(buf[strlen(buf)-1]!='\n')
		{
			fprintf(stderr,
					"The clause on line %lld (%.20s...) is too long for me;\n",clauses,buf);
			fprintf(stderr," my buf_size is only %d!\n",buf_size);
			fprintf(stderr,"Please use the command-line option b<newsize>.\n");
			exit(-4);
		}

		for(j=k=0;;)
		{
			while(buf[j]==' ')
				j++;
			if(buf[j]=='\n')
				break;
			if(buf[j]<' ' || buf[j]>'~')
			{
				fprintf(stderr,"Illegal character (code #%x) in the clause on line %lld!\n", buf[j],clauses);
				exit(-5);
			}
			if(buf[j]=='~')
			{
				i=1;
				j++;
			}
			else
				i= 0;

			struct tmp_var* p;
			if(cur_tmp_var==bad_tmp_var)
			{
				struct vchunk* new_vchunk;
				new_vchunk=(struct vchunk*)malloc(sizeof(struct vchunk));
				assert(new_vchunk);
				new_vchunk->prev=cur_vchunk;
				cur_vchunk=new_vchunk;
				cur_tmp_var=&new_vchunk->var[0];
				bad_tmp_var=&new_vchunk->var[vars_per_vchunk];
			}

			cur_tmp_var->name=0;
			for(h=l=0; buf[j+l] > ' ' && buf[j+l] <= '~'; l++)
			{
				if(l > 7)
				{
					fprintf(stderr, "Variable name %.9s... in the clause on line %lld is too long!\n",
							buf+j, clauses);
					exit(-8);
				}
				h^=hash_bits[buf[j+l]-'!'][l];
				*((char*)&cur_tmp_var->name+l)=buf[j+l];
			}
			if(l==0)
				goto empty_clause;
			j=j+l;
			h= h & (1<<hbits)-1;

			for(p=hash[h]; p; p=p->next)
				if(p->name == cur_tmp_var->name)
					break;
			if(p==NULL)
			{
				p=cur_tmp_var++;
				p->next=hash[h];
				hash[h]=p;
				p->serial=vars++;
				p->stamp=0;
			}

			if(p->stamp==clauses || p->stamp==-clauses)
			{
				if((p->stamp>0) == (i>0))
					goto empty_clause;
			}
			else
			{
				p->stamp=(i ? -clauses : clauses);
				if(cur_cell==bad_cell)
				{
					struct chunk* new_chunk;
					new_chunk= (struct chunk*)malloc(sizeof(struct chunk));
					assert(new_chunk);
					new_chunk->prev=cur_chunk;
					cur_chunk=new_chunk;
					cur_cell=&new_chunk->cell[0];
					bad_cell=&new_chunk->cell[cells_per_chunk];
				}

				*cur_cell=p;
				if(i==1)
					*cur_cell=hack_in(*cur_cell,1);
				if(k==0)
					*cur_cell=hack_in(*cur_cell,2);
				cur_cell++;
				k++;
			}
		}
		if(k==0)
		{
			fprintf(stderr,"(Empty line %lld is being ignored)\n",clauses);
			nullclauses++;
		}
		goto clause_done;
empty_clause:

		while(k)
		{
			if(cur_cell > &cur_chunk->cell[0])
				cur_cell--;
			else
			{
				struct chunk* old_chunk=cur_chunk;
				cur_chunk=old_chunk->prev;
				free(old_chunk);
				bad_cell=&cur_chunk->cell[cells_per_chunk];
				cur_cell=bad_cell-1;
			}

			k--;
		}
		if((buf[0]!='~') || (buf[1]!=' '))
			fprintf(stderr,"(The clause on line %lld is always satisfied)\n",clauses);
		nullclauses++;

clause_done:
		cells=cells+k;

	}
	if((vars>>hbits) >= 10)
	{
		fprintf(stderr,"There are %lld variables but only %d hash tables;\n", vars, 1<<hbits);
		while((vars>>hbits) >= 10)
			hbits++;
		fprintf(stderr," maybe you should use command-line option h%d?\n",hbits);
	}
	clauses-=nullclauses;
	if(clauses==0)
	{
		fprintf(stderr,"No clauses were input!\n");
		exit(-77);
	}
	assert(vars<0x80000000);
	assert(clauses<0x80000000);
	assert(cells<0x100000000);

	if(verbose&show_basics)
		fprintf(stderr, "(%lld variables, %lld clauses, %llu literals successfully read)\n", vars,clauses,cells);

	free(buf);
	free(hash);
	mem= (cell*)malloc(cells*sizeof(cell));
	assert(mem);
	bytes= cells*sizeof(cell);
	nonspec= vars+vars+2;
	assert(nonspec+clauses<0x100000000);
	cmem= (clause*)malloc((nonspec+clauses)*sizeof(clause));
	assert(cmem);
	bytes+= (nonspec+clauses)*sizeof(clause);
	vmem= (variable*)malloc((vars+1)*sizeof(variable));
	assert(vmem);
	bytes+= (vars+1)*sizeof(variable);
	move= (char*)malloc((vars+1)*sizeof(char));
	assert(move);

	for(j= 0;j<nonspec;j++)
	{
		cmem[j].start=0;
		cmem[j].wlink=0;
	};

	for(c=nonspec+clauses-1,k=0; c>=nonspec; c--)
	{
		j= 0;
		for(i= 0;i<2;j++)
		{
			if(cur_cell > &cur_chunk->cell[0])
				cur_cell--;
			else
			{
				struct chunk* old_chunk=cur_chunk;
				cur_chunk=old_chunk->prev;
				free(old_chunk);
				bad_cell=&cur_chunk->cell[cells_per_chunk];
				cur_cell=bad_cell-1;
			}

			i=hack_out(*cur_cell);
			p=hack_clean(*cur_cell)->serial;
			p += p+(i&1)+2;
			if(j==0)
			{
				cmem[c].start=k;
				cmem[c].wlink=cmem[p].wlink;
				cmem[p].wlink=c;
				j=1;
			};
			mem[k++].litno=p;
		}
	}
	cmem[c].start=k;

	for(c=vars; c; c--)
	{
		if(cur_tmp_var > &cur_vchunk->var[0])
			cur_tmp_var--;
		else
		{
			struct vchunk* old_vchunk=cur_vchunk;
			cur_vchunk=old_vchunk->prev;
			free(old_vchunk);
			bad_tmp_var=&cur_vchunk->var[vars_per_vchunk];
			cur_tmp_var=bad_tmp_var-1;
		}

		vmem[c].name=cur_tmp_var->name;
	}

	if(cur_cell != &cur_chunk->cell[0] ||
			cur_chunk->prev!=NULL ||
			cur_tmp_var!=&cur_vchunk->var[0] ||
			cur_vchunk->prev!=NULL)
	{
		fprintf(stderr,"This can't happen (consistency check failure)!\n");
		exit(-14);
	}
	free(cur_chunk);
	free(cur_vchunk);

	level=1;
newlevel:
	if(level > vars)
		goto satisfied;
	//stat[level]++;
	move[level]=(cmem[level+level+1].wlink!=0 || cmem[level+level].wlink==0);
#if 0
	printf ("line %d, mem[level+level+1].wlink=%d mem[level+level].wlink=%d\n",
                __LINE__, cmem[level+level+1].wlink, cmem[level+level].wlink);
	printf ("line %d, move[%d]=%d\n", __LINE__, level, move[level]);
#endif
	//move[level]=1;
	if((verbose&show_choices) && level<=show_choices_max)
	{
		fprintf(stderr,"Level %d, trying %s%.8s",
				level,move[level]?"~":"", (char*)&vmem[level].name);
		fprintf(stderr,"\n");
	}
	nodes++;
        if(verbose&show_details)
	        print_state(level);
tryit:
	parity=move[level]&1;

	for(c=cmem[level+level+1-parity].wlink; c; c=q)
	{
		i=cmem[c].start;
		q=cmem[c].wlink;
		j=cmem[c-1].start;
		for(p=i+1; p<j; p++)
		{
			k=mem[p].litno;
			if(k>=level+level || (((move[k>>1]^k)&1)==0))
				break;
		}
		if(p==j)
		{
			if(verbose&show_details)
				fprintf(stderr,"(Clause %d contradicted)\n", c);
			cmem[level+level+1-parity].wlink=c;
			goto try_again;
		}
		mem[i].litno=k;
		mem[p].litno=level+level+1-parity;
		cmem[c].wlink=cmem[k].wlink;
		cmem[k].wlink=c;
		if(verbose&show_details)
			fprintf(stderr,"(Clause %d now watches %s%.8s)\n",
					c,k&1?"~":"", (char*)&vmem[k>>1].name);
	}
	cmem[level+level+1-parity].wlink=0;

	level++;
	goto newlevel;
try_again:
	if(move[level] < 2)
	{
		move[level] = 3-move[level];
		if((verbose&show_choices) && level<=show_choices_max)
		{
			fprintf(stderr,"Level %d, trying again",level);
			fprintf(stderr,"\n");
		}
		goto tryit;
	}
	if(level > 1)
	{
		level--;
		goto try_again;
	}

	if(1)
	{
		printf("~\n");
		if(verbose&show_basics)
			fprintf(stderr,"UNSAT\n");
	}
	else
	{
satisfied:
		if(verbose&show_basics)
			fprintf(stderr,"!SAT!\n");

                if(verbose&show_details)
		        print_state(level);

		for(k=1; k<level; k++)
			printf(" %s%.8s", move[k]&1?"~":"", (char*)&vmem[k].name);
		printf("\n");

	}

done:
	if(verbose&show_basics)
		fprintf(stderr,"Altogether %llu bytes, %llu nodes.\n",
				bytes,nodes);
}