101
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Efficient Partial Order CDCL Using Assertion Level Choice Heuristics

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We previously designed Partial Order Conflict Driven Clause Learning (PO-CDCL), a variation of the satisfiability solving CDCL algorithm with a partial order on decision levels, and showed that it can speed up the solving on problems with a high independence between decision levels. In this paper, we more thoroughly analyze the reasons of the efficiency of PO-CDCL. Of particular importance is that the partial order introduces several candidates for the assertion level. By evaluating different heuristics for this choice, we show that the assertion level selection has an important impact on solving and that a carefully designed heuristic can significantly improve performances on relevant benchmarks.

          Related collections

          Most cited references6

          • Record: found
          • Abstract: not found
          • Article: not found

          A machine program for theorem-proving

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Graph minors. II. Algorithmic aspects of tree-width

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              GRASP: a search algorithm for propositional satisfiability

                Bookmark

                Author and article information

                Journal
                1301.7676

                Theoretical computer science,Artificial intelligence
                Theoretical computer science, Artificial intelligence

                Comments

                Comment on this article