[問題] Updating by SAT???
跑cirfraig的時候，ref最後面都會有一行Updating by SAT... Total #FEC Group = 0
我原本以為是把SAT的pattern蒐集起來，再simulate一遍，但結果跟我想的不一樣？譬如
說：
(my.aag)
aag 9 2 0 2 2
2
4
6
8
6 3 5
8 7 2
(my.pattern)
11
(執行結果)
fraig> cirr my.aag
fraig> cirsim -f my.pattern
Total #FEC Group = 1
1 patterns simulated.
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0000_0000_0000_0000_0000_0000_0001 =
==================================================
fraig> cirfraig
Proving (3, !4)...SAT!!
Updating by SAT... Total #FEC Group = 0
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0001_0001_1000_0100_1101_0010_0000 =
==================================================
fraig> q -f
fraig之後cirg 1的value應該是從SatSolver::getValue()得到的吧？但是getValue()
一次只能拿到一個bit吧？不知新的simulation pattern是用什麼神奇的方法得到的？
或是我其他地方理解有誤？
--
昔我愛泉石 長揖離公卿 結屋青山下 咫尺蓬與瀛
至人不可見 世塵忽相攖 業風吹浩劫 蝸角爭浮名
偶逢大呂公 如有夙世盟 相從語寥廓 俯仰萬慮輕
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.241.234
推
01/12 22:04, , 1F
01/12 22:04, 1F
→
01/12 22:38, , 2F
01/12 22:38, 2F
推
01/12 22:57, , 3F
01/12 22:57, 3F
→
01/12 22:58, , 4F
01/12 22:58, 4F
→
01/12 22:58, , 5F
01/12 22:58, 5F
→
01/12 23:06, , 6F
01/12 23:06, 6F