Commit b15c685e authored by Masahiko Sakai's avatar Masahiko Sakai

version 1.01 (bugfixed version of 1.00

parent af9a253a
......@@ -26,6 +26,7 @@ Contains types, macros, and inline functions generally useful in a C++ program.
#ifndef Global_h
#define Global_h
#include <signal.h>
#include <cassert>
#include <cstdio>
#include <cstdlib>
......
......@@ -61,7 +61,7 @@ void dump(const vec<Lit>& ps, const vec<Int>& Cs)
dump(Cs[i]);
reportf("*");
dump(ps[i]);
if (i+1 < ps.size()) reportf(" ");
if (i+1 < ps.size()) reportf("...");
}
}
......@@ -73,7 +73,7 @@ void dump(const vec<Formula>& ps, const vec<Int>& Cs)
dump(Cs[i]);
reportf("*");
dump(ps[i]);
if (i+1 < ps.size()) reportf(" ");
if (i+1 < ps.size()) reportf("...");
}
}
......@@ -92,7 +92,7 @@ void dump(const vec<Lit>& ps, const vec<Int>& Cs, const vec<int>& assigns)
reportf(":1");
else
reportf(":0");
if (i+1 < ps.size()) reportf(" ");
if (i+1 < ps.size()) reportf("...");
}
}
......@@ -147,7 +147,7 @@ void dump(const Linear& pb, const vec<int>& assigns)
reportf(":1");
else
reportf(":0");
if (i+1 < pb.size) reportf(" ");
if (i+1 < pb.size) reportf("...");
}
reportf("in ["); dump(pb.lo); reportf(","); dump(pb.hi); reportf("]");
}
* Example of Definition
* Descriptions are equivalent to the following:
* (1*~x2 2*x3 >= 2) or (1*~x2 2*x3 < 2)
d x0 => 1 ~x2 2 x3 >= 2 ;
d x1 => 1 ~x2 2 x3 < 2 ;
1 x0 1 x1 >= 1 ;
* Example of Definition
* Descriptions are equivalent to the following:
* (1*~x2 2*x3 >= 2) or (1*~x2 2*x3 < 2)
d x0 => 1 ~x2 2 x3 >= 2 ;
d x1 => 1 ~x2 2 x3 < 2 ;
1 x0 1 x1 >= 1 ;
1 x0 >= 1;
* Example of Definition
* Descriptions are equivalent to the following:
* (1*~x2 2*x3 >= 2) or (1*~x2 2*x3 < 2)
d x0 <= 1 ~x2 2 x3 >= 2 ;
d x1 <= 1 ~x2 2 x3 < 2 ;
1 x0 1 x1 >= 1 ;
1 x0 >= 1;
1 x1 >= 1;
* Example of Definition
* Descriptions are equivalent to the following:
* (1*~x2 2*x3 >= 2) or (1*~x2 2*x3 < 2)
d x0 <= 1 ~x2 2 x3 >= 2 ;
d x1 <= 1 ~x2 2 x3 < 2 ;
* Example of Definition
* Descriptions are equivalent to the following:
* (1*~x2 2*x3 >= 2) and not (1*~x2 1*x3 >= 2)
d x0 => 1 ~x2 2 x3 >= 2 ;
d x1 <= 1 ~x2 1 x3 >= 2 ;
1 x0 = 1;
1 x1 = 0;
+1 x1 +1 x2 +1 x3 = 2 ;
+1 ~x1 +1 ~x2 +1 x3 = 2 ;
This diff is collapsed.
This diff is collapsed.
+1 x1 +1 x2 +1 ~x3 >= 1 ;
+1 x2 +1 x4 +1 ~x3 = 1 ;
interest: x1 x2 ;
+1 x1 +1 x2 +2 x3 > 1 ;
+1 x1 -5 x2 +2 x3 <= -1 ;
+1 X1 +1 x2 +2 x3 > 1 ;
+1 x1 -5 x2 +2 x3 <= -1 ;
* #variable= 27 #constraint= 118
* converted from file: submitted/een/stein27.opb
min: +1 x0 +1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 ;
+1 x2 +1 x13 +1 x18 >= +1;
+1 x1 +1 x2 +1 x3 >= +1;
+1 x0 +1 x2 +1 x4 >= +1;
+1 x0 +1 x1 +1 x5 >= +1;
+1 x4 +1 x5 +1 x6 >= +1;
+1 x3 +1 x5 +1 x7 >= +1;
+1 x3 +1 x4 +1 x8 >= +1;
+1 x0 +1 x7 +1 x8 >= +1;
+1 x1 +1 x6 +1 x8 >= +1;
+1 x2 +1 x6 +1 x7 >= +1;
+1 x0 +1 x3 +1 x6 >= +1;
+1 x1 +1 x4 +1 x7 >= +1;
+1 x2 +1 x5 +1 x8 >= +1;
+1 x10 +1 x11 +1 x12 >= +1;
+1 x9 +1 x11 +1 x13 >= +1;
+1 x9 +1 x10 +1 x14 >= +1;
+1 x13 +1 x14 +1 x15 >= +1;
+1 x12 +1 x14 +1 x16 >= +1;
+1 x12 +1 x13 +1 x17 >= +1;
+1 x9 +1 x16 +1 x17 >= +1;
+1 x10 +1 x15 +1 x17 >= +1;
+1 x11 +1 x15 +1 x16 >= +1;
+1 x9 +1 x12 +1 x15 >= +1;
+1 x10 +1 x13 +1 x16 >= +1;
+1 x11 +1 x14 +1 x17 >= +1;
+1 x19 +1 x20 +1 x21 >= +1;
+1 x18 +1 x20 +1 x22 >= +1;
+1 x18 +1 x19 +1 x23 >= +1;
+1 x22 +1 x23 +1 x24 >= +1;
+1 x0 +1 x16 +1 x26 >= +1;
+1 x0 +1 x15 +1 x21 >= +1;
+1 x0 +1 x14 +1 x19 >= +1;
+1 x0 +1 x13 +1 x20 >= +1;
+1 x0 +1 x12 +1 x24 >= +1;
+1 x0 +1 x11 +1 x22 >= +1;
+1 x0 +1 x10 +1 x23 >= +1;
+1 x0 +1 x9 +1 x18 >= +1;
+1 x20 +1 x23 +1 x26 >= +1;
+1 x19 +1 x22 +1 x25 >= +1;
+1 x18 +1 x21 +1 x24 >= +1;
+1 x20 +1 x24 +1 x25 >= +1;
+1 x19 +1 x24 +1 x26 >= +1;
+1 x18 +1 x25 +1 x26 >= +1;
+1 x21 +1 x22 +1 x26 >= +1;
+1 x0 +1 x17 +1 x25 >= +1;
+1 x1 +1 x9 +1 x23 >= +1;
+1 x1 +1 x10 +1 x19 >= +1;
+1 x1 +1 x11 +1 x21 >= +1;
+1 x1 +1 x12 +1 x20 >= +1;
+1 x1 +1 x13 +1 x25 >= +1;
+1 x1 +1 x14 +1 x18 >= +1;
+1 x1 +1 x15 +1 x26 >= +1;
+1 x1 +1 x16 +1 x22 >= +1;
+1 x1 +1 x17 +1 x24 >= +1;
+1 x2 +1 x9 +1 x22 >= +1;
+1 x2 +1 x10 +1 x21 >= +1;
+1 x2 +1 x11 +1 x20 >= +1;
+1 x2 +1 x12 +1 x19 >= +1;
+1 x2 +1 x14 +1 x26 >= +1;
+1 x2 +1 x15 +1 x25 >= +1;
+1 x2 +1 x16 +1 x24 >= +1;
+1 x2 +1 x17 +1 x23 >= +1;
+1 x3 +1 x9 +1 x24 >= +1;
+1 x3 +1 x10 +1 x20 >= +1;
+1 x3 +1 x11 +1 x19 >= +1;
+1 x3 +1 x12 +1 x21 >= +1;
+1 x3 +1 x13 +1 x26 >= +1;
+1 x3 +1 x14 +1 x25 >= +1;
+1 x3 +1 x15 +1 x18 >= +1;
+1 x3 +1 x16 +1 x23 >= +1;
+1 x3 +1 x17 +1 x22 >= +1;
+1 x4 +1 x9 +1 x20 >= +1;
+1 x4 +1 x10 +1 x25 >= +1;
+1 x4 +1 x11 +1 x18 >= +1;
+1 x4 +1 x12 +1 x26 >= +1;
+1 x4 +1 x13 +1 x22 >= +1;
+1 x4 +1 x14 +1 x24 >= +1;
+1 x4 +1 x15 +1 x23 >= +1;
+1 x4 +1 x16 +1 x19 >= +1;
+1 x4 +1 x17 +1 x21 >= +1;
+1 x5 +1 x9 +1 x19 >= +1;
+1 x5 +1 x10 +1 x18 >= +1;
+1 x5 +1 x11 +1 x26 >= +1;
+1 x5 +1 x12 +1 x25 >= +1;
+1 x5 +1 x13 +1 x24 >= +1;
+1 x5 +1 x14 +1 x23 >= +1;
+1 x5 +1 x15 +1 x22 >= +1;
+1 x21 +1 x23 +1 x25 >= +1;
+1 x5 +1 x16 +1 x21 >= +1;
+1 x5 +1 x17 +1 x20 >= +1;
+1 x6 +1 x9 +1 x21 >= +1;
+1 x6 +1 x10 +1 x26 >= +1;
+1 x6 +1 x11 +1 x25 >= +1;
+1 x6 +1 x12 +1 x18 >= +1;
+1 x6 +1 x13 +1 x23 >= +1;
+1 x6 +1 x14 +1 x22 >= +1;
+1 x6 +1 x15 +1 x24 >= +1;
+1 x6 +1 x16 +1 x20 >= +1;
+1 x6 +1 x17 +1 x19 >= +1;
+1 x7 +1 x9 +1 x26 >= +1;
+1 x7 +1 x10 +1 x22 >= +1;
+1 x7 +1 x11 +1 x24 >= +1;
+1 x8 +1 x17 +1 x26 >= +1;
+1 x8 +1 x16 +1 x18 >= +1;
+1 x8 +1 x15 +1 x19 >= +1;
+1 x8 +1 x14 +1 x20 >= +1;
+1 x8 +1 x13 +1 x21 >= +1;
+1 x8 +1 x12 +1 x22 >= +1;
+1 x8 +1 x11 +1 x23 >= +1;
+1 x8 +1 x10 +1 x24 >= +1;
+1 x8 +1 x9 +1 x25 >= +1;
+1 x7 +1 x17 +1 x18 >= +1;
+1 x7 +1 x16 +1 x25 >= +1;
+1 x7 +1 x15 +1 x20 >= +1;
+1 x7 +1 x14 +1 x21 >= +1;
+1 x7 +1 x13 +1 x19 >= +1;
+1 x7 +1 x12 +1 x23 >= +1;
+1 x0 +1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 >= +13;
+1 v1 +1 v2 -1 v3 -1 v4 >= 1;
-1 v1 -1 v2 +1 v3 +1 v4 >= 1;
+1 x1 >= 2 ;
+1 v1 +1 v2 -1 v3 -1 v4 >= 1;
-1 v1 -1 v2 +1 v3 +1 v4 >= 1;
......@@ -113,12 +113,8 @@ Lit Clausifier::polarityClausify(Formula f)
}else if (vmapp.at(f) != lit_Undef && !s.varElimed(var(vmapp.at(f)))){
result = vmapp.at(f);
}else{
#if 1
result = vmapp.at(~f) != lit_Undef && !s.varElimed(var(vmapp.at(~f))) ?
result = (vmapp.at(~f) != lit_Undef && !s.varElimed(var(vmapp.at(~f)))) ?
Lit(var(vmapp.at(~f))) : Lit(s.newVar(!opt_branch_pbvars));
#else
result = Lit(s.newVar(!opt_branch_pbvars));
#endif
if (Bin_p(f)){
if (op(f) == op_And){
vec<Formula> conj;
......
......@@ -12,10 +12,6 @@ To make the BigNum version, type
make rs
To use them together (trying the faster 64-bit version first), use the script
gpw_script
-----
TIPS:
For compile error related to gmp.h, install libgmp3-dev library.
......
......@@ -35,6 +35,10 @@ Read a DIMACS file and apply the SAT-solver to it.
#include "Debug.h"
//=================================================================================================
// Tricky hack for priventing memory allocation error in SIGTERM_handler.
char* dummy_heap = (char*) malloc(32*1024);
// Command line options:
......@@ -520,6 +524,7 @@ static void SIGINT_handler(int signum) {
*/
static void SIGTERM_handler(int signum) {
free(dummy_heap);
reportf("\n");
if(signum <= 15) {
reportf("*** TERMINATED ***\n");
......@@ -542,9 +547,10 @@ int main(int argc, char** argv)
pb_solver = new PbSolver(); // (must be constructed AFTER parsing commandline options -- constructor uses 'opt_solver' to determinte which SAT solver to use)
// signal(SIGINT , SIGINT_handler);
signal(SIGINT , SIGTERM_handler);
signal(SIGTERM, SIGTERM_handler);
signal(SIGUSR1, SIGTERM_handler);
signal(SIGINT , SIGTERM_handler); // 2, SIGINT, terminate process, interrupt program
signal(SIGABRT , SIGTERM_handler); // 6, SIGABRT, create core image, abort program (formerly SIGIOT)
signal(SIGTERM, SIGTERM_handler); // 15, SIGTERM, terminate process, software termination signal
signal(SIGUSR1, SIGTERM_handler); // 30, SIGUSR1, terminate process, User defined signal 1
// Set command from 'PBSATISFIABILITYONLY':
char* value = getenv("PBSATISFIABILITYONLY");
......
......@@ -24,7 +24,7 @@ CFLAGS += -IADTs -Iglueminisat -include Main.h -D_FILE_OFFSET_BITS=64 -D __STD
CFLAGS += -I/usr/local/include -fno-strict-aliasing
COPTIMIZE = -O3 -fomit-frame-pointer -falign-loops=4 -falign-functions=16 -foptimize-sibling-calls -finline-functions -fcse-follow-jumps -fcse-skip-blocks -frerun-cse-after-loop -frerun-loop-opt -fgcse
LDFLAGS += -L/usr/local/lib
LDFLAGS += -L/usr/local/lib -L/opt/local/lib
LDFLAGS += -L/usr/lib
.PHONY : s p d r x build clean depend
......
......@@ -89,6 +89,9 @@ void PbSolver::addGoal(const vec<Lit>& ps, const vec<Int>& Cs)
}
} else goal_coeff = 1;
if(opt_verbosity >=1 )
reportf("goal was devided by "),dump(goal_coeff),reportf(".\n");
if(goal_coeff != 1) {
for (int i = 0; i < Cs.size(); i++)
norm_Cs.push( Cs[i] / goal_coeff );
......@@ -914,7 +917,7 @@ Int evalGoal(Linear& goal, Solver& sat_solver)
//}
static
Int possibleGoal(Linear& goal)
Int negSumGoalCoeff(Linear& goal)
{
Int sum = 0;
for (int i = 0; i < goal.size; i++){
......@@ -969,7 +972,8 @@ void PbSolver::solve(const PbSolver& S, solve_Command cmd)
opt_sort_thres *= opt_goal_bias;
if (opt_goal != Int_MAX){ // reportf("opt_GOAL"),dump(opt_goal),reportf("\n");
if(!addConstr(goal_ps, goal_Cs, opt_goal/goal_coeff, -1)) // <=
opt_goal = opt_goal/goal_coeff;
if(!addConstr(goal_ps, goal_Cs, opt_goal, -1)) // <=
{solver_status = sst_unsat; ok = false; return;}
else convertPbs(false);
}
......@@ -988,10 +992,11 @@ void PbSolver::solve(const PbSolver& S, solve_Command cmd)
bool sat = false, exec_loop = true;
int assump_litn;
vec<Lit> assump_ps;
Int try_lessthan = (opt_goal != Int_MAX ? opt_goal/goal_coeff : opt_goal);
Int possible_goalvalue = 0 ;
Int try_lessthan = opt_goal;
Int LB_goalvalue;
// Int LB_goalvalue = Int_MIN ;
if(goal != NULL) possible_goalvalue = possibleGoal(*goal);
if(goal != NULL) LB_goalvalue = negSumGoalCoeff(*goal);
while (exec_loop){
#ifdef DEBUG
if(opt_verbosity >=3)
......@@ -1030,54 +1035,54 @@ void PbSolver::solve(const PbSolver& S, solve_Command cmd)
if (goal == NULL) // ((fix: moved here Oct 4, 2005))
break;
Int goalvalue = evalGoal(*goal, sat_solver);
#ifdef DEBUG
best_goalvalue = evalGoal(*goal, sat_solver);
#ifdef DEBUG
if (opt_verbosity >= 2){
char* hi = toString(goalvalue);
char* hi = toString(best_goalvalue);
char* lo = toString(try_lessthan);
reportf("DEBUG: goalvalue,try_lessthan=%s,%s\n", hi, lo);
reportf("DEBUG-found: best_goalvalue,try_lessthan=%s,%s\n", hi, lo);
xfree(lo),xfree(hi); }
#endif
assert(goalvalue <= try_lessthan);
best_goalvalue = goalvalue;
#endif
assert(best_goalvalue < try_lessthan);
// best_goalvalue = goalvalue;
if (cmd == sc_FirstSolution) break;
{
char* gv = toString(goalvalue);
char* gv = toString(best_goalvalue*goal_coeff);
printf("o %s\n", gv);
if (opt_verbosity >= 1){
char* lo = toString(possible_goalvalue);
reportf("Found a solution: %s. Optimum solution is in [%s,%s]\n", gv, lo, gv);
xfree(lo);
char* lo = toString(LB_goalvalue);
char* hi = toString(best_goalvalue);
reportf("Found a solution: %s*goal_coeff. Optimum solution is in [%s,%s]\n", hi, lo, hi);
xfree(lo);xfree(hi);
}
xfree(gv);
}
// if( (!opt_binary_minimization) || best_goalvalue - possible_goalvalue < 5) {
if( (opt_minimization==0) // sequential
|| best_goalvalue - possible_goalvalue < 5) {
if( (opt_minimization==0)
|| best_goalvalue - LB_goalvalue < 5) { // sequential
if(opt_verbosity >=1) reportf("UOne-by-One\n");
try_lessthan = best_goalvalue;
if (!addConstr(goal_ps, goal_Cs, best_goalvalue, -2))
break; // unsat
} else {
Int lb = Int_MAX;
assump_litn = sat_solver.newVar(false);
#ifdef DEBUG
// if(opt_verbosity >= 1) reportf("3:NewVar: %d%c\n", assump_litn, false?'d':'-');
#endif
//assump_litn = sat_solver.newVar(false);
assump_litn = sat_solver.newVar(true);
#ifdef DEBUG
if(opt_verbosity >= 2) reportf("3:NewVar: %d%c\n", assump_litn, false?'d':'-');
#endif
Lit assump_lit = Lit(assump_litn);
try_lessthan = (possible_goalvalue+best_goalvalue)/2;
if(opt_band_for_goal) lb = possible_goalvalue;
try_lessthan = (LB_goalvalue+best_goalvalue)/2;
if(opt_band_for_goal) lb = LB_goalvalue;
if(opt_verbosity >= 1) {
char* bg = toString(try_lessthan);
char* lg = toString(lb);
char* hi = toString(try_lessthan);
char* lo = toString(lb);
if(lb == Int_MAX)
reportf("Try to find a solution less than %s\n", bg);
reportf("Try to find a solution less than %s\n", hi);
else
reportf("Try to find a solution between [%s,%s)\n", lg,bg);
xfree(bg),xfree(lg);}
reportf("Try to find a solution between [%s,%s)\n", lo,hi);
xfree(lo),xfree(hi);}
if (!addConstr(goal_ps, goal_Cs, try_lessthan, -2, lb, 1, assump_lit)) break; // unsat
......@@ -1104,39 +1109,40 @@ void PbSolver::solve(const PbSolver& S, solve_Command cmd)
sat_solver.addClause(ban); //addUnit?
*/
//**/ {char* po = toString(possible_goalvalue); char* tr = toString(try_lessthan); reportf("DEBUG po,tr= %s,%s\n", po, tr); xfree(po),xfree(tr); }
possible_goalvalue = try_lessthan;
//**/ {char* po = toString(LB_goalvalue); char* tr = toString(try_lessthan); reportf("DEBUG po,tr= %s,%s\n", po, tr); xfree(po),xfree(tr); }
LB_goalvalue = try_lessthan;
if(opt_verbosity >=1){
char* hi = toString(best_goalvalue);
char* lo = toString(possible_goalvalue);
char* lo = toString(LB_goalvalue);
reportf("Better solution not found. Optimum solution is in [%s,%s]\n", lo, hi);
xfree(lo),xfree(hi); }
// if( (!opt_binary_minimization) || best_goalvalue - possible_goalvalue < 5) {
// if( (!opt_binary_minimization) || best_goalvalue - LB_goalvalue < 5) {
if( (opt_minimization != 1) // if not binary
|| best_goalvalue - possible_goalvalue < 5) {
|| best_goalvalue - LB_goalvalue < 5) {
if(opt_verbosity >=1) reportf("UOne-by-One\n");
try_lessthan = best_goalvalue;
if (!addConstr(goal_ps, goal_Cs, best_goalvalue, -2)) // <
break; // unsat
} else {
Int lb = Int_MAX;
assump_litn = sat_solver.newVar(false);
//assump_litn = sat_solver.newVar(false);
assump_litn = sat_solver.newVar(true);
#ifdef DEBUG
// if(opt_verbosity >= 1) reportf("4:NewVar: %d%c\n", assump_litn, false?'d':'-');
#endif
Lit assump_lit = Lit(assump_litn);
try_lessthan = (possible_goalvalue+best_goalvalue)/2;
if(opt_band_for_goal) lb = possible_goalvalue;
try_lessthan = (LB_goalvalue+best_goalvalue)/2;
if(opt_band_for_goal) lb = LB_goalvalue;
if(opt_verbosity >= 1) {
char* bg = toString(try_lessthan);
char* lg = toString(lb);
char* hi = toString(try_lessthan);
char* lo = toString(lb);
if(lb == Int_MAX)
reportf("Try to find a solution less than %s\n", bg);
else reportf("Try to find a solution between [%s,%s)\n", lg,bg);
xfree(bg),xfree(lg);}
reportf("Try to find a solution less than %s\n", hi);
else reportf("Try to find a solution between [%s,%s)\n", lo,hi);
xfree(hi),xfree(lo);}
if (!addConstr(goal_ps, goal_Cs, try_lessthan, -2, lb, 1, assump_lit))
break; // unsat
......
......@@ -50,7 +50,12 @@ Usage: Try
Known BUG:
- -S may result wrong answer.
- -model-check does not work.
- A bug exists. See PB-evaluation 2015 web site.
Version 1.01 Mar 25, 2016.
- Fixed the following bugs.
= A bug when calling Simp-solvers in 1.00.
= A bug when the simplification solver of glueminisat is used.
= A bug on displaying 'o' value in rare case.
Version 1.00 July 30, 2015.
- released. It was renamed from 'gpw version 2.18'. In default,
......
......@@ -134,10 +134,9 @@ class Clause {
unsigned learnt : 1;
unsigned has_extra : 1;
unsigned reloced : 1;
// modified by by nabesima
//unsigned size : 27;
unsigned lbd : 11;
unsigned size : 16;
unsigned size : 27;
// added by nabesima
unsigned lbd;
// added by daiki
uint32_t cid;
} header;
......@@ -153,6 +152,7 @@ class Clause {
header.has_extra = use_extra;
header.reloced = 0;
header.lbd = 0; // added by nabesima
assert(ps.size() < (1 << 26));
header.size = ps.size();
for (int i = 0; i < ps.size(); i++)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment