Author name cluster

Massimo Narizzano

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

SAT Conference 2010 Conference Paper

sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning

Enrico Giunchiglia
Paolo Marin
Massimo Narizzano

Abstract In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines ( i ) variable elimination via Q-resolution, ( ii ) variable elimination via equivalence substitution and ( iii ) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing.

Details

SAT Conference 2009 Conference Paper

PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing

Matthew Lewis 0004
Paolo Marin
Tobias Schubert 0001
Massimo Narizzano
Bernd Becker 0001
Enrico Giunchiglia

Abstract In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multicore boxes to clusters and grids, to solve more relevant instances and faster than previous generation solvers. PaQuBE extends QuBE, its sequential core, by providing a Master/Slave Message Passing Interface (MPI) based design that allows it to split the problem up over an arbitrary number of distributed processes. Furthermore, PaQuBE ’s progressive parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be shared. According to the last QBF Evaluation, QuBE is the most powerful state-of-the-art QBF Solver. It was able to solve more than twice as many benchmarks as the next best independent solver. Our results here, show that PaQuBE provides additional speedup, solving even more instances, faster.

Details

JELIA Conference 2006 Conference Paper

The QBFEVAL Web Portal

Massimo Narizzano
Luca Pulina
Armando Tacchella

Abstract In this paper we describe the QBFEVAL web portal, an on-line resource supporting the participants and the organizers of the yearly evaluation of QBF solvers and instances.

Details

SAT Conference 2004 Conference Paper

QBF Reasoning on Real-World Instances

Enrico Giunchiglia
Massimo Narizzano
Armando Tacchella

During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains. Instances of this kind showed to be challenging for current state-of-the-art QBF solvers, while the ability to deal effectively with them is necessary to foster adoption of QBF-based reasoning in practice. In this paper we describe three reasoning techniques that we implemented in our solver Q U BE++ to increase its performances on real-world instances coming from formal verification and planning domains. We present experimental results that witness the contribution of each technique and the better performances of Q U BE++ with respect to other state-of-the-art QBF solvers. The effectiveness of Q U BE++ is further confirmed by experiments run on challenging real-world SAT instances, where Q U BE++ turns out to be competitive with respect to current state-ofthe-art SAT solvers.

Details

AIJ Journal 2003 Journal Article

Backjumping for Quantified Boolean Logic satisfiability

Enrico Giunchiglia
Massimo Narizzano
Armando Tacchella

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of them based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability (SAT). In this paper we show how it is possible to extend the conflict-directed backjumping schema for SAT to the satisfiability of QBFs: When applicable, conflict-directed backjumping allows search to skip over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same behavior for universally quantified literals. We show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for satisfiability of QBFs. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained. Summing up: We present the first algorithm that applies conflict and solution directed backjumping to QBF, and demonstrate the performance of this algorithm via an empirical study.

Details DOI

SAT Conference 2003 Conference Paper

Watched Data Structures for QBF Solvers

Ian P. Gent
Enrico Giunchiglia
Massimo Narizzano
Andrew G. D. Rowley
Armando Tacchella

Abstract In the last few years, we have seen a tremendous boost in the efficiency of SAT solvers, this boost being mostly due to Chaff. Chaff owes some of its efficiency to its “two-literal watching” data structure. In this paper we present watched data structures for Quantified Boolean Formula (QBF) satisfiability solvers. In particular, we propose ( i ) two Chaff -like literal watching schemes for unit clause detection; and ( ii ) two other watched data structures, one for detecting pure literals and the other for detecting void quantifiers. We have conducted an experimental evaluation of the proposed data structures, using both randomly generated and real-world benchmarks. Our results indicate that clause watching is very effective, while the 2 and 3 literal watching data structures become more effective as the clause length increases. The quantifier watching structure does not appear to be effective on the instances considered.

Details