Development mirror of Jussi Rintanen’s planner Madagascar https://research.ics.aalto.fi/software/sat/madagascar/
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 

828 lines
21 KiB

/* 2012 (C) Jussi Rintanen */
#define noDECDEBUG
#define noHEURDEBUG
#define noDEBUGDISJ
typedef struct {
int l; /* Will satisfy subgoal l */
int var; /* with variable var (action, conditional effect) */
short t; /* at time point t */
int flaws; /* How many later actions this action disables/affects */
} planstep;
#define MAXPLANSTEPS 1000000
planstep plansteps[MAXPLANSTEPS];
int Nsteps;
#define STACKSIZE 50000
typedef struct _stackel {
int lit;
short t;
short val;
} stackel;
int stackptr;
stackel stack[STACKSIZE];
/* Order the subgoals according to a measure.
0. No measure is used (everything is 0).
1. How early does it have to be true.
TODO: 2. How early, + how constrained.
If two are equally early, choose the one that is more constrained
in the sense that can be TRUE in a smaller number of consecutive
time points. Choosing a highly constrained subgoal leads to failures
sooner.
*/
inline int anyactionapplicable(satinstance sati,int l,int t) {
compactCEstruct *ptr;
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
if(!tvarfalsep(sati,ptr->var,t)) { /* Is it applicable? */
return 1;
}
}
return 0;
}
inline int goallitvalue(satinstance sati,int l,int t0) {
int t,t2;
t = t0;
switch(HEURordmode) {
case 1:
/* How long the goal lit has been true before t. */
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
return t+1;
case 2:
/* How long the goal lit has been true before t. */
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
t2 = t;
/* How much earlier it was last false. */
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2-1;
return (t+1)*200+(t-t2);
case 3:
/* How long the goal lit must have been true before t (check applicability
of actions making it true!) */
t = t-1;
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
return t+1;
case 4:
/* How wide is the gap in which it must be made true? */
/* WARNING: This stops depth-first! */
t = t-1;
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
t2 = t;
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
return t-t2;
case 5:
/* Case 1 with Case 4 as a tie-breaker. */
/* How wide is the gap in which it must be made true? */
t = t-1;
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
t2 = t;
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
return t*1000+t-t2;
case 6:
/* Case 3 with Case 4 as a tie-breaker. */
/* How wide is the gap in which it must be made true? */
t = t-1;
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
t2 = t;
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
return t*1000+t-t2;
default:
return 0;
}
}
void push2goalstack(satinstance sati,int l,int t) {
int v,i;
i = stackptr++;
ASSERT(stackptr < STACKSIZE);
v = goallitvalue(sati,l,t);
/* Insert the literal in the stack. Lowest .val is on top (last). */
/* This means that we have a depth-first traversal: support for
one precondition (or top-level goal) is found first, before
proceeding with another precondition (or top-level goal). */
while(i > 0 && stack[i-1].val < v) {
stack[i].lit = stack[i-1].lit;
stack[i].t = stack[i-1].t;
stack[i].val = stack[i-1].val;
i = i-1;
}
stack[i].lit = l;
stack[i].t = t;
stack[i].val = v;
}
/* Push the constituent literals of a conjunctive goal formula in the stack. */
void push2goalstackCfma(satinstance sati,fma *f,int t) {
fmalist *fs;
switch(f->t) {
case patom: push2goalstack(sati,PLIT(f->a),t); break;
case natom: push2goalstack(sati,NLIT(f->a),t); break;
case conj:
fs = f->juncts;
while(fs != NULL) {
push2goalstackCfma(sati,fs->hd,t);
fs = fs->tl;
}
break;
case TRUE: break;
default:
assert(1==2);
}
}
/* Push a subset of the literals in a general NNF formula which are
sufficient for making the formula true, in the stack.
This is as in the ICAPS'11 submission.
For conjunctions all conjuncts have to be taken.
For disjunctions one of the disjuncts is taken. If at least one of
the disjuncts is true or unknown, then the chosen disjunct cannot
be a false one.
*/
/* The implementation is in with a stack of sets of literals.
The operations are
- adding a set into the set (empty or singleton)
- taking the union of two top stacks
- removing the top or the second set from the stack
- comparing the two top sets (cardinality?) for choosing a disjunct
tset_stack: element is the index of the first element of the set in tset_store
*/
typedef struct {
int l;
short t;
} storepair;
int stacktop;
int storetop;
int tset_stack[1000];
int tset_card[1000];
storepair tset_store[100000];
#define CARDTOP (storetop-tset_stack[stacktop]+1)
#define CARD2ND (tset_stack[stacktop]-tset_stack[stacktop-1])
void tset_emptyset() {
#ifdef DEBUGDISJ
printf("tset_emptyset\n");
#endif
stacktop += 1;
tset_card[stacktop] = 0;
tset_stack[stacktop] = storetop+1;
}
void tset_show() {
#ifdef DEBUGDISJ
int i,j;
printf("=========================================================\n");
for(i=0;i<=storetop+1;i++) {
for(j=0;j<=stacktop;j++) {
if(tset_stack[j] == i) printf("START %i (card %i)\n",j,tset_card[j]);
}
if(i<=storetop) {
printf("%i: ",i); printlit(tset_store[i].l); printf("@%i\n",tset_store[i].t);
}
}
printf(" =========================================================\n");
#endif
}
/* Add the empty set in the stack. */
void tset_makeempty() {
#ifdef DEBUGDISJ
printf("tset_makeempty\n");
#endif
stacktop=-1;
storetop=-1;
tset_emptyset(); /* Always have an empty set in the stack. */
}
/* Add a singleton set into the stack. */
void tset_singleton(int l,int t) {
#ifdef DEBUGDISJ
printf("tset_singleton "); printlit(l); printf("@%i\n",t);
#endif
storetop = storetop+1;
tset_store[storetop].l = l;
tset_store[storetop].t = t;
stacktop = stacktop+1;
tset_stack[stacktop] = storetop;
tset_card[stacktop] = 1;
}
/* Take the union of the two top sets. */
void tset_union() {
#ifdef DEBUGDISJ
printf("tset_union\n");
#endif
tset_card[stacktop-1] = tset_card[stacktop-1]+tset_card[stacktop];
stacktop = stacktop - 1;
}
/* Return TRUE if top element has a smaller cardinality than the second. */
int tset_top_better() {
if(tset_card[stacktop] < tset_card[stacktop-1]) return 1; else return 0;
}
/* Remove the top set from the stack. */
void tset_top_delete() {
#ifdef DEBUGDISJ
printf("tset_top_delete\n");
#endif
storetop = storetop-tset_card[stacktop];
stacktop = stacktop-1;
}
/* Remove the second set from the stack. */
void tset_second_delete() {
int i,n;
#ifdef DEBUGDISJ
printf("tset_second_delete\n");
#endif
n = tset_card[stacktop];
/* Move the top set where the second one was. */
for(i=0;i<n;i++) {
tset_store[tset_stack[stacktop-1]+i] = tset_store[tset_stack[stacktop]+i];
}
storetop = tset_stack[stacktop-1]+n-1;
stacktop = stacktop-1;
tset_card[stacktop]=n;
}
int traverseDfma(satinstance sati,fma *f,int t) {
fmalist *fs;
int have;
#ifdef DEBUGDISJ
tset_show();
#endif
switch(f->t) {
/* Here we have to restrict to literals that are not FALSE ? */
case patom:
if(tvarfalsep(sati,f->a,t)) return 0;
tset_singleton(PLIT(f->a),t);
return 1;
case natom:
if(tvartruep(sati,f->a,t)) return 0;
tset_singleton(NLIT(f->a),t);
return 1;
case conj: /* The literal sets for all conjuncts are combined. */
tset_emptyset();
fs = f->juncts;
while(fs != NULL) {
if(traverseDfma(sati,fs->hd,t) == 0) {
tset_top_delete();
return 0;
}
tset_union();
fs = fs->tl;
}
return 1;
case disj: /* The set for one of the disjuncts is chosen, others ignored. */
// tset_emptyset(); ???????????????????
have = 0;
fs = f->juncts;
while(fs != NULL) {
if(traverseDfma(sati,fs->hd,t)) {
if(have) {
#ifdef DEBUGDISJ
tset_show();
#endif
if(tset_top_better()) tset_second_delete(); else tset_top_delete();
}
have = 1;
}
fs = fs->tl;
}
return have;
case TRUE: tset_emptyset(); return 1;
case FALSE: return 0;
}
return 0;
}
void push2goalstackDfma(satinstance sati,fma *f,int t) {
int i,l,t2;
tset_makeempty();
if(traverseDfma(sati,f,t) == 0) return;
#ifdef DEBUGDISJ
tset_show();
#endif
// if(tset_stack[stacktop]+1>storetop) printf("Not pushing anything\n");
/* Push the literals from the traverseDfma stack into the heuristic stack. */
for(i=tset_stack[stacktop];i<=storetop;i++) {
l = tset_store[i].l;
t2 = tset_store[i].t;
#ifdef DEBUGDISJ
printf("Pushing %i:",l); printlit(l); printf("@%i\n",t2);
#endif
push2goalstack(sati,l,t2);
}
}
#ifdef HARDDEBUG
void showheustack(satinstance sati) {
int i;
printf("STACK CONTENTS:\n");
for(i=0;i<stackptr;i++) {
printlit(stack[i].lit);
printf("@%i (score %i)\n",stack[i].t,stack[i].val);
}
}
#endif
#define TMPARRAYSIZE 1000
void do_cpath(satinstance);
int weightedscore(satinstance sati,int i) {
return sati->lits[PLIT(TVAR(plansteps[i].var,plansteps[i].t))].score + 10000-100*plansteps[i].flaws;
}
/* Identify actions that are useful in reaching the goals. */
int do_cpath_heuristic(satinstance sati) {
int i,j,best,besttime;
#ifdef WEIGHTS
int tmparray[TMPARRAYSIZE];
#endif
nextround(sati);
Nsteps = 0;
stackptr = 0;
switch(sati->heuristic_mode) {
case 0: /* Choose an action. */
if(goalisdisjunctive) {
push2goalstackDfma(sati,goal,sati->nOfTPoints-1);
} else {
push2goalstackCfma(sati,goal,sati->nOfTPoints-1);
}
#ifdef HARDDEBUG
showheustack(sati);
#endif
/* Find paths */
do_cpath(sati);
/* Pick action. */
/* Only one action to choose from: return it directly. */
if(Nsteps == 1) return PLIT(TVAR(plansteps[0].var,plansteps[0].t));
if(Nsteps > 0) {
switch(HEURactionchoice) {
case 0: /* Choose action randomly. */
i = random() % Nsteps;
break;
case 1: /* Choose the earliest possible action. */
best = -1;
besttime = 100000;
for(i=0;i<Nsteps;i++) {
if(plansteps[i].t < besttime) {
best = i;
besttime = plansteps[i].t;
}
}
i = best;
break;
case 2: /* Choose action randomly, with bias to earlier. */
j = random() % Nsteps;
i = random() % (j+1);
break;
case 3: /* Choose action randomly, with bias to later. */
j = random() % Nsteps;
i = Nsteps-(random() % (j+1))-1;
break;
case 4: /* Choose action based on its weight, with ties broken
randomly. */
#ifdef WEIGHTS
best = -1;
for(i=0;i< Nsteps;i++) { /* Determine the best score. */
int score = weightedscore(sati,i);
if(score > best) best = score;
}
j = 0;
for(i=0;i<Nsteps;i++) { /* Collect the literals with the best score. */
if(weightedscore(sati,i) == best) {
tmparray[j++] = i;
ASSERT(j < 1000);
}
}
i = tmparray[random() % j];
break;
#else
fprintf(stderr,"Heuristic needs WEIGHTS compiled.\n");
exit(1);
#endif
}
return PLIT(TVAR(plansteps[i].var,plansteps[i].t));
// return TLIT(plansteps[i].l,plansteps[i].t);
}
sati->heuristic_mode = 1;
sati->heuristic_time = 1;
sati->heuristic_index = 0;
case 1: /* No actions needed. Do inertia. */
#ifdef HEURDEBUG
printf("Doing INERTIA\n");
#endif
while(sati->heuristic_time < sati->nOfTPoints) {
i = sati->heuristic_index;
j = sati->heuristic_time;
if(i+1 == sati->nOfSVars) {
sati->heuristic_index = 0;
sati->heuristic_time += 1;
} else {
sati->heuristic_index += 1;
}
if(tvarunsetp(sati,i,j)) {
if(tvartruep(sati,i,j-1)) return PLIT(TVAR(i,j));
else return NLIT(TVAR(i,j));
}
}
sati->heuristic_mode = 2;
sati->heuristic_time = 0;
sati->heuristic_index = 0;
case 2: /* All state variables have a value. Set actions to FALSE. */
while(sati->heuristic_time < sati->nOfTPoints-1) {
i = sati->heuristic_index;
j = sati->heuristic_time;
if(i+1 == sati->nOfActions) {
sati->heuristic_index = 0;
sati->heuristic_time += 1;
} else {
sati->heuristic_index += 1;
}
if(tvarunsetp(sati,ACTVAR(i),j)) return NLIT(TVAR(ACTVAR(i),j));
}
}
return -1;
}
int fmavalue(satinstance sati,fma *f,int t) {
fmalist *juncts;
switch(f->t) {
case patom: if(!tvarfalsep(sati,f->a,t)) return 1; else return 0;
case natom: if(!tvartruep(sati,f->a,t)) return 1; else return 0;
case disj:
juncts = f->juncts;
while(juncts != NULL) {
if(fmavalue(sati,juncts->hd,t) != 0) return 1;
juncts = juncts->tl;
}
return 0;
case conj:
juncts = f->juncts;
while(juncts != NULL) {
if(fmavalue(sati,juncts->hd,t) == 0) return 0;
juncts = juncts->tl;
}
return 1;
case TRUE: return 1;
case FALSE: return 0;
}
return 0;
}
/* Estimate the value for an action */
int actionvalue(satinstance sati,int var,int t,fma *precondition,int disjunctive) {
int i;
int val;
switch(HEURops) {
case 1: /* Evaluate 'constrainedness' of action */
/* How many steps later can this action be taken? */
val = 0;
while(t+1 < sati->nOfTPoints-1 && !tvarfalsep(sati,var,t+1)) {
t = t+1;
val = val + 1;
}
return val;
case 2: /* Evaluate 'constrainedness' of action */
/* How many steps later can this action be taken? */
val = 0;
while(t+1 < sati->nOfTPoints-1 && !tvarfalsep(sati,var,t+1)) {
t = t+1;
val = val + 1;
}
return 1000-val;
case 3: /* Evaluate 'constrainedness' of precondition */
/* How many steps later can the precondition be true? */
val = 0;
while(t+1 < sati->nOfTPoints && fmavalue(sati,precondition,t+1) != 0) {
t = t+1;
val = val + 1;
}
return val;
case 4: /* Evaluate 'constrainedness' of precondition */
/* How many steps later can the precondition be true? */
val = 0;
while(t+1 < sati->nOfTPoints && fmavalue(sati,precondition,t+1) != 0) {
t = t+1;
val = val + 1;
}
return 1000-val;
case 5:
/* How many steps earlier can the precondition be true? */
val = 0;
while(t-1 >= 0 && fmavalue(sati,precondition,t-1) != 0) {
t = t-1;
val = val + 1;
}
return val;
case 6:
/* How many steps earlier can the precondition be true? */
val = 0;
while(t-1 >= 0 && fmavalue(sati,precondition,t-1) != 0) {
t = t-1;
val = val + 1;
}
return 1000-val;
case 7:
/* How many later suggested actions the action disables/affects. */
val = 0;
for(i=0;i<Nsteps;i++) {
if((plansteps[i].t > t) && (actaffects(var,plansteps[i].var))) {
val = val + 1;
}
}
// printf("{%i}",val);
return 1000-val;
default: assert(2==7);
}
}
/* Go through actions at time point t-1 to find one that could
make literal l true at t. "Could" means: l occurs as a conditional
or unconditional effect, and we don't care about the condition.
This is based on the following parameters (given on command line):
HEURtime: which time to consider, 0 = earliest, 1 = latest, 2 = all
HEURops: which operator to consider 0 = first (arbitrary), 1 = all
HEURchoice: which action@time to choose, 0 = random, 1 = weight
*/
/* Choose an action at t1-1 that can make l@t TRUE. The action is returned
in var,t. */
void supports(satinstance sati,int t0,int t1,int l,int *var,int *t,fma **precondition,int *disjunctive) {
compactCEstruct *ptr;
int bestvalue,value;
int bestvar,bestt,bestdisjunctive;
fma *bestprecondition;
if(HEURops == 0) { /* Return the "first" (arbitrary) action. */
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
if(!tvarfalsep(sati,ptr->var,t1-1)) { /* Is it applicable? */
#ifdef HARDDEBUG
printf("Add ACTION %i:",ptr->var); printUvar(ptr->var); printf("@%i\n",t1-1);
#endif
*var = ptr->var;
*t = t1-1;
*precondition = ptr->condition;
*disjunctive = ptr->disjunctive;
return;
}
}
assert(1==2);
}
bestvar = -1;
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
if(!tvarfalsep(sati,ptr->var,t1-1)) { /* Is it applicable? */
#ifdef HARDDEBUG
printf("Consider ACTION %i:",ptr->var); printUvar(ptr->var); printf("@%i\n",t1-1);
#endif
if(bestvar == -1) {
bestvar = ptr->var;
bestt = t1-1;
bestprecondition = ptr->condition;
bestdisjunctive = ptr->disjunctive;
bestvalue = actionvalue(sati,ptr->var,t1-1,ptr->condition,ptr->disjunctive);
} else {
value = actionvalue(sati,ptr->var,t1-1,ptr->condition,ptr->disjunctive);
if(value > bestvalue) {
bestvar = ptr->var;
bestt = t1-1;
bestprecondition = ptr->condition;
bestdisjunctive = ptr->disjunctive;
bestvalue = value;
}
}
}
}
assert(bestvar != -1);
#ifdef DECDEBUG
printf("Best action: ");
printUvar(bestvar);
printf("@%i for ",bestt);
printlit(l);
printf(" has value %i.\n",bestvalue);
#endif
*var = bestvar;
*t = bestt;
*precondition = bestprecondition;
*disjunctive = bestdisjunctive;
}
/* Is some action op actually making l true at t-1? (= op assigned TRUE?) */
int litmadetrue(satinstance sati,int l,int t,fma **precondition,int *disjunctive) {
int i;
if(!littruep(sati,litwithtime(sati,l,t))) return -1; /* l@t is not even true: no action! */
for(i=0;cCEs[l][i].var != -1;i++) { /* All ways of making l@t-1 true. */
if(tvartruep(sati,cCEs[l][i].var,t-1)) {
*precondition = cCEs[l][i].condition;
*disjunctive = cCEs[l][i].disjunctive;
return cCEs[l][i].var;
}
}
return -1; /* l@t-1 not made true. */
}
/***********************************************************************/
/*** Heuristic: ***/
/*** Find an unfulfilled (sub)goal and fulfill it at the earliest ***/
/*** possible time point. ***/
/*** ***/
/***********************************************************************/
#define noPRUNEfromGOAL
#define noPRUNEtoGOAL
void do_cpath(satinstance sati) {
int l,t,t1;
int j,var,isthere;
int suggestedactionsfound;
int depthlimitHIGH;
fma *precondition;
int disjunctive;
depthlimitHIGH = -1;
suggestedactionsfound = 0;
while(stackptr > 0) {
/* Pop literal-time pair from the stack. */
l = stack[stackptr-1].lit;
t = stack[--stackptr].t;
#ifdef PRUNEtoGOAL
if(HEURactiondepthlimit && suggestedactionsfound && t >= depthlimitHIGH)
return;
#endif
#ifdef HEURDEBUG
printf("Find action for goal "); printlit(l); printf("@%i.\n",t);
#endif
/* Starting from last time point, find last time t such that either
1) an action op@t-1 makes l@t TRUE, or
2) l@t-1 is FALSE and l@t is TRUE or UNASSIGNED.
*/
isthere = 0;
var = -1;
for(j=t;j>0;j--) {
var = litmadetrue(sati,l,j,&precondition,&disjunctive);
if(var != -1) {
isthere = 1;
t1 = j-1;
break;
}
if(litfalsep(sati,litwithtime(sati,l,j-1))) break;
}
if(j == 0) { /* Literal is true at time 0. */
#ifdef HEURDEBUG
printf("(true in the initial state.)\n");
#endif
continue;
}
/* Literal is last false at time point j-1. */
if(var == -1) { /* Choose an action that turns l true between j-1 and j. */
supports(sati,t,j,l,&var,&t1,&precondition,&disjunctive);
/* The following assertions cannot be false because
there must be an action that could make l true at t1 (i.e. is not FALSE).
If there were not, the frame action (-l & l) -> ... would
contradict Ass1 and Ass2.
*/
ASSERT(var != 0);
ASSERT(precondition->t != -1);
ASSERT(tlitfalsep(sati,l,j-1));
ASSERT(!tlitfalsep(sati,l,j));
}
if(seenp(sati,TVAR(var,t1))) continue; /* Operator already processed once. */
/* Don't go back to top-level goals. */
#ifndef PRUNEtoGOAL
if(HEURactiondepthlimit && suggestedactionsfound && t1 >= depthlimitHIGH)
return;
#endif
if(!isthere) { /* Add the variable to the list of candidate decisions. */
suggestedactionsfound += 1;
plansteps[Nsteps].var = var;
plansteps[Nsteps].t = t1;
plansteps[Nsteps].flaws = 0;
if(HEURops == 7) {
for(j=0;j<Nsteps;j++) {
if(actaffects(var,plansteps[j].var)) plansteps[Nsteps].flaws += 1;
}
}
plansteps[Nsteps++].l = l;
#ifdef HEURDEBUG
printf("Chose action ");
printUvar(var);
printf(" to make literal true @%i.\n",j);
#endif
#ifdef PRUNEfromGOAL
if(suggestedactionsfound == 1) depthlimitHIGH = t;
#else
if(suggestedactionsfound == 1) depthlimitHIGH = t1;
#endif
}
ASSERT(Nsteps < MAXPLANSTEPS);
if(suggestedactionsfound >= HEURactions) return;
#ifdef HARDDEBUG
printf(" Push preconditions of %i:",var); printUvar(var); printf("@%i into the stack (%i).\n",t1,isthere);
#endif
if(t1 > 0) { /* Push preconditions in the stack. */
if(disjunctive == 0) {
push2goalstackCfma(sati,precondition,t1);
} else {
push2goalstackDfma(sati,precondition,t1);
}
#ifdef HARDDEBUG
showheustack(sati);
#endif
}
}
}