16+
Суббота
25 января
Вход |Карта сайта |Upload |codebook | PARTS

 О смысле всего сущего 0xFF

 Средства и методы разработки

 Мобильная и беспроводная связь

 Блошиный рынок Объявления

caxapa

Микроконтроллеры ARM 

AVR PIC MSP PLD,FPGA,DSP 

Кибернетика Технологии 

Схемы, платы, компоненты 

Средства и методы разработки

 
Новая темаПравила РегистрацияСтатистика Архив
Вернуться в конференциюТопик полностью
Evgeny_CD, Архитектор  (02.06.2018 02:26 - 02.06.2018 02:29, файл(ы), ссылка, ссылка, просмотров: 632)
[Satisfiability modulo theories, SMT, задача выполнимости формул в теориях] Мощнейший математический аппарат для формальной верификации ПО (в том числе). 
Есть классическая Зада́ча выполни́мости бу́левых фо́рмул (SAT) -> Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций. Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. В SMP народ расширил теорию до небулевых формул, чем сильно повысил компактность описания реальных задач. Также создана целая куча решателей этих формул и способы формального описания формул.
Прикреплённые файлы:
0086.pdf:249 K
01e1bfaa7f0d6949c4d2e6ace1d8428d6b84.pdf:481 K
10.1.1.367.9961.pdf:416 K
BarTin-14.pdf:278 K
CDSATpaper.pdf:527 K
Oliveras.pdf:338 K
SMT-BookChapter.pdf:723 K
dissertation_tino_teige_2012_09_21.pdf:3454 K
facj08.pdf:150 K
jovanovic.pdf:1977 K
nbjorner-bmr-smt.pdf:173 K
oregon08.pdf:811 K
smacc_thesis_TUTORIAL.pdf:1046 K
smt.pdf:177 K

Главная | Карта сайта | О проекте | Проекты | Файлообменник | Регистрация | Вебмастер | RSS
Лето 7528 от сотворения мира. При использовании материалов сайта ссылка на caxapу обязательна.
MMI © MMXX