Skip to content

Commit

Permalink
Merge pull request #103 from conp-solutions/parallel-proofs
Browse files Browse the repository at this point in the history
Parallel proofs
  • Loading branch information
conp-solutions authored Jan 15, 2022
2 parents bd16219 + bf248a1 commit 129a792
Show file tree
Hide file tree
Showing 17 changed files with 680 additions and 126 deletions.
5 changes: 1 addition & 4 deletions .github/workflows/build-and-test-parallel.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
RUNOPENWBO: 0
RUNFUZZ: 0
RUNDIVERSIFY: 0
RUNPARALLELPROOF: 1
run: ./tools/ci.sh

- name: mergesat re-build
Expand All @@ -42,10 +43,6 @@ jobs:
run: |
./tools/check-determinism.sh "build/release/bin/mergesat -cores=3" "build/release/bin/mergesat -cores=3 -no-diversify" "build/release/bin/mergesat -cores=2 -no-pre" "build/debug/bin/mergesat -cores=3" "build/debug/bin/mergesat -cores=3 -no-diversify" "build/debug/bin/mergesat -cores=2 -no-pre"
- name: check cadical interface
run: |
./tools/cadical-interface/compare-cadical-mergesat.sh
MacOS:

Expand Down
1 change: 1 addition & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## [unreleased]

* parallel: support proof generation
* testing: use modgen generator during fuzzing runs
* fix FPU control to compile on ARM

Expand Down
14 changes: 11 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,15 @@ MINISAT_LDFLAGS = -Wall $(LD_EXTRA_FLAGS)
ifeq ($(BUILD_TYPE),)
BUILD_TYPE=simp
else
MINISAT_LDFLAGS += -lpthread
ifeq (Darwin,$(findstring Darwin,$(shell uname)))
MINISAT_LDFLAGS += -lpthread
else
# Static linking with conditional variables with glibc and libstdc++
# fails, in case we do not include whole archives. Just adding lpthread
# is not good enough.
# See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909
MINISAT_LDFLAGS += -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
endif
endif

ifeq (Darwin,$(findstring Darwin,$(shell uname)))
Expand Down Expand Up @@ -186,12 +194,12 @@ $(BUILD_DIR)/release/bin/$(MINISAT) $(BUILD_DIR)/debug/bin/$(MINISAT) $(BUILD_DI
$(BUILD_DIR)/debug/tests/%:
$(ECHO) Linking Binary: $@
$(VERB) mkdir -p $(dir $@)
$(VERB) $(CXX) $^ $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@
$(VERB) $(CXX) $^ $(MINISAT_LDFLAGS) $(MINISAT_CXXFLAGS) $(LDFLAGS) -o $@

$(BUILD_DIR)/release/tests/%:
$(ECHO) Linking Binary: $@
$(VERB) mkdir -p $(dir $@)
$(VERB) $(CXX) $^ $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@
$(VERB) $(CXX) $^ $(MINISAT_LDFLAGS) $(MINISAT_CXXFLAGS) $(LDFLAGS) -o $@

## Static Library rule
%/lib/$(MINISAT_SLIB):
Expand Down
33 changes: 33 additions & 0 deletions minisat/core/LockGuard.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
/*************************************************************************************[LockGuard.h]
Copyright (c) 2022, Norbert Manthey
**************************************************************************************************/

#ifndef LockGuard_h
#define LockGuard_h

#include "mtl/XAlloc.h"
#include <mutex>

namespace MERGESAT_NSPACE
{

/** Allow to easily grab a lock for the life time of a function or code block.*/
class LockGuard
{
std::mutex &lock;
bool doUnlock;

public:
LockGuard(std::mutex &externLock, bool doLock) : lock(externLock), doUnlock(doLock)
{
if (doLock) lock.lock();
}
~LockGuard()
{
if (doUnlock) lock.unlock();
}
};

} // namespace MERGESAT_NSPACE

#endif
87 changes: 52 additions & 35 deletions minisat/core/OnlineProofChecker.h
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Copyright (c) 2020, Norbert Manthey
#define OnlineProofChecker_h

#include "core/Constants.h"
#include "core/LockGuard.h"
#include "core/SolverTypes.h"
#include "mtl/Alg.h"
#include "mtl/Heap.h"
Expand Down Expand Up @@ -68,38 +69,40 @@ class OnlineProofChecker
vec<Lit> tmpLits; // for temporary addidion
int verbose;

std::mutex checker_mutex; // mutex to log the checker

public:
/** setup a proof checker with the given format */
OnlineProofChecker(ProofStyle proofStyle);

/** add a clause of the initial formula */
void addParsedclause(const vec<Lit> &cls);
void addParsedclause(const vec<Lit> &cls, bool dolock);

/** add a clause during search
* Note: for DRAT clauses only the very first literal will be used for checking RAT!
* @return true, if the addition of this clause is valid wrt. the current proof format
*/
bool addClause(const std::vector<int> &clause);
template <class T> bool addClause(const T &clause, const Lit &remLit, bool checkOnly = false);
bool addClause(const vec<Lit> &cls, bool checkOnly = false);
bool addClause(const Lit &l);
template <class T> bool addStrengthenedClause(const T &clause, const Lit toDropLit, bool checkOnly = false);
bool addClause(const std::vector<int> &clause, bool dolock);
template <class T> bool addClause(const T &clause, const Lit &remLit, bool checkOnly, bool dolock);
bool addClause(const vec<Lit> &cls, bool checkOnly, bool dolock);
bool addClause(const Lit &l, bool dolock);
template <class T> bool addStrengthenedClause(const T &clause, const Lit toDropLit, bool checkOnly, bool dolock);

/** remove a clause during search */
bool removeClause(const std::vector<int> &clause);
bool removeClause(const Lit &l);
template <class T> bool removeClause(const T &cls);
template <class T> bool removeClause(const T &cls, const Lit &rmLit);
bool removeClause(const std::vector<int> &clause, bool dolock);
bool removeClause(const Lit &l, bool dolock);
template <class T> bool removeClause(const T &cls, bool dolock);
template <class T> bool removeClause(const T &cls, const Lit &rmLit, bool dolock);

/** check whether the given clause exists in the current proof (useful for debugging) */
template <class T> bool hasClause(const T &cls);
bool hasClause(const Lit &cls);
template <class T> bool hasClause(const T &cls, bool dolock);
bool hasClause(const Lit &cls, bool dolock);

/// plot the current unit clauses and the current formula
void printState();

/// check whether all clauses in the online checker are correctly in the data structures!
void fullCheck();
void fullCheck(bool doLock);

/// set verbosity of the checker
void setVerbosity(int newVerbosity);
Expand Down Expand Up @@ -265,27 +268,30 @@ inline bool OnlineProofChecker::propagate()
return (confl != CRef_Undef); // return true, if something was found!
}

