blob: 011cc84802133118c1c9f382dde8170d46d3f49e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
#include <u.h>
#include <libc.h>
#include <sat.h>
#include "impl.h"
int
satmore(SATSolve *s)
{
int *a, i, n;
if(s == nil) return 1;
s->scrap = a = satrealloc(s, nil, s->nvar * sizeof(int));
n = 0;
for(i = 0; i < s->nvar; i++){
if((s->var[i].flags & VARUSER) != 0) continue;
switch(s->lit[2*i].val){
case 0: a[n++] = i+1; break;
case 1: a[n++] = -(i+1); break;
}
}
if(n > 0)
satadd1(s, a, n);
if(n == 1)
s->var[abs(a[0])-1].flags &= ~VARUSER;
free(a);
s->scrap = nil;
return satsolve(s);
}
|
