Strips.c
Jump to navigation
Jump to search
/* Blocks world */
/* This program takes the Blocks World described in a 2019 exam
question for Artificial Intelligence and formulates its planning
problem as a SAT instance, outputting it in the standard DIMACS format
used by SAT solvers. It invokes minisat to find a solution, then
interprets the solution to print a sequence of moves. */
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include <string.h>
/* panic -- halt with a message */
void panic(char *fmt, ...) {
va_list va;
fprintf(stderr, "Panic: ");
va_start(va, fmt);
vfprintf(stderr, fmt, va);
va_end(va);
fprintf(stderr, "\n");
exit(2);
}
// SAT-SOLVER INTERFACE
#define MAX 100 /* Max number of literals in a clause */
#define MAXVARS 10000 /* Max number of variables */
#define BIGMAX 1000000 /* Max number of clauses */
int nvars = 0;
char *vname[MAXVARS]; /* Table mapping var numbers to names */
/* make_var -- create a named variable and return its index */
int make_var(char *fmt, ...) {
char buf[32];
int v;
va_list va;
va_start(va, fmt);
vsprintf(buf, fmt, va);
va_end(va);
v = ++nvars;
vname[v] = strdup(buf);
return v;
}
FILE *script; /* File for outputting the SAT instance */
/* Add a comment to the SAT instance */
void comment(char *fmt, ...) {
va_list va;
fprintf(script, "c ");
va_start(va, fmt);
vfprintf(script, fmt, va);
va_end(va);
fprintf(script, "\n");
}
/* The fussy input format of sat solvers requires us to store all the
clauses just in order to count them and put the count at the top of
the file. To help with troubleshooting, the file contains first
all the clauses in a human-readable format, then the same
information formatted for the SAT solver, where the variables are
coded as bare numbers. */
int nclauses = 0; /* Number of clauses */
int *clauses[BIGMAX]; /* The clauses themselves */
/* add_clause -- add a clause to the SAT instance */
void add_clause(int n, int a[]) {
int *buf;
fprintf(script, "c");
for (int i = 0; i < n; i++) {
if (a[i] > 0)
fprintf(script, " %s", vname[a[i]]);
else
fprintf(script, " -%s", vname[-a[i]]);
}
fprintf(script, "\n");
if (nclauses >= BIGMAX) panic("Too many clauses");
buf = (int *) calloc(n+1, sizeof(int));
for (int i = 0; i < n; i++) buf[i] = a[i];
buf[n] = 0;
clauses[nclauses++] = buf;
}
/* dump -- output saved clauses in numeric form */
void dump(void) {
fprintf(script, "p cnf %d %d\n", nvars, nclauses);
for (int i = 0; i < nclauses; i++) {
for (int j = 0; clauses[i][j] != 0; j++)
fprintf(script, "%d ", clauses[i][j]);
fprintf(script, "0\n");
}
}
/* clause -- convenient varargs version of add_clause */
void clause(int n, ...) {
int buf[100];
va_list va;
va_start(va, n);
for (int i = 0; i < n; i++)
buf[i] = va_arg(va, int);
va_end(va);
add_clause(n, buf);
}
/* set -- unit clause, positive or negative */
void set(int x) {
clause(1, x);
}
/* implies -- implication clause */
void implies(int x, int y) {
clause(2, -x, y);
}
/* impl_equiv -- clauses for A => (B <=> C) */
void impl_equiv(int x, int y, int z) {
clause(3, -x, -y, z);
clause(3, -x, y, -z);
}
/* one_of -- clauses that say exactly one of a[0] ... a[n] is true */
void one_of(int n, int a[]) {
add_clause(n, a);
for (int i = 0; i < n; i++) {
for (int j = i+1; j < n; j++) {
clause(2, -a[i], -a[j]);
}
}
}
// VARIABLES FOR THE STRIPS PROBLEM
#define TIME 3 /* Number of moves */
#define NBLOCKS 3
#define A 0 /* Genuine blocks */
#define B 1
#define C 2
#define T 3 /* The table */
#define isblock(x) ((x) < NBLOCKS)
#define for_blocks(b) for (int b = 0; b < NBLOCKS; b++)
#define for_places(b) for (int b = 0; b <= NBLOCKS; b++)
char *place[] = {
"A", "B", "C", "T"
};
/* Variables:
clear[x][t] if block x is clear at time t (the table is
always able to fit another block);
on[x][y][t] if block x is on place y (could be the table) at time t;
move[x][y][z][t] if block x moves from place y to place z at time t. */
int clear[NBLOCKS+1][TIME+1];
int on[NBLOCKS][NBLOCKS+1][TIME+1];
int move[NBLOCKS][NBLOCKS+1][NBLOCKS+1][TIME];
/* create_vars -- create the variables for Blocks World */
void create_vars(void) {
vname[0] = "?OOPS?";
for (int t = 0; t <= TIME; t++) {
for_blocks (x) {
clear[x][t] = make_var("Clear%s%d", place[x], t);
for_places (y) {
if (x == y) continue;
on[x][y][t] = make_var("On%s%s%d", place[x], place[y], t);
for_places (z) {
if (x == z || y == z || t == TIME) continue;
move[x][y][z][t] =
make_var("Move%s%s%s%d", place[x], place[y],
place[z], t);
}
}
}
}
}
// CLAUSES FOR THE STRIPS PROBLEM
/* init_state -- clauses for the initial state */
void init_state(void) {
comment("Initial state");
set(on[A][T][0]); set(-on[A][B][0]); set(-on[A][C][0]);
set(on[B][T][0]); set(-on[B][A][0]); set(-on[B][C][0]);
set(on[C][A][0]); set(-on[C][B][0]); set(-on[C][T][0]);
set(-clear[A][0]); set(clear[B][0]); set(clear[C][0]);
}
/* goal_state -- clauses for the goal state */
void goal_state(void) {
comment("Goal state");
set(on[A][B][TIME]);
set(on[B][C][TIME]);
set(on[C][T][TIME]);
}
/* steps -- clauses to say one action per unit time */
void steps(void) {
int buf[100];
for (int t = 0; t < TIME; t++) {
int k = 0;
for_blocks (x) {
for_places (y) {
for_places (z) {
if (x == y || y == z || z == x) continue;
buf[k++] = move[x][y][z][t];
}
}
}
comment("Exactly one move at time %d", t);
one_of(k, buf);
}
}
/* moves -- clauses describing pre and post conditions for each move */
void moves(void) {
for (int t = 0; t < TIME; t++) {
for_blocks (x) {
for_places (y) {
for_places (z) {
if (x == y || y == z || z == x) continue;
comment("Move(%s, %s, %s) at time %d",
place[x], place[y], place[z], t);
// Precondition
implies(move[x][y][z][t], clear[x][t]);
implies(move[x][y][z][t], on[x][y][t]);
if (isblock(z))
implies(move[x][y][z][t], clear[z][t]);
// Postcondition
implies(move[x][y][z][t], on[x][z][t+1]);
implies(move[x][y][z][t], clear[x][t+1]);
if (isblock(y))
implies(move[x][y][z][t], clear[y][t+1]);
if (isblock(z))
implies(move[x][y][z][t], -clear[z][t+1]);
// x is not on anything but z
for (int a = 0; a <= NBLOCKS; a++) {
if (a == x || a == z) continue;
implies(move[x][y][z][t], -on[x][a][t+1]);
}
// Other blocks are on what they were before
for (int a = 0; a < NBLOCKS; a++) {
for (int b = 0; b <= NBLOCKS; b++) {
if (a == x || a == b) continue;
impl_equiv(move[x][y][z][t],
on[a][b][t+1], on[a][b][t]);
}
}
// Any other block is clear iff it was before
for (int a = 0; a < NBLOCKS; a++) {
if (a == x || a == y || a == z) continue;
impl_equiv(move[x][y][z][t],
clear[a][t+1], clear[a][t]);
}
}
}
}
}
}
// read_results -- read back satisfying assignment
void read_results(FILE *fp) {
int n, k = 0;
char buf[32], *vn;
fgets(buf, 32, fp);
if (strcmp(buf, "SAT\n") != 0) panic("IMPOSSIBLE");
for (;;) {
fscanf(fp, "%d", &n);
if (n == 0) break;
if (n < 0) continue;
vn = vname[n];
if (strncmp(vn, "Move", 4) == 0) {
char block = vn[4], from = vn[5], to = vn[6], time = vn[7];
printf("Step %c: move %c from %c to %c\n",
time+1, block, from, to);
}
}
}
int main(void) {
FILE *solution;
// Create the SAT instance
script = fopen("clauses", "w");
if (script == NULL) panic("Can't write script");
create_vars();
init_state();
goal_state();
steps();
moves();
dump();
fclose(script);
printf("%d variables, %d clauses\n", nvars, nclauses);
// Invoke minisat
system("minisat clauses solution >trace 2>&1");
// Read back the solution
solution = fopen("solution", "r");
if (solution == NULL) panic("Can't read solution");
read_results(solution);
fclose(solution);
return 0;
}