作者TommyKSHS (湯米)
看板EE_DSnP
標題[問題] 關於 sat solver 的用法
時間Sun Jan 16 17:04:07 2011
我想問的是：
當我們要證一個 fec pair 的時候
應該要 add 一個 XorCNF ( tmp, fec1, fec2 ) ？
然後 assume 這個 tmp 的 Var 是 true 吧？
那如果證完之後
再 assumeRelease
要證下一對 pair 時，上次 add 的 xorCNF 會影響到下一次證明的結果嗎？
--
╭═══╤═══╮ ╰═╮ ╭═╯
│ │ │╭═和平，土地，麵包═╮ │ │
│ ╭═╧╧╮╤═╤═╮═╤═╤╧╮ │ │
│ │ ││ │ │ │ │ │ ╰═╤═╯
│ │ ││ │ │ │ │ │ │
╰╧╯╰═══╯╰ ╰ ╰ ╰ ╰ ╰ ─╯
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.244.6