diff --git a/examples/rc2.py b/examples/rc2.py index 9a76fa8..087ffef 100755 --- a/examples/rc2.py +++ b/examples/rc2.py @@ -206,7 +206,7 @@ def __init__(self, formula, solver='g3', adapt=False, exhaust=False, self.trim = trim # clause selectors and mapping from selectors to clause ids - self.sels, self.smap, self.sall, self.s2cl = [], {}, [], {} + self.sels, self.smap, self.sall, self.s2cl, self.sneg = [], {}, [], {}, set([]) # other MaxSAT related stuff self.topv = formula.nv @@ -529,6 +529,15 @@ def enumerate(self, block=0): if selv in m: # clause is satisfied cl.append(-selv) + + # next time we want to falsify one of these + # clauses, i.e. we should encode the negation + # of each of these selectors + if selv in self.s2cl and not selv in self.sneg: + self.sneg.add(selv) + for il in self.s2cl[selv]: + self.oracle.add_clause([selv, -il]) + elif selv in self.s2cl: # clause is falsified and it is not unit size for il in self.s2cl[selv]: @@ -1706,10 +1715,10 @@ def usage(): if i == to_enum: break - - # needed for MSE'20 - if to_enum != 1 and block == 1: - print('v') + else: + # needed for MSE'20 + if verbose > 2 and vnew and to_enum != 1 and block == 1: + print('v') if verbose: if not optimum_found: diff --git a/pysat/__init__.py b/pysat/__init__.py index 4a40630..f6e1175 100644 --- a/pysat/__init__.py +++ b/pysat/__init__.py @@ -10,7 +10,7 @@ # current version #============================================================================== -VERSION = (0, 1, 6, "dev", 2) +VERSION = (0, 1, 6, "dev", 3) # PEP440 Format diff --git a/solvers/patches/cadical.patch b/solvers/patches/cadical.patch index cb86f73..89ecbac 100644 --- a/solvers/patches/cadical.patch +++ b/solvers/patches/cadical.patch @@ -15,7 +15,7 @@ diff -Naur build/solvers/cadical/Makefile solvers/cadical/Makefile +CXXPROF := -O3 -g3 -fno-inline -fno-omit-frame-pointer -pg -DNDEBUG +INCLUDES := -I. +LIBS := -L. -+SOURCES := analyze.cpp arena.cpp assume.cpp averages.cpp backtrack.cpp backward.cpp bins.cpp block.cpp ccadical.cpp checker.cpp clause.cpp collect.cpp compact.cpp config.cpp cover.cpp decide.cpp decompose.cpp deduplicate.cpp elim.cpp ema.cpp extend.cpp external.cpp file.cpp flags.cpp format.cpp gates.cpp instantiate.cpp internal.cpp ipasir.cpp limit.cpp logging.cpp lucky.cpp message.cpp minimize.cpp occs.cpp options.cpp parse.cpp phases.cpp probe.cpp profile.cpp proof.cpp propagate.cpp queue.cpp random.cpp reduce.cpp rephase.cpp report.cpp resources.cpp restart.cpp restore.cpp score.cpp signal.cpp solution.cpp solver.cpp stats.cpp subsume.cpp terminal.cpp ternary.cpp tracer.cpp transred.cpp util.cpp var.cpp version.cpp vivify.cpp walk.cpp watch.cpp ++SOURCES := analyze.cpp arena.cpp assume.cpp averages.cpp backtrack.cpp backward.cpp bins.cpp block.cpp ccadical.cpp checker.cpp clause.cpp collect.cpp compact.cpp config.cpp cover.cpp decide.cpp decompose.cpp deduplicate.cpp elim.cpp ema.cpp extend.cpp external.cpp file0.cpp flags.cpp format.cpp gates.cpp instantiate.cpp internal.cpp ipasir.cpp limit.cpp logging.cpp lucky.cpp message.cpp minimize.cpp occs.cpp options.cpp parse.cpp phases.cpp probe.cpp profile.cpp proof.cpp propagate.cpp queue.cpp random.cpp reduce.cpp rephase.cpp report.cpp resources.cpp restart.cpp restore.cpp score.cpp signal.cpp solution.cpp solver.cpp stats.cpp subsume.cpp terminal.cpp ternary.cpp tracer.cpp transred.cpp util.cpp var.cpp version.cpp vivify.cpp walk.cpp watch.cpp +OBJECTS := $(SOURCES:.cpp=.o) +TRGT := cadical + @@ -65,9 +65,9 @@ diff -Naur build/solvers/cadical/contract.hpp solvers/cadical/contract.hpp /*------------------------------------------------------------------------*/ // If the user violates API contracts while calling functions declared in -diff -Naur build/solvers/cadical/file.cpp solvers/cadical/file.cpp ---- build/solvers/cadical/file.cpp 2019-07-12 22:22:02.000000000 +0200 -+++ solvers/cadical/file.cpp 2019-12-02 08:41:16.375326400 +0100 +diff -Naur build/solvers/cadical/file0.cpp solvers/cadical/file0.cpp +--- build/solvers/cadical/file0.cpp 2019-07-12 22:22:02.000000000 +0200 ++++ solvers/cadical/file0.cpp 2019-12-02 08:41:16.375326400 +0100 @@ -19,6 +19,19 @@ /*------------------------------------------------------------------------*/ diff --git a/solvers/prepare.py b/solvers/prepare.py index f947be1..24cde7c 100644 --- a/solvers/prepare.py +++ b/solvers/prepare.py @@ -129,7 +129,7 @@ ('src/extend.cpp', 'extend.cpp'), ('src/external.cpp', 'external.cpp'), ('src/external.hpp', 'external.hpp'), - ('src/file.cpp', 'file.cpp'), + ('src/file.cpp', 'file0.cpp'), ('src/file.hpp', 'file.hpp'), ('src/flags.cpp', 'flags.cpp'), ('src/flags.hpp', 'flags.hpp'), diff --git a/web/news.rst b/web/news.rst index b785b7f..f02b01b 100644 --- a/web/news.rst +++ b/web/news.rst @@ -11,6 +11,12 @@ to date and then is good idea. Changelog and more ------------------ +07.07.2020 (*0.1.6.dev3*) +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- Fixed RC2's enumeration of MSSes. +- Minor changes to the patch for CaDiCaL + 06.07.2020 (*0.1.6.dev2*) ~~~~~~~~~~~~~~~~~~~~~~~~~~