В структуру данных дизъюнкты добавляются и удаляются. Число в таблице - это максимальный объем структуры данных, который был в ходе итераций. Например, в логе это 28434.
Число >86000 клауз - это сколько дизъюнктов в структуре данных. В самом тесте 840 дизъюнктов от 225 переменных. Дальше метод резолюций выводит новые дизъюнкты, исключая переменные и пополняя базу дизъюнктов. Одни дизъюнкты (с очередной переменной) удаляются, а их попарные резольвенты добавляются.
В качестве примера работы могу только привести, сколько дизъюнктов в базе на каждой итерации.
Спасибо за полезный ответ! Действительно, алгоритм очень похож на DP, но вместо эвристик "Unit-literal rule" и "Pure-literal rule" поддерживается структура данных, сразу исключающая все возможные поглощения клауз. За счет этого количество клауз в множестве становится меньше.
Данная задача возникла на таком примере. С помощью численных методов рассчитывалась зависимость температуры двух тепловых источников от их мощности. В результате получилась зависимость, похожая на линейную. Точнее, линии уровня на координатной плоскости были почти прямыми линиями, но не равноотстоящими. В связи с этим возникла идея: как оценить аналитически такую зависимость. Если наклон изолиний заранее неизвестен, а также неизвестна функция связи.
так кроме сплайнов-то f может еще чем-то быть или нет?
В примере f = sqrt(z), то есть это может быть любая функция.
Сплайны здесь используются скорее для оценки плавности зависимости, т.е. для расчета целевой функции. Чтобы получить функцию связи в обобщенной линейной модели, сплайн можно сгладить.
Тогда потребуется соединить N сумматоров. К тому же сложность решения такой задачи выполнимости может сильно возрасти. В первоначальном варианте КНФ имеет простую структуру, и методу типа резолюций будет легче справиться с этой задачей.
Хорошие идеи, но данные по выгоранию слегка не открытые. Вот если попытаться применить этот же метод, например, к данным MNIST (рукописные цифры), то интересно, какая получится точность.
Спасибо за комментарий. Из книги "Professional burnout: recent developments in theory and research" (1993): According to Maslach (1982a), "burnout is a syndrome of emotional exhaustion, depersonalization, and reduced personal accomplishment that can occur among individuals who do 'people work' of some kind" (p. 3). According to Pines and Aronson (1988), burnout is "a state of physical, emotional and mental exhaustion caused by long term involvement in situations that are emotionally demanding" (p. 9). According to Freudenberger and Richelson, this process is caused by failure to produce an expected and desired goal. Вообще выгорание является многомерной характеристикой.
Есть многомерные данные. Признаки непрерывные. Можно построить логистическую регрессию для предсказания выходного признака. Но чтобы объяснить, почему модель сработала на данных именно так, производят дихотомизацию признаков. И теперь задача - выбрать пороги и веса так, чтобы точность модели была как можно выше. Здесь решается подзадача выбора пороговой области и фильтрующего свойства в этой области. Потому что, обозначив это свойство за новый бинарный признак и прибавив этот признак с весом, мы добьемся того, что решающая функция увеличится, и модель изменит предсказание с 0 на 1.
Это пример простой левой списочной рекурсии. Запятая - операция продолжения списка. Штрих создает дамми-переменную такого же типа, которая распространяется только на текущий оператор. "Имя функции от выражения" транслируется в if, в котором проверяется равенство этого выражения и входного аргумента.
Простая правая списочная рекурсия:
def sum (a: Seq<Num>) -> Num:
sum([x a']) = x + sum(a')
sum([]) = 0
Насколько актуальной может явиться возможность поуровневого переопределения всех операций, используемых в разных фрагментах кода? В этом примере это относится к оператору, который сводит задачу к такой же подзадаче. В коде как бы неявно вводится соотношение
f(x) = f(x // base) + [x % base] при x > 0 и f(x) = [] при x = 0.
По умолчанию этот код будет транслироваться и выполняться так, как он написан.
Но если сказать, как будет выполняться + и в каком виде будут храниться данные - то могут быть разные варианты. Для этого потребуется переопределить во обрамляющем блоке способ работы со списком.
Можно заметить, что вычисление сведется к подстановкам
f(12345) =
= f(1234) + [5] =
= (f(123) + [4]) + [5] =
= ((f(12) + [3]) + [4]) + [5] =
= (((f(1) + [2]) + [3]) + [4]) + [5] =
= ((((f(0) + [1]) + [2]) + [3]) + [4]) + [5] =
= (((([] + [1]) + [2]) + [3]) + [4]) + [5] =
= ((([1] + [2]) + [3]) + [4]) + [5] =
= (([1, 2] + [3]) + [4]) + [5] =
= ([1, 2, 3] + [4]) + [5] =
= [1, 2, 3, 4] + [5] =
= [1, 2, 3, 4, 5],
и чтобы транслятор сделал это лучше с точки зрения использования памяти, ему можно сообщить, где будут храниться списки.
Сделать это можно так ($ - от слова storage - указание на способ хранения данных):
def convert(x: Num) -> a: Seq<Num> = {
def f(x: Num) -> a: Seq<Num> = {
$a = reverse_array() # массив, который растет влево
if x == 0:
return []
else:
return f(x // base) + [x % base]
}
y = f(x)
return y if y else [0]
}
С точки зрения реализации на машине Тьюринга, всякий раз при выполнении строки 7 интерпретатор находится в одном и том же состоянии, и результатом выполнения этой строки будет "сдвиг каретки".
Приколов может быть сколько угодно. Допустим, идея в том, чтобы язык выглядел как императивный, но интерпретировался подобно функциональному. То есть в этом примере - строка с рекурсией - надо, чтобы к этому коду программист дописывал, как эта рекурсия должна выполняться - как рекурсия или всё-таки как цикл.
В структуру данных дизъюнкты добавляются и удаляются. Число в таблице - это максимальный объем структуры данных, который был в ходе итераций. Например, в логе это 28434.
Число >86000 клауз - это сколько дизъюнктов в структуре данных. В самом тесте 840 дизъюнктов от 225 переменных. Дальше метод резолюций выводит новые дизъюнкты, исключая переменные и пополняя базу дизъюнктов. Одни дизъюнкты (с очередной переменной) удаляются, а их попарные резольвенты добавляются.
В качестве примера работы могу только привести, сколько дизъюнктов в базе на каждой итерации.
Лог вывода
Здесь Counter(...) - это статистика по длинам дизъюнктов.
pos .., neg ... - это сколько дизъюнктов попарно резольвируется (pos - дизъюнкты с очередной переменной, neg - с отрицанием переменной)
Пример теста - pigeonhole. До середины итераций число дизъюнктов растет, дальше уменьшается.
Спасибо за полезный ответ! Действительно, алгоритм очень похож на DP, но вместо эвристик "Unit-literal rule" и "Pure-literal rule" поддерживается структура данных, сразу исключающая все возможные поглощения клауз. За счет этого количество клауз в множестве становится меньше.
Данная задача возникла на таком примере. С помощью численных методов рассчитывалась зависимость температуры двух тепловых источников от их мощности. В результате получилась зависимость, похожая на линейную. Точнее, линии уровня на координатной плоскости были почти прямыми линиями, но не равноотстоящими. В связи с этим возникла идея: как оценить аналитически такую зависимость. Если наклон изолиний заранее неизвестен, а также неизвестна функция связи.
В примере f = sqrt(z), то есть это может быть любая функция.
Сплайны здесь используются скорее для оценки плавности зависимости, т.е. для расчета целевой функции. Чтобы получить функцию связи в обобщенной линейной модели, сплайн можно сгладить.
Имеет смысл сравнить экспериментально эти два подхода. В сумматоре фигурирует конъюнкция входов, что может усложнить КНФ.
Тогда потребуется соединить N сумматоров. К тому же сложность решения такой задачи выполнимости может сильно возрасти. В первоначальном варианте КНФ имеет простую структуру, и методу типа резолюций будет легче справиться с этой задачей.
Тогда длина КНФ будет порядка
.
Хорошие идеи, но данные по выгоранию слегка не открытые. Вот если попытаться применить этот же метод, например, к данным MNIST (рукописные цифры), то интересно, какая получится точность.
Вот черновик. Фолдов 5.
Спасибо за комментарий. Из книги "Professional burnout: recent developments in theory and research" (1993):
According to Maslach (1982a), "burnout is a syndrome of emotional exhaustion, depersonalization, and reduced personal accomplishment that can occur among individuals who do 'people work' of some kind" (p. 3). According to Pines and Aronson (1988), burnout is "a state of physical, emotional and mental exhaustion caused by long term involvement in situations that are emotionally demanding" (p. 9). According to Freudenberger and Richelson, this process is caused by failure to produce an expected and desired goal.
Вообще выгорание является многомерной характеристикой.
Есть многомерные данные. Признаки непрерывные. Можно построить логистическую регрессию для предсказания выходного признака. Но чтобы объяснить, почему модель сработала на данных именно так, производят дихотомизацию признаков. И теперь задача - выбрать пороги и веса так, чтобы точность модели была как можно выше. Здесь решается подзадача выбора пороговой области и фильтрующего свойства в этой области. Потому что, обозначив это свойство за новый бинарный признак и прибавив этот признак с весом, мы добьемся того, что решающая функция увеличится, и модель изменит предсказание с 0 на 1.
Полагаю, что easy - это за O(n^3), наивным алгоритмом.
Почему бы нет, если задача возникла в приложении? Есть ссылка на аналогичную задачу?
@ - спецификатор, который указывает на возможность изменить значение переменной, переданной по ссылке.
Еще пример:
Вас понял. Тогда буду постепенно формулировать спецификацию, исходя из примеров.
Это пример простой левой списочной рекурсии. Запятая - операция продолжения списка. Штрих создает дамми-переменную такого же типа, которая распространяется только на текущий оператор. "Имя функции от выражения" транслируется в if, в котором проверяется равенство этого выражения и входного аргумента.
Простая правая списочная рекурсия:
Стандартные операторы:
Может быть, для более сложных случаев потребуется явное указание для транслятора.
Насколько актуальной может явиться возможность поуровневого переопределения всех операций, используемых в разных фрагментах кода? В этом примере это относится к оператору, который сводит задачу к такой же подзадаче. В коде как бы неявно вводится соотношение
f(x) = f(x // base) + [x % base] при x > 0 и f(x) = [] при x = 0.
По умолчанию этот код будет транслироваться и выполняться так, как он написан.
Но если сказать, как будет выполняться + и в каком виде будут храниться данные - то могут быть разные варианты. Для этого потребуется переопределить во обрамляющем блоке способ работы со списком.
Можно заметить, что вычисление сведется к подстановкам
f(12345) =
= f(1234) + [5] =
= (f(123) + [4]) + [5] =
= ((f(12) + [3]) + [4]) + [5] =
= (((f(1) + [2]) + [3]) + [4]) + [5] =
= ((((f(0) + [1]) + [2]) + [3]) + [4]) + [5] =
= (((([] + [1]) + [2]) + [3]) + [4]) + [5] =
= ((([1] + [2]) + [3]) + [4]) + [5] =
= (([1, 2] + [3]) + [4]) + [5] =
= ([1, 2, 3] + [4]) + [5] =
= [1, 2, 3, 4] + [5] =
= [1, 2, 3, 4, 5],
и чтобы транслятор сделал это лучше с точки зрения использования памяти, ему можно сообщить, где будут храниться списки.
Сделать это можно так ($ - от слова storage - указание на способ хранения данных):
С точки зрения реализации на машине Тьюринга, всякий раз при выполнении строки 7 интерпретатор находится в одном и том же состоянии, и результатом выполнения этой строки будет "сдвиг каретки".
Приколов может быть сколько угодно. Допустим, идея в том, чтобы язык выглядел как императивный, но интерпретировался подобно функциональному. То есть в этом примере - строка с рекурсией - надо, чтобы к этому коду программист дописывал, как эта рекурсия должна выполняться - как рекурсия или всё-таки как цикл.