arXiv 1505.024082015-05-10cs.LOcs.AI

DistMS: A Non-Portfolio Distributed Solver for Maximum Satisfiability

INESC-ID；Instituto Superior Técnico, Universidade de Lisboa（里斯本大学高等技术学院）

Miguel Neves, Inês Lynce, Vasco Manquinho

英文摘要：

The most successful parallel SAT and MaxSAT solvers follow a portfolio approach, where each thread applies a different algorithm (or the same algorithm configured differently) to solve a given problem instance. The main goal of building a portfolio is to diversify the search process being carried out by each thread. As soon as one thread finishes, the instance can be deemed solved. In this paper we present a new open source distributed solver for MaxSAT solving that addresses two issues commonly found in multicore parallel solvers, namely memory contention and scalability. Preliminary results show that our non-portfolio distributed MaxSAT solver outperforms its sequential version and is able to solve more instances as the number of processes increases.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Polsat: A Portfolio LTL Satisfiability Solver

In this paper we present a portfolio LTL-satisfiability solver, called Polsat. To achieve fast satisfiability checking for LTL formulas, the tool integrates four representative LTL solvers: pltl, TRP++, NuSMV, and Aalta. The idea of Polsat is to run the component solvers in parallel to get best overall performance; once one of the solvers terminates, it stops all other solvers. Remarkably, the Polsat solver utilizes the power of modern multi-core compute clusters. The empirical experiments show that Polsat takes advantages of it. Further, Polsat is also a testing plat- form for all LTL solvers…

2013-11-07cs.LO

给定计算时间限制下伪布尔优化的自动算法选择

Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits

Universidad de Concepción（康塞普西翁大学）；University of California, Berkeley（加州大学伯克利分校）；Universidad Técnica Federico Santa María（费德里科圣玛丽亚理工大学）

本研究针对伪布尔优化问题，设计了一种考虑用户指定计算时间限制的随时元求解器，通过广泛的实证证明其性能大幅优于组合中最佳单求解器Gurobi。

2023-09-07cs.AIcs.LO

parSAT：浮点可满足性的并行求解

parSAT: Parallel Solving of Floating-Point Satisfiability

本文提出parSAT方法，通过将浮点可满足性问题重新形式化并结合全局优化与多核并行执行，构建面向浮点算术的组合式半决策过程，以补充传统SMT求解器在非线性浮点约束求解中的不足。

2025-09-16cs.LO

HordeSat: A Massively Parallel Portfolio SAT Solver

A simple yet successful approach to parallel satisfiability (SAT) solving is to run several different (a portfolio of) SAT solvers on the input problem at the same time until one solver finds a solution. The SAT solvers in the portfolio can be instances of a single solver with different configuration settings. Additionally the solvers can exchange information usually in the form of clauses. In this paper we investigate whether this approach is applicable in the case of massively parallel SAT solving. Our solver is intended to run on clusters with thousands of processors, hence the name HordeSa…

2015-08-03cs.LO

可满足性模整数算术理论的局部搜索

Local Search For Satisfiability Modulo Integer Arithmetic Theories

开发了首个直接操作变量的SMT(IA)局部搜索算法LS-IA，设计针对整数算术的操作符、评分函数和两级选择启发式，实验证明其与Z3组合提升了SMT-LIB可满足基准集上的现有水平。

2023-05-17cs.LO

分布式SMT求解的划分策略

Partitioning Strategies for Distributed SMT Solving

针对并行SMT求解受限于串行性能的问题，本文提出多种新的分治划分策略，实验证明融入该策略的混合组合求解器在大量难例基准上性能显著优于传统组合方案。

2023-06-08cs.DCcs.LO

更多相关论文收起更多论文

Phase Selection Heuristics for Satisfiability Solvers

In general, a SAT Solver based on conflict-driven DPLL consists of variable selection, phase selection, Boolean Constraint Propagation, conflict analysis, clause learning and its database maintenance. Optimizing any part of these components can enhance the performance of a solver. This paper focuses on optimizing phase selection. Although the ACE (Approximation of the Combined lookahead Evaluation) weight is applied to a lookahead SAT solver such as March, so far, no conflict-driven SAT solver applies successfully the ACE weight, since computing the ACE weight is time-consuming. Here we apply …

2011-06-07cs.DMcs.LO

On Continuous Local BDD-Based Search for Hybrid SAT Solving

Rice University（莱斯大学）

We explore the potential of continuous local search (CLS) in SAT solving by proposing a novel approach for finding a solution of a hybrid system of Boolean constraints. The algorithm is based on CLS combined with belief propagation on binary decision diagrams (BDDs). Our framework accepts all Boolean constraints that admit compact BDDs, including symmetric Boolean constraints and small-coefficient pseudo-Boolean constraints as interesting families. We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS s…

2021-06-12cs.AIcs.ITcs.LG