In Proceedings of the 12th NASA formal methods symposium (NFM’20)
Abstract In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.
In Proceedings of the 23rd international conference on theory and applications of satisfiability testing (SAT’20)
Abstract Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses” that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study.
Copyright (c) 2022, LRE; all rights reserved.
Template by Bootstrapious. Ported to Hugo by DevCows.
