о разных алгоритмах

[avva]

(интересно будет только программистам)

1. Неплохое описание схемы работы с большими массивами без инициализации, при том, что в них может лежать мусор. Это красивый трюк, и изредка действительно полезный; я додумался до него сам как-то в процессе решения какой-то задачи в университете (подробностей не помню, может, задача именно так и была сформулирована), но ни разу не применял его на практике.

2. Я зашел на Project Euler впервые после долгого перерыва, и решил две последние задачки. Получил огромное удовольствие, хоть и написал решения на C не вполне понятно почему. В одной из них мне пригодился фокус из HAKMEM (перебор всех способов выбрать k элементов из n, с помощью битмаски), а в другой - disjoint-set, которым я тоже не пользовался очень давно.

Вообще disjoint-set - волшебно красивая штука. Я помню, что у меня затаило дыхание, когда я впервые увидел. Это алгоритм из Книги, поистине.

3. В связи с одной из задач наткнулся на страничку про MiniSat. Я не знал, что есть соревнования по решению SAT! Хочется найти время и почитать этот, вроде бы относительно простой и тем не менее эффективный, алгоритм. Исходники там есть.

4. Я тут узнал, что не все знают о Project Euler. Друзья, если вы получаете удовольствие от программирования, вам прямая дорога туда. Почти в каждой задаче там надо придумать способ ее решить, который даст ответ достаточно быстро - но суть не в бездумных оптимизациях, а в алгоритмах и структурах данных. Это, может, звучит сухо, но на деле невероятно увлекательно; а еще - умный ход - когда правильно решаешь задачу, получаешь доступ на тему на форуме, где уже решившие обсуждают свои решения и делятся кодом.

Comments

Re: MiniSAT

[avva.livejournal.com]

How do you apply MiniSAT to searching bugs? Do you have a link to her paper?

Re: MiniSAT

[(Anonymous)]

my understanding (but I am not in this business so may be wrong) is that they convert C/C++ code into a database of a special format. The format is convenient to run MiniSAT (or other SAT solver) over. The (assumed) bug (e.g. memory overflow etc.) itself is represented as a Boolean formula (in fact, it is negation of the statement that there is NO such bug). SAT searches satisfying assignment ( which is a counterexample) of this formula using the database as a context (i.e. set of the restrictions on the search space). If there is such assignment, it is decoded back into the fragment of the original C code and identifies the bug.

it's better to ask her, of course

webpage:

http://www.inf.unisi.ch/faculty/sharygina/

there are even some tools for such debugging on the webpage...

iz.

Re: MiniSAT

[avva.livejournal.com]

Alright, thanks a lot!