arXiv 1809.030972018-09-10cs.LO

A Comparison of BDD-Based Parity Game Solvers

Lisette Sanchez, Wieger Wesselink, Tim A. C. Willemse

备注：: In Proceedings GandALF 2018, arXiv:1809.02416
发表信息：: EPTCS 277, 2018, pp. 103-117
DOI：: 10.4204/EPTCS.277.8

英文摘要：

Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four parity game solving algorithms, viz. Zielonka's recursive algorithm, the more recent Priority Promotion algorithm, the Fixpoint-Iteration algorithm and the automata based APT algorithm. We compare their performance on several types of random games and on a number of cases taken from the Keiren benchmark set.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

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

继续探索

相关论文

Generating Extended Resolution Proofs with a BDD-Based SAT Solver

In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantific…

2023-03-27cs.LO

关于《基于BDD的桶消除的界》的注记

Notes on "Bounds on BDD-Based Bucket Elimination''

本文针对基于BDD的SAT求解器的不可满足性证明，通过实验验证Mengel提出的不同变量排序下鸽巢问题证明的$O(n^5)$多项式规模，同时确认同排序下的指数级增长特性。

2023-06-17cs.LO

Symbolic Parity Game Solvers that Yield Winning Strategies

Parity games play an important role for LTL synthesis as evidenced by recent breakthroughs on LTL synthesis, which rely in part on parity game solving. Yet state space explosion remains a major issue if we want to scale to larger systems or specifications. In order to combat this problem, we need to investigate symbolic methods such as BDDs, which have been successful in the past to tackle exponentially large systems. It is therefore essential to have symbolic parity game solving algorithms, operating using BDDs, that are fast and that can produce the winning strategies used to synthesize the …

2020-09-23cs.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

Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications

Existing approaches to synthesize reactive systems from declarative specifications mostly rely on Binary Decision Diagrams (BDDs), inheriting their scalability issues. We present novel algorithms for safety specifications that use decision procedures for propositional formulas (SAT solvers), Quantified Boolean Formulas (QBF solvers), or Effectively Propositional Logic (EPR). Our algorithms are based on query learning, templates, reduction to EPR, QBF certification, and interpolation. A parallelization combines multiple algorithms. Our optimizations expand quantifiers and utilize unreachable st…

2016-04-21cs.LO

基于消解的可交互证明系统用于不可满足性

A Resolution-Based Interactive Proof System for UNSAT

Technical University of Munich（慕尼黑工业大学）

本文通过将交互式证明系统与消解过程结合，提出了首个针对Davis-Putnam消解过程的交互协议，并证明了寻找竞争性交互协议可归结为寻找满足交换性质的公式算术化问题。

2026-05-21cs.LO

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

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers

Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion. Then we demonstrate how these new forms of attractors can be embedded within greatest fixed-point computations to design solvers of parity games that run in polynomial time but are partial in that the…

2014-05-19cs.LO

Partial Solvers for Parity Games: Effective Polynomial-Time Composition

Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial so…

2016-09-14cs.LO

Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)

Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instance is a combination of traditional clauses and parity constraints. This paper studies how such combined problems can be efficiently solved by augmenting a modern SAT solver with an xor-reasoning module in the DPLL(XOR) framework. A new xor-reasoning module that deduces all possible implied literals using incremental Gauss-Jordan elimination is presented. A decomposition technique that can greatly reduce the size of pa…

2012-09-08cs.LO

Simulating Parity Reasoning (extended version)

Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. However, in some application areas such as circuit verification, bounded model checking, and logical cryptanalysis, instances can have many parity (xor) constraints which may not be handled efficiently if translated to CNF. Thus, extensions to the CNF-driven search with various parity reasoning engines ranging from equivalence reasoning to incremental Gaussian elimination have been proposed. This paper studies how stronger parity reasoning tec…

2013-11-18cs.LO

Oink: an Implementation and Evaluation of Modern Parity Game Solvers

Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, as they are widely believed to admit a polynomial solution, but so far no such algorithm is known. In recent years, a number of new algorithms and improvements to existing algorithms have been proposed. We implement a new and easy to extend tool Oink, which is a high-performance implementation of modern parity game algorithms. We further present a comprehensive empirical evaluatio…

2018-03-05cs.GTcs.LO

使 $\ extsf{IP}=\ extsf{PSPACE}$ 实用化：面向 BDD 算法的高效交互式协议

Making $\textsf{IP}=\textsf{PSPACE}$ Practical: Efficient Interactive Protocols for BDD Algorithms

本文提出基于BDD的交互式协议，使证明者高效验证QBF计数问题，实现工具blic，在标准基准上与先进求解器竞争，验证开销小且错误概率极低。

2023-09-06cs.CCcs.LO

Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs

The dramatic improvements in combinatorial optimization algorithms over the last decades have had a major impact in artificial intelligence, operations research, and beyond, but the output of current state-of-the-art solvers is often hard to verify and is sometimes wrong. For Boolean satisfiability (SAT) solvers proof logging has been introduced as a way to certify correctness, but the methods used seem hard to generalize to stronger paradigms. What is more, even for enhanced SAT techniques such as parity (XOR) reasoning, cardinality detection, and symmetry handling, it has remained beyond rea…

2022-09-25cs.LO

Justifications and a Reconstruction of Parity Game Solving Algorithms

Parity games are infinite two-player games played on directed graphs. Parity game solvers are used in the domain of formal verification. This paper defines parametrized parity games and introduces an operation, Justify, that determines a winning strategy for a single node. By carefully ordering Justify steps, we reconstruct three algorithms well known from the literature.

2021-02-02cs.LO

Alpaga: A Tool for Solving Parity Games with Imperfect Information

Alpaga is a solver for two-player parity games with imperfect information. Given the description of a game, it determines whether the first player can ensure to win and, if so, it constructs a winning strategy. The tool provides a symbolic implementation of a recent algorithm based on antichains.

2009-01-29cs.GTcs.LO

Attracting Tangles to Solve Parity Games

Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, because they are widely believed to admit a polynomial solution, but so far no such algorithm is known. We propose a new algorithm to solve parity games based on learning tangles, which are strongly connected subgraphs for which one player has a strategy to win all cycles in the subgraph. We argue that tangles play a fundamental role in the prominent parity game solving algorithms…

2018-04-14cs.GTcs.LO

Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games

Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data. Solving a PBES is usually done by instantiation to a Parity Game and then solving the game. Practical game solvers exist, but the instantiation step is the bottleneck. We enhance the instantiation in two steps. First, we transform the PBES to a Parameterised Parity Game (PPG), a PBES with each equation either conjunctive or disjunctive. Then we use LTSmin, that offers transit…

2012-10-24cs.GTcs.LO

Hardware Acceleration for Boolean Satisfiability Solver by Applying Belief Propagation Algorithm

University of Michigan（密歇根大学）

Boolean satisfiability (SAT) has an extensive application domain in computer science, especially in electronic design automation applications. Circuit synthesis, optimization, and verification problems can be solved by transforming original problems to SAT problems. However, the SAT problem is known as NP-complete, which means there is no efficient method to solve it. Therefore, an efficient SAT solver to enhance the performance is always desired. We propose a hardware acceleration method for SAT problems. By surveying the properties of SAT problems and the decoding of low-density parity-check…

2016-03-16cs.AIcs.LO