Podsumowanie: Nowe podejście, brak nowych rozwiązań , fajny program do zabawy i kilka interesujących rezultatów lokalnej niemożliwości poprawy znanych rozwiązań. Aha, i kilka ogólnie przydatnych obserwacji.
Stosując
podejście oparte na SAT , mogłem całkowicie
rozwiązać
podobny problem dla labiryntów 4x4 z zablokowanymi komórkami zamiast cienkich ścian i ze stałymi pozycjami początkowymi i wyjściowymi w przeciwległych rogach. Miałem więc nadzieję, że uda mi się wykorzystać te same pomysły do rozwiązania tego problemu. Jednakże, chociaż dla drugiego problemu użyłem tylko 2423 labiryntów (w międzyczasie zaobserwowano, że 2083 wystarczy) i ma rozwiązanie o długości 29, kodowanie SAT wykorzystało miliony zmiennych, a jego rozwiązanie zajęło kilka dni.
Postanowiłem więc zmienić podejście na dwa ważne sposoby:
- Nie nalegaj na wyszukiwanie rozwiązania od zera, ale pozwól naprawić część ciągu rozwiązania. (W każdym razie łatwo to zrobić, dodając klauzule jednostki, ale mój program sprawia, że jest to wygodne.)
- Nie używaj wszystkich labiryntów od samego początku. Zamiast tego stopniowo dodawaj jeden nierozwiązany labirynt naraz. Niektóre labirynty mogą być rozwiązane przypadkowo lub zawsze są rozwiązywane, gdy te już rozważone zostaną rozwiązane. W tym drugim przypadku nigdy nie zostanie dodany, bez naszej wiedzy na temat konsekwencji.
Zrobiłem także pewne optymalizacje, aby użyć mniej zmiennych i klauzul jednostkowych.
Program oparty jest na @ orlp's. Ważną zmianą był wybór labiryntów:
- Przede wszystkim labirynty są podawane tylko przez strukturę ściany i pozycję początkową. (Przechowują również pozycje osiągalne.) Funkcja
is_solution
sprawdza, czy wszystkie osiągalne pozycje są osiągnięte.
- (Bez zmian: nadal nie używają labiryntów z tylko 4 lub mniej dostępnymi pozycjami. Ale większość z nich i tak zostanie wyrzucona przez następujące obserwacje).
- Jeśli labirynt nie używa żadnej z trzech górnych komórek, jest to odpowiednik przesuniętego w górę labiryntu. Więc możemy to upuścić. Podobnie w przypadku labiryntu, który nie wykorzystuje żadnej z trzech lewych komórek.
- Nie ma znaczenia, czy nieosiągalne części są połączone, dlatego nalegamy, aby każda nieosiągalna komórka była całkowicie otoczona ścianami.
- Labirynt z pojedynczą ścieżką, który jest submaze większego labiryntu z pojedynczą ścieżką, jest zawsze rozwiązywany, gdy większy jest rozwiązywany, więc nie potrzebujemy go. Każdy labirynt pojedynczej ścieżki o wielkości maksymalnie 7 jest częścią większego (wciąż mieszczącego się w rozmiarze 3 x 3), ale istnieją labirynty o pojedynczej ścieżce wielkości 8, które nie są. Upraszczając, po prostu upuśćmy labirynty z pojedynczą ścieżką o rozmiarze mniejszym niż 8. (I nadal używam tego, że tylko skrajne punkty muszą być uważane za pozycje początkowe. Wszystkie pozycje są używane jako pozycje wyjściowe, co ma znaczenie tylko dla części SAT programu).
W ten sposób otrzymuję 10772 labiryntów z pozycjami początkowymi.
Oto program:
#include <algorithm>
#include <array>
#include <bitset>
#include <cstring>
#include <iostream>
#include <set>
#include <vector>
#include <limits>
#include <cassert>
extern "C"{
#include "lglib.h"
}
// reusing a lot of @orlp's ideas and code
enum { N = -8, W = -2, E = 2, S = 8 };
static const int encoded_pos[] = {8, 10, 12, 16, 18, 20, 24, 26, 28};
static const int wall_idx[] = {9, 11, 12, 14, 16, 17, 19, 20, 22, 24, 25, 27};
static const int move_offsets[] = { N, E, S, W };
static const uint32_t toppos = 1ull << 8 | 1ull << 10 | 1ull << 12;
static const uint32_t leftpos = 1ull << 8 | 1ull << 16 | 1ull << 24;
static const int unencoded_pos[] = {0,0,0,0,0,0,0,0,0,0,1,0,2,0,0,0,3,
0,4,0,5,0,0,0,6,0,7,0,8};
int do_move(uint32_t walls, int pos, int move) {
int idx = pos + move / 2;
return walls & (1ull << idx) ? pos + move : pos;
}
struct Maze {
uint32_t walls, reach;
int start;
Maze(uint32_t walls=0, uint32_t reach=0, int start=0):
walls(walls),reach(reach),start(start) {}
bool is_dummy() const {
return (walls==0);
}
std::size_t size() const{
return std::bitset<32>(reach).count();
}
std::size_t simplicity() const{ // how many potential walls aren't there?
return std::bitset<32>(walls).count();
}
};
bool cmp(const Maze& a, const Maze& b){
auto asz = a.size();
auto bsz = b.size();
if (asz>bsz) return true;
if (asz<bsz) return false;
return a.simplicity()<b.simplicity();
}
uint32_t reachable(uint32_t walls) {
static int fill[9];
uint32_t reached = 0;
uint32_t reached_relevant = 0;
for (int start : encoded_pos){
if ((1ull << start) & reached) continue;
uint32_t reached_component = (1ull << start);
fill[0]=start;
int count=1;
for(int i=0; i<count; ++i)
for(int m : move_offsets) {
int newpos = do_move(walls, fill[i], m);
if (reached_component & (1ull << newpos)) continue;
reached_component |= 1ull << newpos;
fill[count++] = newpos;
}
if (count>1){
if (reached_relevant)
return 0; // more than one nonsingular component
if (!(reached_component & toppos) || !(reached_component & leftpos))
return 0; // equivalent to shifted version
if (std::bitset<32>(reached_component).count() <= 4)
return 0;
reached_relevant = reached_component;
}
reached |= reached_component;
}
return reached_relevant;
}
void enterMazes(uint32_t walls, uint32_t reached, std::vector<Maze>& mazes){
int max_deg = 0;
uint32_t ends = 0;
for (int pos : encoded_pos)
if (reached & (1ull << pos)) {
int deg = 0;
for (int m : move_offsets) {
if (pos != do_move(walls, pos, m))
++deg;
}
if (deg == 1)
ends |= 1ull << pos;
max_deg = std::max(deg, max_deg);
}
uint32_t starts = reached;
if (max_deg == 2){
if (std::bitset<32>(reached).count() <= 7)
return; // small paths are redundant
starts = ends; // need only start at extremal points
}
for (int pos : encoded_pos)
if ( starts & (1ull << pos))
mazes.emplace_back(walls, reached, pos);
}
std::vector<Maze> gen_valid_mazes() {
std::vector<Maze> mazes;
for (int maze_id = 0; maze_id < (1 << 12); maze_id++) {
uint32_t walls = 0;
for (int i = 0; i < 12; ++i)
if (maze_id & (1 << i))
walls |= 1ull << wall_idx[i];
uint32_t reached=reachable(walls);
if (!reached) continue;
enterMazes(walls, reached, mazes);
}
std::sort(mazes.begin(),mazes.end(),cmp);
return mazes;
};
bool is_solution(const std::vector<int>& moves, Maze& maze) {
int pos = maze.start;
uint32_t reached = 1ull << pos;
for (auto move : moves) {
pos = do_move(maze.walls, pos, move);
reached |= 1ull << pos;
if (reached == maze.reach) return true;
}
return false;
}
std::vector<int> str_to_moves(std::string str) {
std::vector<int> moves;
for (auto c : str) {
switch (c) {
case 'N': moves.push_back(N); break;
case 'E': moves.push_back(E); break;
case 'S': moves.push_back(S); break;
case 'W': moves.push_back(W); break;
}
}
return moves;
}
Maze unsolved(const std::vector<int>& moves, std::vector<Maze>& mazes) {
int unsolved_count = 0;
Maze problem{};
for (Maze m : mazes)
if (!is_solution(moves, m))
if(!(unsolved_count++))
problem=m;
if (unsolved_count)
std::cout << "unsolved: " << unsolved_count << "\n";
return problem;
}
LGL * lgl;
constexpr int TRUELIT = std::numeric_limits<int>::max();
constexpr int FALSELIT = -TRUELIT;
int new_var(){
static int next_var = 1;
assert(next_var<TRUELIT);
return next_var++;
}
bool lit_is_true(int lit){
int abslit = lit>0 ? lit : -lit;
bool res = (abslit==TRUELIT) || (lglderef(lgl,abslit)>0);
return lit>0 ? res : !res;
}
void unsat(){
std::cout << "Unsatisfiable!\n";
std::exit(1);
}
void clause(const std::set<int>& lits){
if (lits.find(TRUELIT) != lits.end())
return;
for (int lit : lits)
if (lits.find(-lit) != lits.end())
return;
int found=0;
for (int lit : lits)
if (lit != FALSELIT){
lgladd(lgl, lit);
found=1;
}
lgladd(lgl, 0);
if (!found)
unsat();
}
void at_most_one(const std::set<int>& lits){
if (lits.size()<2)
return;
for(auto it1=lits.cbegin(); it1!=lits.cend(); ++it1){
auto it2=it1;
++it2;
for( ; it2!=lits.cend(); ++it2)
clause( {- *it1, - *it2} );
}
}
/* Usually, lit_op(lits,sgn) creates a new variable which it returns,
and adds clauses that ensure that the variable is equivalent to the
disjunction (if sgn==1) or the conjunction (if sgn==-1) of the literals
in lits. However, if this disjunction or conjunction is constant True
or False or simplifies to a single literal, that is returned without
creating a new variable and without adding clauses. */
int lit_op(std::set<int> lits, int sgn){
if (lits.find(sgn*TRUELIT) != lits.end())
return sgn*TRUELIT;
lits.erase(sgn*FALSELIT);
if (!lits.size())
return sgn*FALSELIT;
if (lits.size()==1)
return *lits.begin();
int res=new_var();
for(int lit : lits)
clause({sgn*res,-sgn*lit});
for(int lit : lits)
lgladd(lgl,sgn*lit);
lgladd(lgl,-sgn*res);
lgladd(lgl,0);
return res;
}
int lit_or(std::set<int> lits){
return lit_op(lits,1);
}
int lit_and(std::set<int> lits){
return lit_op(lits,-1);
}
using A4 = std::array<int,4>;
void add_maze_conditions(Maze m, std::vector<A4> dirs, int len){
int mp[9][2];
int rp[9];
for(int p=0; p<9; ++p)
if((1ull << encoded_pos[p]) & m.reach)
rp[p] = mp[p][0] = encoded_pos[p]==m.start ? TRUELIT : FALSELIT;
int t=0;
for(int i=0; i<len; ++i){
std::set<int> posn {};
for(int p=0; p<9; ++p){
int ep = encoded_pos[p];
if((1ull << ep) & m.reach){
std::set<int> reach_pos {};
for(int d=0; d<4; ++d){
int np = do_move(m.walls, ep, move_offsets[d]);
reach_pos.insert( lit_and({mp[unencoded_pos[np]][t],
dirs[i][d ^ ((np==ep)?0:2)] }));
}
int pl = lit_or(reach_pos);
mp[p][!t] = pl;
rp[p] = lit_or({rp[p], pl});
posn.insert(pl);
}
}
at_most_one(posn);
t=!t;
}
for(int p=0; p<9; ++p)
if((1ull << encoded_pos[p]) & m.reach)
clause({rp[p]});
}
void usage(char* argv0){
std::cout << "usage: " << argv0 <<
" <string>\n where <string> consists of 'N', 'E', 'S', 'W' and '*'.\n" ;
std::exit(2);
}
const std::string nesw{"NESW"};
int main(int argc, char** argv) {
if (argc!=2)
usage(argv[0]);
std::vector<Maze> mazes = gen_valid_mazes();
std::cout << "Mazes with start positions: " << mazes.size() << "\n" ;
lgl = lglinit();
int len = std::strlen(argv[1]);
std::cout << argv[1] << "\n with length " << len << "\n";
std::vector<A4> dirs;
for(int i=0; i<len; ++i){
switch(argv[1][i]){
case 'N':
dirs.emplace_back(A4{TRUELIT,FALSELIT,FALSELIT,FALSELIT});
break;
case 'E':
dirs.emplace_back(A4{FALSELIT,TRUELIT,FALSELIT,FALSELIT});
break;
case 'S':
dirs.emplace_back(A4{FALSELIT,FALSELIT,TRUELIT,FALSELIT});
break;
case 'W':
dirs.emplace_back(A4{FALSELIT,FALSELIT,FALSELIT,TRUELIT});
break;
case '*': {
dirs.emplace_back();
std::generate_n(dirs[i].begin(),4,new_var);
std::set<int> dirs_here { dirs[i].begin(), dirs[i].end() };
at_most_one(dirs_here);
clause(dirs_here);
for(int l : dirs_here)
lglfreeze(lgl,l);
break;
}
default:
usage(argv[0]);
}
}
int maze_nr=0;
for(;;) {
std::cout << "Solving...\n";
int res=lglsat(lgl);
if(res==LGL_UNSATISFIABLE)
unsat();
assert(res==LGL_SATISFIABLE);
std::string sol(len,' ');
for(int i=0; i<len; ++i)
for(int d=0; d<4; ++d)
if (lit_is_true(dirs[i][d])){
sol[i]=nesw[d];
break;
}
std::cout << sol << "\n";
Maze m=unsolved(str_to_moves(sol),mazes);
if (m.is_dummy()){
std::cout << "That solves all!\n";
return 0;
}
std::cout << "Adding maze " << ++maze_nr << ": " <<
m.walls << "/" << m.start <<
" (" << m.size() << "/" << 12-m.simplicity() << ")\n";
add_maze_conditions(m,dirs,len);
}
}
Pierwszy configure.sh
i Solver, a następnie skompilować program ze coś takiego
, gdzie jest ścieżka gdzie resp. są, więc oba mogą być na przykład
. Lub po prostu umieść je w tym samym katalogu i nie używaj opcji i .make
lingeling
g++ -std=c++11 -O3 -I ... -o m3sat m3sat.cc -L ... -llgl
...
lglib.h
liblgl.a
../lingeling-<version>
-I
-L
Program trwa jedną obowiązkową wiersza poleceń argumentu ciąg składający się z N
, E
, S
, W
(dla stałych kierunków) lub *
. Możesz więc wyszukać ogólne rozwiązanie o rozmiarze 78, podając ciąg 78 *
s (w cudzysłowach), lub wyszukaj rozwiązanie, zaczynając NEWS
od NEWS
poprzedzających go tylu, *
ile chcesz , aby wykonać dodatkowe kroki. Jako pierwszy test weź swoje ulubione rozwiązanie i zamień niektóre litery na *
. Szybko znajduje to rozwiązanie dla zaskakująco wysokiej wartości „niektórych”.
Program powie, który labirynt dodaje, opisany przez strukturę ściany i pozycję początkową, a także poda liczbę dostępnych pozycji i ścian. Labirynty są sortowane według tych kryteriów i dodawany jest pierwszy nierozwiązany. Dlatego większość dodanych labiryntów ma (9/4)
, ale czasami pojawiają się również inne.
Wziąłem znane rozwiązanie o długości 79 i dla każdej grupy sąsiadujących 26 liter próbowałem zastąpić je dowolnymi 25 literami. Próbowałem także usunąć 13 liter od początku i od końca i zastąpić je dowolnymi 13 na początku i dowolnymi 12 na końcu i odwrotnie. Niestety wszystko wyszło niezadowalająco. Czy możemy zatem uznać to za wskaźnik, że długość 79 jest optymalna? Nie, podobnie próbowałem ulepszyć rozwiązanie o długości 80 do długości 79, ale to też nie powiodło się.
Wreszcie próbowałem połączyć początek jednego rozwiązania z końcem drugiego, a także z jednym rozwiązaniem przekształconym przez jedną z symetrii. Teraz brakuje mi ciekawych pomysłów, więc postanowiłem pokazać ci, co mam, mimo że nie doprowadziło to do nowych rozwiązań.