我编写了以下 Perl 脚本来生成 smt2 格式的逻辑约束，以解决给定输入文件的数独难题。输入文件格式如下：
5 3 * * 7 * * * *
6 * * 1 9 5 * * *
* 9 8 * * * * 6 *
8 * * * 6 * * * 3
4 * * 8 * 3 * * 1
7 * * * 2 * * * 6
* 6 * * * * 2 8 *
* * * 4 1 9 * * 5
* * * * 8 * * 7 9
又大又丑的 Perl 脚本是：
#! /usr/local/bin/perl
# CSC 410 A2 Q2
# Sudoku
use strict;
use warnings;
# All of the indices in a sudoku array
my @row1 = qw(r1c1 r1c2 r1c3 r1c4 r1c5 r1c6 r1c7 r1c8 r1c9);
my @row2 = qw(r2c1 r2c2 r2c3 r2c4 r2c5 r2c6 r2c7 r2c8 r2c9);
my @row3 = qw(r3c1 r3c2 r3c3 r3c4 r3c5 r3c6 r3c7 r3c8 r3c9);
my @row4 = qw(r4c1 r4c2 r4c3 r4c4 r4c5 r4c6 r4c7 r4c8 r4c9);
my @row5 = qw(r5c1 r5c2 r5c3 r5c4 r5c5 r5c6 r5c7 r5c8 r5c9);
my @row6 = qw(r6c1 r6c2 r6c3 r6c4 r6c5 r6c6 r6c7 r6c8 r6c9);
my @row7 = qw(r7c1 r7c2 r7c3 r7c4 r7c5 r7c6 r7c7 r7c8 r7c9);
my @row8 = qw(r8c1 r8c2 r8c3 r8c4 r8c5 r8c6 r8c7 r8c8 r8c9);
my @row9 = qw(r9c1 r9c2 r9c3 r9c4 r9c5 r9c6 r9c7 r9c8 r9c9);
my @rows = (\@row1, \@row2, \@row3, \@row4, \@row5, \@row6, \@row7, \@row8, \@row9);
# All of the indices in a sudoku block
my @block1 = qw(r1c1 r1c2 r1c3 r2c1 r2c2 r2c3 r3c1 r3c2 r3c3);
my @block2 = qw(r1c4 r1c5 r1c6 r2c4 r2c5 r2c6 r3c4 r3c5 r3c6);
my @block3 = qw(r1c7 r1c8 r1c9 r2c7 r2c8 r2c9 r3c7 r3c8 r3c9);
my @block4 = qw(r4c1 r4c2 r4c3 r5c1 r5c2 r5c3 r6c1 r6c2 r6c3);
my @block5 = qw(r4c4 r4c5 r4c6 r5c4 r5c5 r5c6 r6c4 r6c5 r6c6);
my @block6 = qw(r4c7 r4c8 r4c9 r5c7 r5c8 r5c9 r6c7 r6c8 r6c9);
my @block7 = qw(r7c1 r7c2 r7c3 r8c1 r8c2 r8c3 r9c1 r9c2 r9c3);
my @block8 = qw(r7c4 r7c5 r7c6 r8c4 r8c5 r8c6 r9c4 r9c5 r9c6);
my @block9 = qw(r7c7 r7c8 r7c9 r8c7 r8c8 r8c9 r9c7 r9c8 r9c9);
my @blocks = (\@block1, \@block2, \@block3, \@block4, \@block5, \@block6, \@block7, \@block8, \@block9);
open (FORMULA, ">", "sudoku.smt2") or die $!;
my $var;
my $i;
my $r;
my $c;
print (FORMULA "; Declare integers constants.\n");
for ($r = 0; $r < 9; $r++)
{
for ($c = 0; $c < 9; $c++)
{
print (FORMULA "(declare-const $rows[$r][$c] Int)\n");
}
}
print (FORMULA "\n");
print (FORMULA "; Assert for each variable r_ic_j that 1 <= r_ic_j <= 9\n");
for ($r = 0; $r < 9; $r++)
{
for ($c = 0; $c < 9; $c++)
{
print (FORMULA "(assert (not (and (not ($rows[$r][$c] = 1)) (not ($rows[$r][$c] = 2)) (not ($rows[$r][$c] = 3)) (not ($rows[$r][$c] = 4)) (not ($rows[$r][$c] = 5)) (not ($rows[$r][$c] = 6)) (not ($rows[$r][$c] = 7)) (not ($rows[$r][$c] = 8)) (not ($rows[$r][$c] = 9)))))\n");
}
}
print (FORMULA "\n");
print (FORMULA "; Assert that each row and column contains a number only once.\n");
for ($r = 0; $r < 9; $r++)
{
for ($c = 0; $c < 9; $c++)
{
$var = $rows[$r][$c];
for ($i = 0; $i < 9; $i++)
{
if ($var ne $rows[$r][$i])
{
print (FORMULA "(assert (not (= $var $rows[$r][$i])))\n");
}
}
for ($i = 0; $i < 9; $i++)
{
if ($var ne $rows[$i][$c])
{
print (FORMULA "(assert (not (= $var $rows[$i][$c])))\n");
}
}
}
}
print (FORMULA "\n");
print (FORMULA "; Assert that each number appears only once in each block.\n");
for ($r = 0; $r < 9; $r++)
{
for ($c = 0; $c < 9; $c++)
{
$var = $blocks[$r][$c];
for ($i = 0; $i < 9; $i++)
{
if ($var ne $blocks[$r][$i])
{
print (FORMULA "(assert (not (= $var $blocks[$r][$i])))\n");
}
}
}
}
print (FORMULA "\n");
print (FORMULA "; Declare input constants\n");
open (INPUT, "<", $ARGV[0]) or die $!;
my @lines;
my $line_num = 0;
while (@lines = split(/ /, <INPUT>))
{
for ($i = 0; $i <= $#lines; $i++)
{
chomp($lines[$i]);
if ($lines[$i] ne "*")
{
print (FORMULA "(assert (= $rows[$line_num][$i] $lines[$i]))\n");
}
}
$line_num++;
}
print (FORMULA "\n");
print (FORMULA "(check-sat)\n");
print (FORMULA "(get-model)\n");
close (FORMULA);
exit;
导致段错误的脚本部分是：
print (FORMULA "; Assert for each variable r_ic_j that 1 <= r_ic_j <= 9\n");
for ($r = 0; $r < 9; $r++)
{
for ($c = 0; $c < 9; $c++)
{
print (FORMULA "(assert (not (and (not ($rows[$r][$c] = 1)) (not ($rows[$r][$c] = 2)) (not ($rows[$r][$c] = 3)) (not ($rows[$r][$c] = 4)) (not ($rows[$r][$c] = 5)) (not ($rows[$r][$c] = 6)) (not ($rows[$r][$c] = 7)) (not ($rows[$r][$c] = 8)) (not ($rows[$r][$c] = 9)))))\n");
}
}
但是这个片段只是打印出这样的东西：
(assert (not (and (not (x = 1)) (not (x = 2)) (not (x = 3)) ... (not (x = 9)))))
这在逻辑上应该等同于：
(assert (or (= x 1) (= x 2) (= x 3) ... (= x 9)))
任何建议表示赞赏。
问候。