隨機解決方案在Yices求解器

我想在c程序中使用Yices SMT solver來解決表達式x > 100並獲得解決方案x。這裏是我的代碼：隨機解決方案在Yices求解器

#include<stdio.h> 
#include"yices_c.h" 

int main() { 
    yices_context ctx = yices_mk_context(); 
    char int_ty_name[] = "int"; 
    yices_type int_ty = yices_mk_type(ctx, int_ty_name); 
    char vname[] = "x"; 
    yices_expr e1 = yices_mk_num(ctx,100); 
    yices_var_decl v = yices_mk_var_decl(ctx,vname,int_ty); 
    yices_expr e2 = yices_mk_var_from_decl(ctx,v); 
    yices_expr eq1 = yices_mk_lt(ctx, e1, e2); 
    yices_assert(ctx, eq1); 
    yices_dump_context(ctx); 
    switch(yices_check(ctx)) { 
    case l_true: 
    printf("satisfiable\n"); 
    yices_model m = yices_get_model(ctx); 
    long i; 
    yices_get_int_value(m,v,&i); 
    printf("e2 = %d\n", i); 
    yices_display_model(m); 
    break; 
    case l_false: 
    printf("unsatisfiable\n"); 
    break; 
    case l_undef: 
    printf("unknown\n"); 
    break; 
    } 
    yices_del_context(ctx); 
    return 0; 
}

該程序總是結果x =101。 101只是這個表達式的可能結果之一。我希望求解器從所有可能的結果中選擇一個隨機結果（一個從101到MAX_INT的隨機整數）。

我該怎麼辦？

來源

2013-09-01 mrd abd

嘗試使用yices_find_weighted_model(ctx, 1)而不是yices_check(ctx)。

如果你沒有加權限制，yices_find_weighted_model(ctx, 0)應該在語義上等於yices_check(ctx)。但yices_find_weighted_model的第二個參數random允許您使用隨機搜索而不是默認決策過程，如果將其設置爲非零值。檢查documentation。

來源

2013-09-01 11:26:54 nickie

再次返回'101'。 –

如果是這樣，似乎對於你的約束，隨機搜索結果不是非常隨機的。我不認爲你能做什麼;要求SMT解決方案提供所有可能的模型，以便您可以隨意選擇一個模型，這相當多。 – nickie

我不想要所有可能的模型。我想要一個模型，但隨機選擇。例如在程序i的第一次運行中看到'x = 1000'，在運行編號2'x = 201'，運行編號3'x = 234234'，... –

您將首先獲得非隨機結果。然後你可以添加一個隨機增量的隨機約束（X>nonRandomResult+delta或X<nonRandomResult-delta）。

只要不能解決問題，您將不得不改變約束與一個新的三角洲有一半的前值。只要它有一個解決方案，該解決方案將最有可能像該三角洲一樣隨機。

來源

2013-09-30 16:39:36 comonad

隨機解決方案在Yices求解器

回答

相關問題