id	sid	tid	token	lemma	pos
0c483j35215	1	1	there	there	PRON
0c483j35215	1	2	are	be	VERB
0c483j35215	1	3	many	many	ADJ
0c483j35215	1	4	problems	problem	NOUN
0c483j35215	1	5	that	that	PRON
0c483j35215	1	6	can	can	AUX
0c483j35215	1	7	not	not	PART
0c483j35215	1	8	be	be	AUX
0c483j35215	1	9	solved	solve	VERB
0c483j35215	1	10	with	with	ADP
0c483j35215	1	11	today	today	NOUN
0c483j35215	1	12	's	's	PART
0c483j35215	1	13	digital	digital	ADJ
0c483j35215	1	14	computers	computer	NOUN
0c483j35215	1	15	.	.	PUNCT
0c483j35215	2	1	one	one	NUM
0c483j35215	2	2	of	of	ADP
0c483j35215	2	3	the	the	DET
0c483j35215	2	4	most	most	ADV
0c483j35215	2	5	studied	study	VERB
0c483j35215	2	6	such	such	ADJ
0c483j35215	2	7	problems	problem	NOUN
0c483j35215	2	8	is	be	AUX
0c483j35215	2	9	boolean	boolean	ADJ
0c483j35215	2	10	satisfiability	satisfiability	NOUN
0c483j35215	2	11	(	(	PUNCT
0c483j35215	2	12	k	k	PROPN
0c483j35215	2	13	-	-	NOUN
0c483j35215	2	14	sat	sat	PROPN
0c483j35215	2	15	)	)	PUNCT
0c483j35215	2	16	,	,	PUNCT
0c483j35215	2	17	which	which	PRON
0c483j35215	2	18	asks	ask	VERB
0c483j35215	2	19	to	to	PART
0c483j35215	2	20	find	find	VERB
0c483j35215	2	21	the	the	DET
0c483j35215	2	22	truth	truth	NOUN
0c483j35215	2	23	-	-	PUNCT
0c483j35215	2	24	values	value	NOUN
0c483j35215	2	25	for	for	ADP
0c483j35215	2	26	a	a	DET
0c483j35215	2	27	set	set	NOUN
0c483j35215	2	28	of	of	ADP
0c483j35215	2	29	boolean	boolean	ADJ
0c483j35215	2	30	variables	variable	NOUN
0c483j35215	2	31	in	in	ADP
0c483j35215	2	32	a	a	DET
0c483j35215	2	33	way	way	NOUN
0c483j35215	2	34	to	to	PART
0c483j35215	2	35	satisfy	satisfy	VERB
0c483j35215	2	36	a	a	DET
0c483j35215	2	37	given	give	VERB
0c483j35215	2	38	number	number	NOUN
0c483j35215	2	39	of	of	ADP
0c483j35215	2	40	constraints	constraint	NOUN
0c483j35215	2	41	.	.	PUNCT
0c483j35215	3	1	this	this	DET
0c483j35215	3	2	problem	problem	NOUN
0c483j35215	3	3	appears	appear	VERB
0c483j35215	3	4	in	in	ADP
0c483j35215	3	5	many	many	ADJ
0c483j35215	3	6	real	real	ADJ
0c483j35215	3	7	-	-	PUNCT
0c483j35215	3	8	world	world	NOUN
0c483j35215	3	9	applications	application	NOUN
0c483j35215	3	10	,	,	PUNCT
0c483j35215	3	11	and	and	CCONJ
0c483j35215	3	12	it	it	PRON
0c483j35215	3	13	has	have	VERB
0c483j35215	3	14	a	a	DET
0c483j35215	3	15	key	key	ADJ
0c483j35215	3	16	role	role	NOUN
0c483j35215	3	17	in	in	ADP
0c483j35215	3	18	the	the	DET
0c483j35215	3	19	theory	theory	NOUN
0c483j35215	3	20	of	of	ADP
0c483j35215	3	21	computational	computational	ADJ
0c483j35215	3	22	complexity	complexity	NOUN
0c483j35215	3	23	and	and	CCONJ
0c483j35215	3	24	in	in	ADP
0c483j35215	3	25	particular	particular	ADJ
0c483j35215	3	26	np	np	NOUN
0c483j35215	3	27	-	-	NOUN
0c483j35215	3	28	completeness	completeness	NOUN
0c483j35215	3	29	:	:	PUNCT
0c483j35215	3	30	if	if	SCONJ
0c483j35215	3	31	one	one	PRON
0c483j35215	3	32	would	would	AUX
0c483j35215	3	33	find	find	VERB
0c483j35215	3	34	an	an	DET
0c483j35215	3	35	efficient	efficient	ADJ
0c483j35215	3	36	(	(	PUNCT
0c483j35215	3	37	polynomial	polynomial	ADJ
0c483j35215	3	38	-	-	PUNCT
0c483j35215	3	39	time	time	NOUN
0c483j35215	3	40	)	)	PUNCT
0c483j35215	3	41	algorithm	algorithm	X
0c483j35215	3	42	to	to	PART
0c483j35215	3	43	solve	solve	VERB
0c483j35215	3	44	k	k	PROPN
0c483j35215	3	45	-	-	NOUN
0c483j35215	3	46	sat	sat	PROPN
0c483j35215	3	47	(	(	PUNCT
0c483j35215	3	48	for	for	ADP
0c483j35215	3	49	k>2	k>2	PROPN
0c483j35215	3	50	)	)	PUNCT
0c483j35215	3	51	,	,	PUNCT
0c483j35215	3	52	then	then	ADV
0c483j35215	3	53	we	we	PRON
0c483j35215	3	54	would	would	AUX
0c483j35215	3	55	be	be	AUX
0c483j35215	3	56	able	able	ADJ
0c483j35215	3	57	to	to	PART
0c483j35215	3	58	generate	generate	VERB
0c483j35215	3	59	solutions	solution	NOUN
0c483j35215	3	60	efficiently	efficiently	ADV
0c483j35215	3	61	to	to	ADP
0c483j35215	3	62	all	all	DET
0c483j35215	3	63	problems	problem	NOUN
0c483j35215	3	64	from	from	ADP
0c483j35215	3	65	the	the	DET
0c483j35215	3	66	np	np	PROPN
0c483j35215	3	67	class	class	NOUN
0c483j35215	3	68	(	(	PUNCT
0c483j35215	3	69	cook	cook	NOUN
0c483j35215	3	70	-	-	PUNCT
0c483j35215	3	71	levin	levin	PROPN
0c483j35215	3	72	theorem	theorem	PROPN
0c483j35215	3	73	)	)	PUNCT
0c483j35215	3	74	,	,	PUNCT
0c483j35215	3	75	i.e.	i.e.	X
0c483j35215	3	76	,	,	PUNCT
0c483j35215	3	77	to	to	ADP
0c483j35215	3	78	a	a	DET
0c483j35215	3	79	very	very	ADV
0c483j35215	3	80	large	large	ADJ
0c483j35215	3	81	number	number	NOUN
0c483j35215	3	82	of	of	ADP
0c483j35215	3	83	hard	hard	ADJ
0c483j35215	3	84	problems.the	problems.the	DET
0c483j35215	3	85	thesis	thesis	NOUN
0c483j35215	3	86	focuses	focus	VERB
0c483j35215	3	87	on	on	ADP
0c483j35215	3	88	the	the	DET
0c483j35215	3	89	k	k	PROPN
0c483j35215	3	90	-	-	PUNCT
0c483j35215	3	91	sat	sit	VERB
0c483j35215	3	92	problem	problem	NOUN
0c483j35215	3	93	and	and	CCONJ
0c483j35215	3	94	presents	present	VERB
0c483j35215	3	95	a	a	DET
0c483j35215	3	96	novel	novel	ADJ
0c483j35215	3	97	approach	approach	NOUN
0c483j35215	3	98	to	to	ADP
0c483j35215	3	99	it	it	PRON
0c483j35215	3	100	,	,	PUNCT
0c483j35215	3	101	using	use	VERB
0c483j35215	3	102	a	a	DET
0c483j35215	3	103	deterministic	deterministic	ADJ
0c483j35215	3	104	continuous	continuous	ADJ
0c483j35215	3	105	-	-	PUNCT
0c483j35215	3	106	time	time	NOUN
0c483j35215	3	107	dynamical	dynamical	ADJ
0c483j35215	3	108	system	system	NOUN
0c483j35215	3	109	.	.	PUNCT
0c483j35215	4	1	this	this	DET
0c483j35215	4	2	dynamical	dynamical	ADJ
0c483j35215	4	3	system	system	NOUN
0c483j35215	4	4	solves	solve	VERB
0c483j35215	4	5	the	the	DET
0c483j35215	4	6	problem	problem	NOUN
0c483j35215	4	7	efficiently	efficiently	ADV
0c483j35215	4	8	(	(	PUNCT
0c483j35215	4	9	in	in	ADP
0c483j35215	4	10	polynomial	polynomial	ADJ
0c483j35215	4	11	continuous	continuous	ADJ
0c483j35215	4	12	-	-	PUNCT
0c483j35215	4	13	time	time	NOUN
0c483j35215	4	14	)	)	PUNCT
0c483j35215	4	15	at	at	ADP
0c483j35215	4	16	the	the	DET
0c483j35215	4	17	expense	expense	NOUN
0c483j35215	4	18	of	of	ADP
0c483j35215	4	19	exponential	exponential	ADJ
0c483j35215	4	20	fluctuations	fluctuation	NOUN
0c483j35215	4	21	in	in	ADP
0c483j35215	4	22	its	its	PRON
0c483j35215	4	23	energy	energy	NOUN
0c483j35215	4	24	function	function	NOUN
0c483j35215	4	25	,	,	PUNCT
0c483j35215	4	26	while	while	SCONJ
0c483j35215	4	27	it	it	PRON
0c483j35215	4	28	also	also	ADV
0c483j35215	4	29	shows	show	VERB
0c483j35215	4	30	that	that	SCONJ
0c483j35215	4	31	problem	problem	NOUN
0c483j35215	4	32	hardness	hardness	NOUN
0c483j35215	4	33	is	be	AUX
0c483j35215	4	34	translated	translate	VERB
0c483j35215	4	35	into	into	ADP
0c483j35215	4	36	a	a	DET
0c483j35215	4	37	transiently	transiently	ADV
0c483j35215	4	38	chaotic	chaotic	ADJ
0c483j35215	4	39	behavior	behavior	NOUN
0c483j35215	4	40	of	of	ADP
0c483j35215	4	41	the	the	DET
0c483j35215	4	42	analog	analog	ADJ
0c483j35215	4	43	trajectories	trajectory	NOUN
0c483j35215	4	44	by	by	ADP
0c483j35215	4	45	this	this	DET
0c483j35215	4	46	system	system	NOUN
0c483j35215	4	47	.	.	PUNCT
0c483j35215	5	1	we	we	PRON
0c483j35215	5	2	use	use	VERB
0c483j35215	5	3	the	the	DET
0c483j35215	5	4	escape	escape	NOUN
0c483j35215	5	5	rate	rate	NOUN
0c483j35215	5	6	,	,	PUNCT
0c483j35215	5	7	an	an	DET
0c483j35215	5	8	invariant	invariant	ADJ
0c483j35215	5	9	measure	measure	NOUN
0c483j35215	5	10	of	of	ADP
0c483j35215	5	11	transient	transient	ADJ
0c483j35215	5	12	chaos	chaos	NOUN
0c483j35215	5	13	,	,	PUNCT
0c483j35215	5	14	to	to	PART
0c483j35215	5	15	show	show	VERB
0c483j35215	5	16	that	that	SCONJ
0c483j35215	5	17	hardness	hardness	NOUN
0c483j35215	5	18	appears	appear	VERB
0c483j35215	5	19	through	through	ADP
0c483j35215	5	20	a	a	DET
0c483j35215	5	21	second	second	ADJ
0c483j35215	5	22	-	-	PUNCT
0c483j35215	5	23	order	order	NOUN
0c483j35215	5	24	phase	phase	NOUN
0c483j35215	5	25	transition	transition	NOUN
0c483j35215	5	26	in	in	ADP
0c483j35215	5	27	the	the	DET
0c483j35215	5	28	random	random	ADJ
0c483j35215	5	29	3	3	NUM
0c483j35215	5	30	-	-	PUNCT
0c483j35215	5	31	sat	sat	NOUN
0c483j35215	5	32	and	and	CCONJ
0c483j35215	5	33	4	4	NUM
0c483j35215	5	34	-	-	PUNCT
0c483j35215	5	35	sat	sit	VERB
0c483j35215	5	36	ensemble	ensemble	NOUN
0c483j35215	5	37	.	.	PUNCT
0c483j35215	6	1	since	since	SCONJ
0c483j35215	6	2	the	the	DET
0c483j35215	6	3	solver	solver	NOUN
0c483j35215	6	4	(	(	PUNCT
0c483j35215	6	5	i.e.	i.e.	X
0c483j35215	6	6	,	,	PUNCT
0c483j35215	6	7	the	the	DET
0c483j35215	6	8	dynamical	dynamical	ADJ
0c483j35215	6	9	system	system	NOUN
0c483j35215	6	10	expressed	express	VERB
0c483j35215	6	11	as	as	ADP
0c483j35215	6	12	ordinary	ordinary	ADJ
0c483j35215	6	13	differential	differential	ADJ
0c483j35215	6	14	equations	equation	NOUN
0c483j35215	6	15	)	)	PUNCT
0c483j35215	6	16	,	,	PUNCT
0c483j35215	6	17	involves	involve	VERB
0c483j35215	6	18	only	only	ADV
0c483j35215	6	19	polynomial	polynomial	ADJ
0c483j35215	6	20	functions	function	NOUN
0c483j35215	6	21	of	of	ADP
0c483j35215	6	22	low	low	ADJ
0c483j35215	6	23	order	order	NOUN
0c483j35215	6	24	,	,	PUNCT
0c483j35215	6	25	is	be	AUX
0c483j35215	6	26	well	well	ADV
0c483j35215	6	27	suited	suited	ADJ
0c483j35215	6	28	for	for	ADP
0c483j35215	6	29	implementation	implementation	NOUN
0c483j35215	6	30	by	by	ADP
0c483j35215	6	31	specialized	specialized	ADJ
0c483j35215	6	32	analog	analog	NOUN
0c483j35215	6	33	circuits	circuit	NOUN
0c483j35215	6	34	.	.	PUNCT
0c483j35215	7	1	as	as	SCONJ
0c483j35215	7	2	the	the	DET
0c483j35215	7	3	dynamical	dynamical	ADJ
0c483j35215	7	4	system	system	NOUN
0c483j35215	7	5	is	be	AUX
0c483j35215	7	6	not	not	PART
0c483j35215	7	7	unique	unique	ADJ
0c483j35215	7	8	,	,	PUNCT
0c483j35215	7	9	we	we	PRON
0c483j35215	7	10	introduce	introduce	VERB
0c483j35215	7	11	several	several	ADJ
0c483j35215	7	12	slightly	slightly	ADV
0c483j35215	7	13	modified	modify	VERB
0c483j35215	7	14	versions	version	NOUN
0c483j35215	7	15	of	of	ADP
0c483j35215	7	16	it	it	PRON
0c483j35215	7	17	,	,	PUNCT
0c483j35215	7	18	with	with	ADP
0c483j35215	7	19	the	the	DET
0c483j35215	7	20	goal	goal	NOUN
0c483j35215	7	21	of	of	ADP
0c483j35215	7	22	making	make	VERB
0c483j35215	7	23	its	its	PRON
0c483j35215	7	24	implementation	implementation	NOUN
0c483j35215	7	25	even	even	ADV
0c483j35215	7	26	more	more	ADV
0c483j35215	7	27	feasible	feasible	ADJ
0c483j35215	7	28	.	.	PUNCT
0c483j35215	8	1	we	we	PRON
0c483j35215	8	2	briefly	briefly	ADV
0c483j35215	8	3	present	present	VERB
0c483j35215	8	4	a	a	DET
0c483j35215	8	5	proposal	proposal	NOUN
0c483j35215	8	6	for	for	ADP
0c483j35215	8	7	a	a	DET
0c483j35215	8	8	modular	modular	ADJ
0c483j35215	8	9	and	and	CCONJ
0c483j35215	8	10	programmable	programmable	ADJ
0c483j35215	8	11	design	design	NOUN
0c483j35215	8	12	for	for	ADP
0c483j35215	8	13	an	an	DET
0c483j35215	8	14	analog	analog	ADJ
0c483j35215	8	15	hardware	hardware	NOUN
0c483j35215	8	16	sat	sat	NOUN
0c483j35215	8	17	-	-	PUNCT
0c483j35215	8	18	solver	solver	PROPN
0c483j35215	8	19	,	,	PUNCT
0c483j35215	8	20	which	which	PRON
0c483j35215	8	21	solves	solve	VERB
0c483j35215	8	22	hard	hard	ADJ
0c483j35215	8	23	problems	problem	NOUN
0c483j35215	8	24	more	more	ADJ
0c483j35215	8	25	than	than	ADP
0c483j35215	8	26	10,000	10,000	NUM
0c483j35215	8	27	times	time	NOUN
0c483j35215	8	28	faster	fast	ADJ
0c483j35215	8	29	than	than	ADP
0c483j35215	8	30	state	state	NOUN
0c483j35215	8	31	-	-	PUNCT
0c483j35215	8	32	of	of	ADP
0c483j35215	8	33	-	-	PUNCT
0c483j35215	8	34	the	the	DET
0c483j35215	8	35	-	-	PUNCT
0c483j35215	8	36	art	art	NOUN
0c483j35215	8	37	algorithms	algorithm	NOUN
0c483j35215	8	38	(	(	PUNCT
0c483j35215	8	39	minisat	minisat	PROPN
0c483j35215	8	40	)	)	PUNCT
0c483j35215	8	41	run	run	VERB
0c483j35215	8	42	on	on	ADP
0c483j35215	8	43	digital	digital	ADJ
0c483j35215	8	44	computers	computer	NOUN
0c483j35215	8	45	.	.	PUNCT
0c483j35215	9	1	finally	finally	ADV
0c483j35215	9	2	,	,	PUNCT
0c483j35215	9	3	we	we	PRON
0c483j35215	9	4	use	use	VERB
0c483j35215	9	5	our	our	PRON
0c483j35215	9	6	system	system	NOUN
0c483j35215	9	7	to	to	PART
0c483j35215	9	8	solve	solve	VERB
0c483j35215	9	9	max	max	PROPN
0c483j35215	9	10	-	-	PUNCT
0c483j35215	9	11	sat	sat	PROPN
0c483j35215	9	12	instances	instance	NOUN
0c483j35215	9	13	.	.	PUNCT
0c483j35215	10	1	max	max	PROPN
0c483j35215	10	2	-	-	PUNCT
0c483j35215	10	3	sat	sat	PROPN
0c483j35215	10	4	is	be	AUX
0c483j35215	10	5	an	an	DET
0c483j35215	10	6	optimization	optimization	NOUN
0c483j35215	10	7	problem	problem	NOUN
0c483j35215	10	8	,	,	PUNCT
0c483j35215	10	9	which	which	PRON
0c483j35215	10	10	asks	ask	VERB
0c483j35215	10	11	to	to	PART
0c483j35215	10	12	find	find	VERB
0c483j35215	10	13	the	the	DET
0c483j35215	10	14	assignment	assignment	NOUN
0c483j35215	10	15	of	of	ADP
0c483j35215	10	16	the	the	DET
0c483j35215	10	17	boolean	boolean	ADJ
0c483j35215	10	18	variables	variable	NOUN
0c483j35215	10	19	such	such	ADJ
0c483j35215	10	20	as	as	ADP
0c483j35215	10	21	to	to	PART
0c483j35215	10	22	minimize	minimize	VERB
0c483j35215	10	23	the	the	DET
0c483j35215	10	24	number	number	NOUN
0c483j35215	10	25	of	of	ADP
0c483j35215	10	26	constraints	constraint	NOUN
0c483j35215	10	27	that	that	PRON
0c483j35215	10	28	can	can	AUX
0c483j35215	10	29	not	not	PART
0c483j35215	10	30	be	be	AUX
0c483j35215	10	31	satisfied	satisfied	ADJ
0c483j35215	10	32	.	.	PUNCT
0c483j35215	11	1	we	we	PRON
0c483j35215	11	2	present	present	VERB
0c483j35215	11	3	a	a	DET
0c483j35215	11	4	heuristic	heuristic	ADJ
0c483j35215	11	5	analog	analog	NOUN
0c483j35215	11	6	algorithm	algorithm	X
0c483j35215	11	7	based	base	VERB
0c483j35215	11	8	on	on	ADP
0c483j35215	11	9	our	our	PRON
0c483j35215	11	10	dynamical	dynamical	ADJ
0c483j35215	11	11	system	system	NOUN
0c483j35215	11	12	and	and	CCONJ
0c483j35215	11	13	show	show	VERB
0c483j35215	11	14	that	that	SCONJ
0c483j35215	11	15	it	it	PRON
0c483j35215	11	16	,	,	PUNCT
0c483j35215	11	17	indeed	indeed	ADV
0c483j35215	11	18	,	,	PUNCT
0c483j35215	11	19	solves	solve	VERB
0c483j35215	11	20	many	many	ADJ
0c483j35215	11	21	max	max	PROPN
0c483j35215	11	22	-	-	PUNCT
0c483j35215	11	23	sat	sit	VERB
0c483j35215	11	24	problems	problem	NOUN
0c483j35215	11	25	efficiently	efficiently	ADV
0c483j35215	11	26	.	.	PUNCT