~ubuntu-branches/ubuntu/vivid/minisat+/vivid : revision 3

1

/******************************************************************************************[Main.C]

2

3

4

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and

5

associated documentation files (the "Software"), to deal in the Software without restriction,

6

including without limitation the rights to use, copy, modify, merge, publish, distribute,

7

sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is

8

furnished to do so, subject to the following conditions:

9

10

The above copyright notice and this permission notice shall be included in all copies or

11

substantial portions of the Software.

12

13

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT

14

NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND

15

NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,

16

DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT

17

OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

18

**************************************************************************************************/

19

20

/**************************************************************************************************

21

22

Read a DIMACS file and apply the SAT-solver to it.

23

24

**************************************************************************************************/

25

26

27

#include <cstdarg>

28

#include <unistd.h>

29

#include <signal.h>

30

#include "MiniSat.h"

31

#include "PbSolver.h"

32

#include "PbParser.h"

33

34

35

//=================================================================================================

36

// Command line options:

37

38

39

bool opt_satlive = true;

40

bool opt_ansi = true;

41

char* opt_cnf = NULL;

42

int opt_verbosity = 1;

43

bool opt_try = false; // (hidden option -- if set, then "try" to parse, but don't output "s UNKNOWN" if you fail, instead exit with error code 5)

44

45

SolverT opt_solver = st_MiniSat;

46

ConvertT opt_convert = ct_Mixed;

47

ConvertT opt_convert_goal = ct_Undef;

48

bool opt_convert_weak = true;

49

double opt_bdd_thres = 3;

50

double opt_sort_thres = 20;

51

double opt_goal_bias = 3;

52

Int opt_goal = Int_MAX;

53

Command opt_command = cmd_Minimize;

54

bool opt_branch_pbvars = false;

55

int opt_polarity_sug = 1;

56

bool opt_old_format = false;

57

58

char* opt_input = NULL;

59

char* opt_result = NULL;

60

61

//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

62

63

cchar* doc =

64

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"

65

"MiniSat+ 1.0, based on MiniSat v1.13 -- (C) Niklas Een, Niklas Sorensson, 2005\n"

66

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"

67

"USAGE: minisat+ <input-file> [<result-file>] [-<option> ...]\n"

68

"\n"

69

"Solver options:\n"

70

" -M -minisat Use MiniSat v1.13 as backend (default)\n"

71

" -S -satelite Use SatELite v1.0 as backend\n"

72

"\n"

73

" -ca -adders Convert PB-constrs to clauses through adders.\n"

74

" -cs -sorters Convert PB-constrs to clauses through sorters.\n"

75

" -cb -bdds Convert PB-constrs to clauses through bdds.\n"

76

" -cm -mixed Convert PB-constrs to clauses by a mix of the above. (default)\n"

77

" -ga/gs/gb/gm Override conversion for goal function (long name: -goal-xxx).\n"

78

" -w -weak-off Clausify with equivalences instead of implications.\n"

79

"\n"

80

" -bdd-thres= Threshold for prefering BDDs in mixed mode. [def: %g]\n"

81

" -sort-thres= Threshold for prefering sorters. Tried after BDDs. [def: %g]\n"

82

" -goal-bias= Bias goal function convertion towards sorters. [def: %g]\n"

83

"\n"

84

" -1 -first Don\'t minimize, just give first solution found\n"

85

" -A -all Don\'t minimize, give all solutions\n"

86

" -goal=<num> Set initial goal limit to '<= num'.\n"

87

"\n"

88

" -p -pbvars Restrict decision heuristic of SAT to original PB variables.\n"

89

" -ps{+,-,0} Polarity suggestion in SAT towards/away from goal (or neutral).\n"

90

"\n"

91

"Input options:\n"

92

" -of -old-fmt Use old variant of OPB file format.\n"

93

"\n"

94

"Output options:\n"

95

" -s -satlive Turn off SAT competition output.\n"

96

" -a -ansi Turn off ANSI codes in output.\n"

97

" -v0,-v1,-v2 Set verbosity level (1 default)\n"

98

" -cnf=<file> Write SAT problem to a file. Trivial UNSAT => no file written.\n"

99

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"

100

;

101

102

//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

103

104

bool oneof(cchar* arg, cchar* alternatives)

105

{

106

// Force one leading '-', allow for two:

107

if (*arg != '-') return false;

108

arg++;

109

if (*arg == '-') arg++;

110

111

// Scan alternatives:

112

vec<char*> alts;

113

splitString(alternatives, ",", alts);

114

for (int i = 0; i < alts.size(); i++){

115

if (strcmp(arg, alts[i]) == 0){

116

xfreeAll(alts);

117

return true;

118

}

119

}

120

xfreeAll(alts);

121

return false;

122

}

123

124

125

void parseOptions(int argc, char** argv)

126

