Prax 2: lausearvutuse lahendajatega eksperimenteerimine - Redigeerimiste ajalugu

Tammet – 12. märts 2015, kell 12:39

2015-03-12T12:39:38Z

←Vanem redaktsioon		Redaktsioon: 12. märts 2015, kell 14:39
4. rida:		4. rida:
	* Katsetada veidi [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html] lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.		* Katsetada veidi [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html] lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff, [http://minisat.se/ Minisat]) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/).
	* Otsi erinevaid ülesande-näidete komplekte.		* Otsi erinevaid ülesande-näidete komplekte.
	* Proovi lahendajaid keerukamatel näidetel:		* Proovi lahendajaid keerukamatel näidetel:

Tammet – 26. veebruar 2015, kell 15:57

2015-02-26T15:57:08Z

←Vanem redaktsioon		Redaktsioon: 26. veebruar 2015, kell 17:57
2. rida:		2. rida:
	Selle ülesande sisuks on:		Selle ülesande sisuks on:

	* Katsetada veidi [http://dijkstra.cs.ttu.ee/~tammet/~~proptools~~.html] lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.		* Katsetada veidi [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html] lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)
14. rida:		14. rida:
	*** ja siis googeldada		*** ja siis googeldada
	** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)		** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)
	** katseta, kas mõni [http://dijkstra.cs.ttu.ee/~tammet/~~proptools~~.html] lehel lahendaja suudab eelmist liiki ülesannet lahendada (tõenäoliselt ei suuda).		** katseta, kas mõni [http://dijkstra.cs.ttu.ee/~tammet/proplogic.html] lehel lahendaja suudab eelmist liiki ülesannet lahendada (tõenäoliselt ei suuda).
	** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud		** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud
	* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.		* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.

	Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.		Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.

Tammet – 26. veebruar 2015, kell 15:56

2015-02-26T15:56:42Z

←Vanem redaktsioon		Redaktsioon: 26. veebruar 2015, kell 17:56
2. rida:		2. rida:
	Selle ülesande sisuks on:		Selle ülesande sisuks on:

	* Katsetada veidi proptools lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.		* Katsetada veidi [http://dijkstra.cs.ttu.ee/~tammet/proptools.html] lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)
14. rida:		14. rida:
	*** ja siis googeldada		*** ja siis googeldada
	** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)		** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)
	** katseta, kas mõni proptools lehel lahendaja suudab eelmist liiki ülesannet lahendada (tõenäoliselt ei suuda).		** katseta, kas mõni [http://dijkstra.cs.ttu.ee/~tammet/proptools.html] lehel lahendaja suudab eelmist liiki ülesannet lahendada (tõenäoliselt ei suuda).
	** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud		** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud
	* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.		* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.

	Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.		Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.

Tammet – 26. veebruar 2015, kell 15:56

2015-02-26T15:56:02Z

←Vanem redaktsioon		Redaktsioon: 26. veebruar 2015, kell 17:56
1. rida:		1. rida:

	Selle ülesande sisuks on:		Selle ülesande sisuks on:

			* Katsetada veidi proptools lehel olevate erinevate algoritmidega: leia iga kolme algoritmi jaoks (naiivseid pole vaja kasutada) mittetriviaalne ülesanne, mida see algoritm teeb oluliselt kiiremini, kui teised algoritmid. Eeskätt siis leia tabeli ja resolutsioonimeetodi jaoks ülesanded, mis nende puhul lahenduvad oluliselt kiiremini kui dpll-ga. Võibolla see ei õnnestu.

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)
12. rida:		14. rida:
	*** ja siis googeldada		*** ja siis googeldada
	** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)		** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)
			** katseta, kas mõni proptools lehel lahendaja suudab eelmist liiki ülesannet lahendada (tõenäoliselt ei suuda).
	** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud		** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud
	* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.		* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.

	Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.		Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.

Tammet – 14. veebruar 2013, kell 17:09

2013-02-14T17:09:32Z

