sat

    0熱度

    1回答

    Z3解算器拋出'模型不可用'python 3上的異常3

    爲了解決SAT問題，我決定使用Microsoft和Python 3的Z3解算器。目標是獲取長模型（多達500,000個特徵）並找到所有可能的解決方案。要找到它們，我想將第一個解S1添加到初始方程中，並排除S1等等。我會用while循環來做。 解決SAT問題對我來說很重要，因爲我想分析特徵模型。 但是我面臨着在初始方程中增加某些問題。我將分享一個最小的例子： # Import statements
    z3 python-3.5 z3py sat 2016-09-14

    0熱度

    1回答

    問題，而使用Z3 <smt2-file > CC_NUM_THREADS = 3

    問題，而使用Z3 CC_NUM_THREADS配置並行Z3配置並行Z3 = 3 我試圖運行Z3水貨版本與CC_NUM_THREADS我SMT2文件 以下錯誤= 3坡平向上。 ERROR: unknown parameter 'cc_num_threads' Legal parameters are: auto_config (bool) (default: true) debug_ref_c
    python z3 z3py sat 2016-11-04

    0熱度

    1回答

    將Java對象映射到Prolog表示

    在java中，我有一組相互連接的對象。讓我們假設他們在一起模型，讓我們這樣稱呼它。 我想根據某些規範（定義爲一組條件）驗證該模型。條件可以是這樣的： forall child in parent.children child.name startswith "A" 可以有一堆這樣的條件，他們都必須按順序說一個模型符合規範得到滿足。所有這些條件都是一些由變量和邏輯表達式組成的謂詞，我想
    java prolog sat 2016-06-08

    1熱度

    1回答

    類布爾到布爾可滿足性[多項式時間減少]第2部分

    我問幾天前，一個關於如何將大學課堂排序問題轉換爲布爾可滿足性問題的問題。 （Class Scheduling to Boolean satisfiability [Polynomial-time reduction]） 我通過@Amit回答誰是非常優雅，易於代碼。 基本上，他的答案是這樣的：他不考慮課程，而是考慮時間間隔。 因此，對於第i個課程，他只是指出了本課程的所有可能的時間間隔。當每個課程至
    algorithm scheduling np-complete np sat 2015-03-19

    0熱度

    1回答

    Z3中的部分分配

    我有一個布爾公式（格式：CNF），它的滿足性我使用Z3 SAT解算器進行檢查。當公式可以滿足時，我有興趣獲得部分作業。我試圖用model.partial=true對一個OR門的簡單公式進行分析，但沒有得到任何部分分配。 你能建議如何做到這一點嗎？除了它是部分的，我對任務沒有任何限制。
    z3 sat 2017-01-02

    2熱度

    1回答

    解析和簡化CNF文件的時間

    我剛開始使用Sat4j庫。你能指導我如何計算解析和簡化給定的CNF輸入所花費的時間。 我已經使用 ISolver solver = SolverFactory.newDefault(); Reader reader = new DimacsReader(solver); IProblem problem = reader.parseInstance(filename.cnf); boolea
    java sat sat4j 2016-08-11

    1熱度

    1回答

    使用命題邏輯求解方程

    我正在尋找關於如何將數學方程式編碼爲cnf-sat形式的想法，以便他們可以通過像MiniSat這樣的開源SAT求解器來解決。 所以，我怎麼轉換是這樣的： 3X + 4Y - Z = 14 -2x - 4Z < = -6 X - 3Y + Z> = 15 成爲可以通過使用SAT求解器求解的命題式。 任何建議，因爲我很難過？
    logic smt bitvector sat sat-solvers 2015-12-08

    1熱度

    1回答

    將不可滿足的約束集合轉換爲可滿足的較小約束集合

    我在我的腦海中有一個項目，我很好奇之前是否做過類似的事情。假設有一組不同的約束條件，並且這些約束條件不能一起滿足。 C = {C1，C2，C3，...，CN} （c1和c2和c3 ... CN）：不符合要求 我的目標是分割該組分爲k集合（可能k非常小），使得每一組約束都可單獨滿足。 基本的解決方案是使用貪婪的方法。約束將被選作第一個約束並標記爲第一組。然後，將選擇第二個，並檢查它是否可用第一個約束
    constraint-programming satisfiability sat 2015-10-20

    0熱度

    2回答

    在特定行中編輯特定單詞

    我知道這已被問了幾次，但我需要一種快速方式在具有不同大小（小文件和大文件）的文件中執行此操作。 我需要在sat（txt）文件中編輯比例因子。這是在第三行中的第一數量： 700 104 1 0 16的Autodesk的AutoCAD 19 ASM 221.0.0.1871 NT 24週二 年08月16 9時02分14秒2016 9.9999999999999995 E-007 1E-010
    c# sat 2016-08-16

    -1熱度

    1回答

    在SMT求解器中爲AES定義替換框

    如何定義一個函數，該函數根據表中的值執行值替換？ static const unsigned char FSb[256] = { 0x63, 0x7C, 0x77, 0x7B, 0xF2, 0x6B, 0x6F, 0xC5, 0x30, 0x01, 0x67, 0x2B, 0xFE, 0xD7, 0xAB, 0x76, 0xCA, 0x82, 0xC9, 0x7D,
    cryptography smt sat 2015-07-22
最新問題