{

127

vec<char*> args; // Non-options

128

129

for (int i = 1; i < argc; i++){

130

char* arg = argv[i];

131

if (arg[0] == '-'){

132

if (oneof(arg,"h,help")) fprintf(stderr, doc, opt_bdd_thres, opt_sort_thres, opt_goal_bias), exit(0);

133

134

else if (oneof(arg, "M,minisat" )) opt_solver = st_MiniSat;

135

else if (oneof(arg, "S,satelite")) opt_solver = st_SatELite;

136

137

else if (oneof(arg, "ca,adders" )) opt_convert = ct_Adders;

138

else if (oneof(arg, "cs,sorters")) opt_convert = ct_Sorters;

139

else if (oneof(arg, "cb,bdds" )) opt_convert = ct_BDDs;

140

else if (oneof(arg, "cm,mixed" )) opt_convert = ct_Mixed;

141

142

else if (oneof(arg, "ga,goal-adders" )) opt_convert_goal = ct_Adders;

143

else if (oneof(arg, "gs,goal-sorters")) opt_convert_goal = ct_Sorters;

144

else if (oneof(arg, "gb,goal-bdds" )) opt_convert_goal = ct_BDDs;

145

else if (oneof(arg, "gm,goal-mixed" )) opt_convert_goal = ct_Mixed;

146

147

else if (oneof(arg, "w,weak-off" )) opt_convert_weak = false;

148

149

//(make nicer later)

150

else if (strncmp(arg, "-bdd-thres=" , 11) == 0) opt_bdd_thres = atof(arg+11);

151

else if (strncmp(arg, "-sort-thres=", 12) == 0) opt_sort_thres = atof(arg+12);

152

else if (strncmp(arg, "-goal-bias=", 11) == 0) opt_goal_bias = atof(arg+11);

153

else if (strncmp(arg, "-goal=" , 6) == 0) opt_goal = atoi(arg+ 6); // <<== real bignum parsing here

154

else if (strncmp(arg, "-cnf=" , 5) == 0) opt_cnf = arg + 5;

155

//(end)

156

157

else if (oneof(arg, "1,first" )) opt_command = cmd_FirstSolution;

158

else if (oneof(arg, "A,all" )) opt_command = cmd_AllSolutions;

159

160

else if (oneof(arg, "p,pbvars" )) opt_branch_pbvars = true;

161

else if (oneof(arg, "ps+" )) opt_polarity_sug = +1;

162

else if (oneof(arg, "ps-" )) opt_polarity_sug = -1;

163

else if (oneof(arg, "ps0" )) opt_polarity_sug = 0;

164

165

else if (oneof(arg, "of,old-fmt" )) opt_old_format = true;

166

167

else if (oneof(arg, "s,satlive" )) opt_satlive = false;

168

else if (oneof(arg, "a,ansi" )) opt_ansi = false;

169

else if (oneof(arg, "try" )) opt_try = true;

170

else if (oneof(arg, "v0" )) opt_verbosity = 0;

171

else if (oneof(arg, "v1" )) opt_verbosity = 1;

172

else if (oneof(arg, "v2" )) opt_verbosity = 2;

173

174

else

175

fprintf(stderr, "ERROR! Invalid command line option: %s\n", argv[i]), exit(1);

176

177

}else

178

args.push(arg);

179

}

180

181

if (args.size() == 0)

182

fprintf(stderr, doc, opt_bdd_thres, opt_sort_thres, opt_goal_bias), exit(0);

183

if (args.size() >= 1)

184

opt_input = args[0];

185

if (args.size() == 2)

186

opt_result = args[1];

187

else if (args.size() > 2)

188

fprintf(stderr, "ERROR! Too many files specified on commandline.\n"),

189

exit(1);

190

}

191

192

193

//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

194

195

196

void reportf(const char* format, ...)

197

{

198

static bool col0 = true;

199

static bool bold = false;

200

va_list args;

201

va_start(args, format);

202

char* text = vnsprintf(format, args);

203

va_end(args);

204

205

for(char* p = text; *p != 0; p++){

206

if (col0 && opt_satlive)

207

putchar('c'), putchar(' ');

208

209

if (*p == '\b'){

210

bold = !bold;

211

if (opt_ansi)

212

putchar(27), putchar('['), putchar(bold?'1':'0'), putchar('m');

213

col0 = false;

214

}else{

215

putchar(*p);

216

col0 = (*p == '\n' || *p == '\r');

217

}

218

}

219

fflush(stdout);

220

}

221

222

223

//=================================================================================================

224

// Helpers:

225

226

227

PbSolver* pb_solver = NULL; // Made global so that the SIGTERM handler can output best solution found.

228

229

230

void outputResult(const PbSolver& S, bool optimum = true)

231