←Vanem redaktsioon		Redaktsioon: 14. veebruar 2013, kell 19:09
2. rida:		2. rida:
	Selle ülesande sisuks on:		Selle ülesande sisuks on:

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi wiki lõpust http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ja võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)
	* Otsi erinevaid ülesande-näidete komplekte.		* Otsi erinevaid ülesande-näidete komplekte.
	* Proovi lahendajaid keerukamatel näidetel:		* Proovi lahendajaid keerukamatel näidetel:

Tammet – 14. veebruar 2013, kell 17:09

2013-02-14T17:09:05Z

←Vanem redaktsioon		Redaktsioon: 14. veebruar 2013, kell 19:09
2. rida:		2. rida:
	Selle ülesande sisuks on:		Selle ülesande sisuks on:

	* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat.		* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. Võid valida mõne tuntudm veidi vanema, aga selle sajandi tõestaja (SATO, Grasp, zChaff) ja/või mõne uuema (neid otsi võistluse lehtedelt http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010/)
	* Otsi erinevaid ülesande-näidete komplekte.		* Otsi erinevaid ülesande-näidete komplekte.
	* Proovi lahendajaid keerukamatel näidetel:		* Proovi lahendajaid keerukamatel näidetel:
	** leia mõned näited, mida kumbki lahendaja ei suuda ntx 10 sekundi jooksul lahendada		** leia mõned näited, mida kumbki lahendaja ei suuda ntx 10 sekundi jooksul lahendada. Näiteid võid leida:
			*** http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html (enamasti lihtsamad näited)
			*** http://en.wikipedia.org/wiki/Boolean_satisfiability_problem lõpust
			*** http://www.satlib.org/ (suur näidete kogu)
			*** võistlused http://www.satcompetition.org/ ja http://baldur.iti.uka.de/sat-race-2010
			*** ja siis googeldada
	** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)		** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)
	** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud		** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud

Tammet – 14. veebruar 2013, kell 17:00

2013-02-14T17:00:12Z

←Vanem redaktsioon		Redaktsioon: 14. veebruar 2013, kell 19:00
6. rida:		6. rida:
	* Proovi lahendajaid keerukamatel näidetel:		* Proovi lahendajaid keerukamatel näidetel:
	** leia mõned näited, mida kumbki lahendaja ei suuda ntx 10 sekundi jooksul lahendada		** leia mõned näited, mida kumbki lahendaja ei suuda ntx 10 sekundi jooksul lahendada
	** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks ~~oll~~ SAT ja mõned mitte-sat näited)		** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks olla SAT ja mõned mitte-sat näited)
	** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud		** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud
	* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.		* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.

	Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.		Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.

Tammet: Uus lehekülg: ' Selle ülesande sisuks on: * Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. * Otsi erinevaid ülesande-näidete komplekte....'

2013-02-14T16:59:52Z

Uus lehekülg: ' Selle ülesande sisuks on: * Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat. * Otsi erinevaid ülesande-näidete komplekte....'

Uus lehekülg

Selle ülesande sisuks on:

* Pane endal käima vähemalt kaks erinevat olemasolevat, tuntud ja võimsat lausearvutuse lahendajat.
* Otsi erinevaid ülesande-näidete komplekte.
* Proovi lahendajaid keerukamatel näidetel:
** leia mõned näited, mida kumbki lahendaja ei suuda ntx 10 sekundi jooksul lahendada
** leia mõned näited, mida üks lahendaja suudab, aga teine ei suuda ntx 10 sekundi jooksul lahendada (mõned võiks oll SAT ja mõned mitte-sat näited)
** vaata, kas lahendajal on mingid valitavad otsingustrateegiad: kui jah, siis proovi lahendaja strateegiat sättida, nii et ta suudaks sättimise järel lahendada mõne ülesande, mida ta ilma sättimata ei suutnud
* Hea mõte - ei ole otse kohustuslik - on genereerida ise ülesandeid, mida lahendaja ei suudaks ntx 10 sek jooksul lahenda. Näiteks nii, et genereerid lihtsamaid, siis keerulisemaid jne kuni lahendajal läheb liiga kaua aega. Kui ülesandeid ise genereerid, siis ei ol vaja mujalt näiteid otsida.

Tee tulemustest väike presentatsioon ja kanna praksis ette, aega selleks ca 5 minutit.