Skip to content

Commit

Permalink
Fixing a problem with a satisfied literals in soft clauses, when pass…
Browse files Browse the repository at this point in the history
…ing them to SCIP
  • Loading branch information
marekpiotrow committed Nov 26, 2023
1 parent 8d6c3bd commit 40d5e45
Show file tree
Hide file tree
Showing 10 changed files with 19 additions and 19 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ Since the version 1.4 you can use the solver as a library with the IPAMIR interf
4. build the SCIP solver library (if you want to use it)
* 4.1 get sources of scipoptsuite from https://scipopt.org/index.php#download
* 4.2 untar and build a static library it:
tar zxvf scipoptsuite-8.0.3.tgz
cd scipoptsuite-8.0.3
tar zxvf scipoptsuite-8.0.4.tgz
cd scipoptsuite-8.0.4
sed -i "s/add_library(libscip/add_library(libscip STATIC/g" scip/src/CMakeLists.txt
mkdir build && cd build
cmake -DNO_EXTERNAL_CODE=on -DSOPLEX=on -DTPI=tny ..
Expand Down
2 changes: 1 addition & 1 deletion ScipSolver.cc
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ lbool add_constr(SCIP *scip,
for (int j = 0; j < ps.size(); j++)
{
auto lit = ps[j];
if (solver->value(lit) != l_Undef) continue;
if (solver->value(lit) == l_False) continue;
if (set_scip_var(scip, solver, vars, lit)== l_False) return l_False;
auto v = vars[var(lit)];
MY_SCIP_CALL(SCIPaddCoefLinear(scip, cons, v, sign(lit) ? -1 : 1));
Expand Down
4 changes: 2 additions & 2 deletions config.cadical
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.cominisatps
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.cryptoms
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.glucose3
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.glucose4
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.maple
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.mergesat
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=
4 changes: 2 additions & 2 deletions config.minisat
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ MCL_INCLUDE?=
MCL_LIB?=
endif
ifneq ($(USESCIP),)
MCL_INCLUDE+=-I../scipoptsuite-8.0.3/scip/src -I../scipoptsuite-8.0.3/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.3/build/lib -lscip -lsoplex-pic
MCL_INCLUDE+=-I../scipoptsuite-8.0.4/scip/src -I../scipoptsuite-8.0.4/build/scip
MCL_LIB+=-L../scipoptsuite-8.0.4/build/lib -lscip -lsoplex-pic
endif
prefix?=

0 comments on commit 40d5e45

Please sign in to comment.