{

232

if (!opt_satlive) return;

233

234

if (optimum){

235

if (S.best_goalvalue == Int_MAX) printf("s UNSATISFIABLE\n");

236

else printf("s OPTIMUM FOUND\n");

237

}else{

238

if (S.best_goalvalue == Int_MAX) printf("s UNKNOWN\n");

239

else printf("s SATISFIABLE\n");

240

}

241

242

if (S.best_goalvalue != Int_MAX){

243

printf("v");

244

for (int i = 0; i < S.best_model.size(); i++)

245

printf(" %s%s", S.best_model[i]?"":"-", S.index2name[i]);

246

printf("\n");

247

}

248

fflush(stdout);

249

}

250

251

252

static void SIGINT_handler(int signum) {

253

reportf("\n");

254

reportf("*** INTERRUPTED ***\n");

255

SatELite::deleteTmpFiles();

256

_exit(0); } // (using 'exit()' rather than '_exit()' sometimes causes the solver to hang (why?))

257

258

259

static void SIGTERM_handler(int signum) {

260

reportf("\n");

261

reportf("*** TERMINATED ***\n");

262

outputResult(*pb_solver, false);

263

SatELite::deleteTmpFiles();

264

_exit(pb_solver->best_goalvalue == Int_MAX ? 0 : 10); }

265

266

267

void printStats(BasicSolverStats& stats, double cpu_time)

268

{

269

reportf("restarts : %"I64_fmt"\n", stats.starts);

270

reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", stats.conflicts , stats.conflicts /cpu_time);

271

reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", stats.decisions , stats.decisions /cpu_time);

272

reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time);

273

reportf("inspects : %-12"I64_fmt" (%.0f /sec)\n", stats.inspects , stats.inspects /cpu_time);

274

reportf("CPU time : %g s\n", cpu_time);

275

}

276

277

278

PbSolver::solve_Command convert(Command cmd) {

279

switch (cmd){

280

case cmd_Minimize: return PbSolver::sc_Minimize;

281

case cmd_FirstSolution: return PbSolver::sc_FirstSolution;

282

case cmd_AllSolutions: return PbSolver::sc_AllSolutions;

283

default: assert(false); }

284

}

285

286

287

//=================================================================================================

288

289

290

int main(int argc, char** argv)

291

{

292

/*DEBUG*/if (argc > 1 && (strcmp(argv[1], "-debug") == 0 || strcmp(argv[1], "--debug") == 0)){ void test(); test(); exit(0); }

293

294

parseOptions(argc, argv);

295

pb_solver = new PbSolver(); // (must be constructed AFTER parsing commandline options -- constructor uses 'opt_solver' to determinte which SAT solver to use)

296

signal(SIGINT , SIGINT_handler);

297

signal(SIGTERM, SIGTERM_handler);

298

299

// Set command from 'PBSATISFIABILITYONLY':

300

char* value = getenv("PBSATISFIABILITYONLY");

301

if (value != NULL && atoi(value) == 1)

302

reportf("Setting switch '-first' from environment variable 'PBSATISFIABILITYONLY'.\n"),

303

opt_command = cmd_FirstSolution;

304

305

if (opt_verbosity >= 1) reportf("Parsing PB file...\n");

306

parse_PB_file(opt_input, *pb_solver, opt_old_format);

307

pb_solver->solve(convert(opt_command));

308

309

if (pb_solver->goal == NULL && pb_solver->best_goalvalue != Int_MAX)

310

opt_command = cmd_FirstSolution; // (otherwise output will be wrong)

311

if (!pb_solver->okay())

312

opt_command = cmd_Minimize; // (HACK: Get "UNSATISFIABLE" as output)

313

314

// <<== write result to file 'opt_result'

315

316

if (opt_command == cmd_Minimize)

317

outputResult(*pb_solver);

318

else if (opt_command == cmd_FirstSolution)

319

outputResult(*pb_solver, false);

320

321

if (opt_verbosity >= 1) {

322

reportf("_______________________________________________________________________________\n\n");

323

printStats(pb_solver->stats, cpuTime());

324

reportf("_______________________________________________________________________________\n");

325

}

326

327

exit(pb_solver->best_goalvalue == Int_MAX ? 20 : (pb_solver->goal == NULL || opt_command == cmd_FirstSolution) ? 10 : 30); // (faster than "return", which will invoke the destructor for 'PbSolver')

328

}

329

330

331

332

//=================================================================================================

333

#include "Hardware.h"

334

#include "Debug.h"

335

336

#define N 10

337

338

void test(void)

339

{

340

Formula f = var(0), g = var(N-1);

341

for (int i = 1; i < N; i++)

342

f = Bin_new(op_Equiv, f, var(i)),

343

g = Bin_new(op_Equiv, g, var(N-i-1));

344

345

dump(f); dump(g);

346

347

printf("f= %d\n", index(f));

348

printf("g= %d\n", index(g));

349

350

Solver S(true);

351

vec<Formula> fs;

352

fs.push(f ^ g);

353

clausify(S, fs);

354

355

S.setVerbosity(1);

356

printf(S.solve() ? "SAT\n" : "UNSAT\n");

357

}