Created
July 9, 2025 20:26
-
-
Save vi/b58c1fe7c88efcf5086426773e7902a5 to your computer and use it in GitHub Desktop.
Patch for MiniSat+ to also output mapping from OPB to CNF variables when using -cnf option
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--- PbSolver.C.orig 2025-07-09 22:25:44.393796385 +0200 | |
+++ PbSolver.C 2025-07-09 22:24:07.817685378 +0200 | |
@@ -535,10 +535,22 @@ | |
addConstr(goal_ps, goal_Cs, opt_goal, -1), | |
convertPbs(false); | |
- if (opt_cnf != NULL) | |
- reportf("Exporting CNF to: \b%s\b\n", opt_cnf), | |
- sat_solver.exportCnf(opt_cnf), | |
+ if (opt_cnf != NULL) { | |
+ reportf("Exporting CNF to: \b%s\b\n", opt_cnf); | |
+ sat_solver.exportCnf(opt_cnf); | |
+ reportf("Exporting OPB to CNF mapping to %s.map\n", opt_cnf); | |
+ char fnbuf[4096]; | |
+ snprintf(fnbuf, sizeof(fnbuf), "%s.map", opt_cnf); | |
+ FILE *f = fopen(fnbuf, "wt"); | |
+ if(f) { | |
+ size_t n = index2name.size(); | |
+ for (size_t i = 0; i<n; i+=1) { | |
+ fprintf(f, "%s\n", index2name[i]); | |
+ } | |
+ fclose(f); | |
+ } | |
exit(0); | |
+ } | |
bool sat = false; | |
int n_solutions = 0; // (only for AllSolutions mode) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment