Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix Problem With Unused Branches #16

Closed
wants to merge 2 commits into from
Closed

Fix Problem With Unused Branches #16

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
52f14a2
Fix seed in tests
s-mandra May 31, 2024
49fa895
Fix seed in tests
s-mandra May 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 7 additions & 13 deletions include/pysa/sat/instance.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,23 +39,17 @@ auto GetRandomInstance(const std::size_t k, const std::size_t n,
using clause_type = std::vector<int>;

// Check
if (n < k)
throw std::runtime_error("'n' must be larger than 'k'");
if (n < k) throw std::runtime_error("'n' must be larger than 'k'");

// Get random seed
const std::size_t seed_ = seed.value_or(std::random_device()());

// Initialize random generator
std::mt19937_64 rng_(seed_);

#ifndef NDEBUG
std::cerr << "# Used seed: " << seed_ << std::endl;
#endif

// Initialize set of indexes
std::vector<int> indexes_(n);
for (std::size_t i_ = 0; i_ < n; ++i_)
indexes_[i_] = i_ + 1;
for (std::size_t i_ = 0; i_ < n; ++i_) indexes_[i_] = i_ + 1;

// Generate single clause
auto get_clause_ = [&rng_, &indexes_, k]() {
Expand All @@ -80,15 +74,15 @@ auto GetRandomInstance(const std::size_t k, const std::size_t n,
return clauses_;
}

template <typename Formula> auto GetNVars(Formula &&formula) {
template <typename Formula>
auto GetNVars(Formula &&formula) {
std::size_t max_ = 0;
for (const auto &clause_ : formula)
for (const auto &x_ : clause_) {
// All variables should be different from zero
if (x_ == 0)
throw std::runtime_error("All variables should be different from zero");
if (const std::size_t a_ = std::abs(x_); a_ > max_)
max_ = a_;
if (const std::size_t a_ = std::abs(x_); a_ > max_) max_ = a_;
}
return max_;
}
Expand Down Expand Up @@ -144,7 +138,7 @@ struct Instance {
last_var == other.last_var;
}

private:
private:
template <typename Formula>
static constexpr auto _Build(const Formula &formula) {
// Check all variables are different from zero
Expand Down Expand Up @@ -200,4 +194,4 @@ struct Instance {
return Instance{clauses_, signs_, last_var_};
}
};
} // namespace pysa::dpll::sat
} // namespace pysa::dpll::sat
24 changes: 19 additions & 5 deletions tests/test_dpll_sat.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,15 +46,29 @@ int main() {
if (mpi_rank_ == 0)
#endif
{
TestBranch();
std::size_t seed_;
seed_ = std::random_device()();
std::cerr << "# Seed: " << seed_ << std::endl;
TestBranch(seed_);
for (const auto &n_ : {8, 16, 32, 64, 96, 128, 142}) TestBitSet(n_);
TestDPLLSAT(3, 21, 60, std::size_t{1} << 20, true);
TestDPLLSAT(2, 21, 60, 10, true);
TestDPLLSAT(3, 21, 60, 0, true);
seed_ = std::random_device()();
std::cerr << "# Seed: " << seed_ << std::endl;
TestDPLLSAT(3, 21, 60, std::size_t{1} << 20, true, seed_);
seed_ = std::random_device()();
std::cerr << "# Seed: " << seed_ << std::endl;
TestDPLLSAT(2, 21, 60, 10, true, seed_);
seed_ = std::random_device()();
std::cerr << "# Seed: " << seed_ << std::endl;
TestDPLLSAT(3, 21, 60, 0, true, seed_);
}

#ifdef USE_MPI
TestDPLLSAT_MPI(3, 42, 3 * 42, 0, true);
{
std::size_t seed_;
seed_ = std::random_device()();
std::cerr << "# Seed: " << seed_ << std::endl;
TestDPLLSAT_MPI(3, 42, 3 * 42, 0, true);
}
#endif

// Finalize
Expand Down
18 changes: 10 additions & 8 deletions tests/test_dpll_sat.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,9 +141,9 @@ auto TestBitSet(const std::size_t n) {
}
}

auto TestBranch() {
auto TestBranch(std::optional<std::size_t> seed = std::nullopt) {
// Get random SAT problem
const auto formula_ = sat::GetRandomInstance(4, 20, 30);
const auto formula_ = sat::GetRandomInstance(4, 20, 30, seed);

// Get root
sat::Branch root_{formula_, 10};
Expand Down Expand Up @@ -190,9 +190,10 @@ auto TestBranch() {
}

auto TestDPLLSAT(std::size_t k, std::size_t n, std::size_t m,
std::size_t max_n_unsat, bool verbose = false) {
std::size_t max_n_unsat, bool verbose = false,
const std::optional<std::size_t> seed = std::nullopt) {
// Get random SAT problem
const auto formula_ = sat::GetRandomInstance(k, n, m);
const auto formula_ = sat::GetRandomInstance(k, n, m, seed);

// Get configurations from exhaustive enumeration
if (verbose) std::cerr << "# Start exhaustive enumeration ... ";
Expand Down Expand Up @@ -223,7 +224,8 @@ auto TestDPLLSAT(std::size_t k, std::size_t n, std::size_t m,

#ifdef USE_MPI
auto TestDPLLSAT_MPI(std::size_t k, std::size_t n, std::size_t m,
std::size_t max_n_unsat = 0, bool verbose = false) {
std::size_t max_n_unsat = 0, bool verbose = false,
std::optional<std::size_t> seed = std::nullopt) {
// Duplicate worlds
MPI_Comm mpi_comm_world;
MPI_Comm_dup(MPI_COMM_WORLD, &mpi_comm_world);
Expand All @@ -238,10 +240,10 @@ auto TestDPLLSAT_MPI(std::size_t k, std::size_t n, std::size_t m,
}();

// Get random formula
auto formula_ = [k, n, m, mpi_rank_ = mpi_rank_]()
-> decltype(sat::GetRandomInstance(0, 0, 0, 0)) {
auto formula_ = [k, n, m, mpi_rank_ = mpi_rank_,
seed]() -> decltype(sat::GetRandomInstance(0, 0, 0, 0)) {
if (mpi_rank_ == 0)
return sat::GetRandomInstance(k, n, m, std::random_device()());
return sat::GetRandomInstance(k, n, m, seed);
else
return {};
}();
Expand Down
Loading