inline bool OnlineProofChecker::removeClause(const std::vector<int> &clause)
inline bool OnlineProofChecker::removeClause(const std::vector<int> &clause, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
tmpLits.clear();
for (size_t i = 0; i < clause.size(); ++i) {
tmpLits.push(clause[i] < 0 ? mkLit(-clause[i] - 1, true) : mkLit(clause[i] - 1, false));
}
// remove this clause in the usual way
return removeClause(tmpLits);
return removeClause(tmpLits, false);
}

inline bool OnlineProofChecker::removeClause(const Lit &l)
inline bool OnlineProofChecker::removeClause(const Lit &l, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
// create a clause with l
tmpLits.clear();
tmpLits.push(l);
// add this clause in the usual way
return removeClause(tmpLits);
return removeClause(tmpLits, false);
}

template <class T> inline bool OnlineProofChecker::removeClause(const T &cls, const Lit &remLit)
template <class T> inline bool OnlineProofChecker::removeClause(const T &cls, const Lit &remLit, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
tmpLits.clear();
if (remLit != lit_Undef) {
tmpLits.push(remLit);
Expand All @@ -296,18 +302,20 @@ template <class T> inline bool OnlineProofChecker::removeClause(const T &cls, co
}
}
// remove this clause in the usual way
return removeClause(tmpLits);
return removeClause(tmpLits, false);
}

inline bool OnlineProofChecker::hasClause(const Lit &cls)
inline bool OnlineProofChecker::hasClause(const Lit &cls, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
vec<Lit> l;
l.push(cls);
return hasClause(l);
return hasClause(l, false);
}

template <class T> inline bool OnlineProofChecker::hasClause(const T &cls)
template <class T> inline bool OnlineProofChecker::hasClause(const T &cls, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
if (verbose > 3) {
std::cerr << "c [DRAT-OTFC] check for clause " << cls << std::endl;
}
Expand Down Expand Up @@ -380,8 +388,9 @@ template <class T> inline bool OnlineProofChecker::hasClause(const T &cls)
}


