代码之家 › 专栏 › 技术社区 › Patrick Trentin

fzn2smt求解器在测试公式上回答“未知”

flatzinc minizinc smt

1

Patrick Trentin · 技术社区 · 7 年前

这个 fzn2smt 扁平锌 Yices公司 .

UNKNOWN 例如 :

~$ java -Xmx4096M fzn2smt -ce "./yices-2.5.2/bin/yices -f" -i 2DPacking.fzn 
Time1:170
=====UNKNOWN=====

2DPacking.fzn.smt 实例位于 2DPacking.fzn

~$ ls
2DPacking.fzn.smt    2DPacking.fzn    2DPacking.mzn    2DPacking.ozn

如果我手动运行 Yices 超过 smt

~$ yices-smt -f 2DPacking.fzn.smt 
sat

(= x____00002_6_ 0)
...

IMPLICANT:
(>= x____00003_4_ 0)
...

Q: fzn2smt 知道如何解决这个问题吗?

为了确保我遇到的问题不是由于安装部分引起的,我将在这里分享:

 main_dir
 main_dir/fzn2smt-2-0-02      # unpacked fzn2smt files
 main_dir/antlr               # unpacked antlr-runtime-3.5 files
 main_dir/yices-2.5.2         # unpacked yices files

我还根据工具说明的要求修改了环境变量:

 PATH=${main_dir}/yices-2.5.2/bin/:${PATH}
 PATH=${main_dir}/fzn2smt-2-0-02/:${PATH}

 CLASSPATH=${main_dir}:${CLASSPATH}
 CLASSPATH=${main_dir}/antlr:${CLASSPATH}
 CLASSPATH=${main_dir}/fzn2smt-2-0-02:${CLASSPATH}

1 回复 | 直到 7 年前

1

Patrick Trentin 7 年前

评论中建议,该问题是由于 fzn2smt

经过一些尝试和错误,我发现最新版本的 Yices fzn2smt 2.2.1 .

可以按以下方式执行:

~$ java -Xmx4096M fzn2smt -ce "./yices-2.2.1/bin/yices-smt -f" -i 2DPacking.fzn
Time1:162
Time: 207
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
Time: 223
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
==========
Time2:228

与版本相结合 2 属于 Yices公司 SMT-COMP 2009 . 要使用该版本,使用该工具的命令行指令是 略有不同

~$ java -Xmx4096M fzn2smt -ce "./yices2smt09/bin/yices -f" -i 2DPacking.fzn
Time1:160
Time: 208
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
==========
Time2:223

请注意

可执行文件名为 yices 在这里,而不是 yices-smt
输出略有不同,由于某些原因,在使用较新版本的工具时,解决方案会多次打印

旧版本的 here