fzn2smt 求解器在测试公式中以“未知”作为答案
fzn2smt solver answers with `unknown` on tested formulas
fzn2smt 工具允许通过 Yices.
求解 flatzinc 公式
当我尝试 运行 时,求解器会用 UNKNOWN
回答我测试的每个公式。 例如:
~$ java -Xmx4096M fzn2smt -ce "./yices-2.5.2/bin/yices -f" -i 2DPacking.fzn
Time1:170
=====UNKNOWN=====
但是,在给定的示例中,它似乎在 2DPacking.fzn
文件的同一目录中正确地创建了 2DPacking.fzn.smt
实例:
~$ ls
2DPacking.fzn.smt 2DPacking.fzn 2DPacking.mzn 2DPacking.ozn
如果我在 smt
公式上手动 运行 Yices
,我会得到一个肯定的结果:
~$ yices-smt -f 2DPacking.fzn.smt
sat
(= x____00002_6_ 0)
...
IMPLICANT:
(>= x____00003_4_ 0)
...
问:有没有其他人有过 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}
正如 @Dekker 在评论中所建议的那样,问题是由于 fzn2smt
似乎有一段时间没有更新了。
经过反复试验,我发现似乎与 fzn2smt
兼容的 Yices
的最新版本是版本 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
最初,fzn2smt
与在 SMT-COMP 2009 上展示的 Yices
版本 2
相结合。要使用该版本,使用该工具的命令行指令略有不同:
~$ 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
输出略有不同,由于某些原因,在使用较新版本的工具时多次打印解决方案
旧版本的 Yices
可以从 here 下载。
fzn2smt 工具允许通过 Yices.
求解 flatzinc 公式 当我尝试 运行 时,求解器会用 UNKNOWN
回答我测试的每个公式。 例如:
~$ java -Xmx4096M fzn2smt -ce "./yices-2.5.2/bin/yices -f" -i 2DPacking.fzn
Time1:170
=====UNKNOWN=====
但是,在给定的示例中,它似乎在 2DPacking.fzn
文件的同一目录中正确地创建了 2DPacking.fzn.smt
实例:
~$ ls
2DPacking.fzn.smt 2DPacking.fzn 2DPacking.mzn 2DPacking.ozn
如果我在 smt
公式上手动 运行 Yices
,我会得到一个肯定的结果:
~$ yices-smt -f 2DPacking.fzn.smt
sat
(= x____00002_6_ 0)
...
IMPLICANT:
(>= x____00003_4_ 0)
...
问:有没有其他人有过 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}
正如 @Dekker 在评论中所建议的那样,问题是由于 fzn2smt
似乎有一段时间没有更新了。
经过反复试验,我发现似乎与 fzn2smt
兼容的 Yices
的最新版本是版本 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
最初,fzn2smt
与在 SMT-COMP 2009 上展示的 Yices
版本 2
相结合。要使用该版本,使用该工具的命令行指令略有不同:
~$ 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
输出略有不同,由于某些原因,在使用较新版本的工具时多次打印解决方案
旧版本的 Yices
可以从 here 下载。