template <class T> inline bool OnlineProofChecker::removeClause(const T &cls)
template <class T> inline bool OnlineProofChecker::removeClause(const T &cls, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
if (verbose > 3) {
std::cerr << "c [DRAT-OTFC] remove clause " << cls << std::endl;
printState();
Expand Down Expand Up @@ -503,8 +512,9 @@ template <class T> inline bool OnlineProofChecker::removeClause(const T &cls)
return true;
}

inline void OnlineProofChecker::addParsedclause(const vec<Lit> &cls)
inline void OnlineProofChecker::addParsedclause(const vec<Lit> &cls, bool doLock)
{
LockGuard guard(checker_mutex, doLock);
if (cls.size() == 0) {
ok = false;
return;
Expand Down Expand Up @@ -534,19 +544,22 @@ inline void OnlineProofChecker::addParsedclause(const vec<Lit> &cls)
// here, do not check whether the clause is entailed, because its still input!
}

inline bool OnlineProofChecker::addClause(const std::vector<int> &clause)
inline bool OnlineProofChecker::addClause(const std::vector<int> &clause, bool lock)
{
LockGuard guard(checker_mutex, lock);
// create a clause where remLit is the first literal
tmpLits.clear();
for (size_t i = 0; i < clause.size(); ++i) {
tmpLits.push(clause[i] < 0 ? mkLit(-clause[i] - 1, true) : mkLit(clause[i] - 1, false));
}
// add this clause in the usual way
return addClause(tmpLits);
return addClause(tmpLits, false, false);
}

template <class T> inline bool OnlineProofChecker::addClause(const T &clause, const Lit &remLit, bool checkOnly)
template <class T>
inline bool OnlineProofChecker::addClause(const T &clause, const Lit &remLit, bool checkOnly, bool lock)
{
LockGuard guard(checker_mutex, lock);
// create a clause where remLit is the first literal
tmpLits.clear();
if (remLit != lit_Undef) {
Expand All @@ -558,12 +571,13 @@ template <class T> inline bool OnlineProofChecker::addClause(const T &clause, co
}
}
// add this clause in the usual way
return addClause(tmpLits, checkOnly);
return addClause(tmpLits, checkOnly, false);
}

template <class T>
inline bool OnlineProofChecker::addStrengthenedClause(const T &clause, const Lit toDropLit, bool checkOnly)
inline bool OnlineProofChecker::addStrengthenedClause(const T &clause, const Lit toDropLit, bool checkOnly, bool lock)
{
LockGuard guard(checker_mutex, lock);
// create a clause without literal remLit
tmpLits.clear();
for (int i = 0; i < clause.size(); ++i) {
Expand All @@ -572,27 +586,29 @@ inline bool OnlineProofChecker::addStrengthenedClause(const T &clause, const Lit
}
}
// add this clause in the usual way
return addClause(tmpLits, checkOnly);
return addClause(tmpLits, checkOnly, false);
}

inline bool OnlineProofChecker::addClause(const Lit &l)
inline bool OnlineProofChecker::addClause(const Lit &l, bool lock)
{
LockGuard guard(checker_mutex, lock);
// create a clause with l
tmpLits.clear();
if (l != lit_Undef) {
tmpLits.push(l);
}
// add this clause in the usual way
return addClause(tmpLits);
return addClause(tmpLits, false, false);
}

inline bool OnlineProofChecker::addClause(const vec<Lit> &cls, bool checkOnly)
inline bool OnlineProofChecker::addClause(const vec<Lit> &cls, bool checkOnly, bool lock)
{
if (!ok) {
return true;
} // trivially true, we reached the empty clause already!
bool conflict = false;

LockGuard guard(checker_mutex, lock);
const int initialVars = nVars();

// have enough variables present
Expand Down Expand Up @@ -771,7 +787,7 @@ inline void OnlineProofChecker::printState()
return;
}

fullCheck();
fullCheck(false);

std::cerr << "c [DRAT-OTFC] STATE:" << std::endl;
for (int i = 0; i < unitClauses.size(); ++i) {
Expand All @@ -789,8 +805,9 @@ inline void OnlineProofChecker::printState()
}
}

inline void OnlineProofChecker::fullCheck()
inline void OnlineProofChecker::fullCheck(bool doLock)
{
LockGuard guard(checker_mutex, doLock);
for (int i = 0; i < clauses.size(); ++i) {
const CRef cr = clauses[i];
const Clause &c = ca[cr];
Expand Down
Loading

0 comments on commit 129a792

Please sign in to comment.