Experimenting with SAT Solvers in Vampire

We perform formal verification of quantum circuits by integrating several techniques specialized to particular classes of circuits. Our verification methodology is based on the new notion of a reversible miter that allows one to leverage existing techniques for simplification of quantum circuits. For reversible circuits which arise as runtime bottlenecks of key quantum algorithms, we develop several verification techniques and empirically compare them. We also combine existing quantum verification tools with the use of SAT-solvers. Experiments with circuits for Shor's number-factoring algorithm, containing thousands of gates, show improvements in efficiency by four orders of magnitude.

Download Full-text

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2018/181 ◽

2018 ◽

Cited By ~ 5

Author(s):

Jan Elffers ◽

Jesús Giráldez-Cru ◽

Stephan Gocht ◽

Jakob Nordström ◽

Laurent Simon

Keyword(s):

Systematic Study ◽

Boolean Satisfiability ◽

Proof System ◽

Sat Solvers ◽

Proof Search ◽

Wide Range ◽

Clause Learning ◽

Resolution Proof ◽

Shed Light

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

Download Full-text

Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽

2018 ◽

Author(s):

Gilles Audemard ◽

Benoît Hoessen ◽

Saïd Jabbour ◽

Cédric Piette

Keyword(s):

Shared Memory ◽

State Of The Art ◽

Divide And Conquer ◽

Sat Solving ◽

Sat Solvers ◽

Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

Download Full-text

A Theory of Satisfiability-Preserving Proofs in SAT Solving

10.29007/tc7q ◽

2018 ◽

Author(s):

Adrián Rebola-Pardo ◽

Martin Suda

Keyword(s):

Propositional Logic ◽

Logical Truth ◽

Point Of View ◽

Traditional View ◽

Satisfiability Problem ◽

Sat Solving ◽

Sat Solvers ◽

Proof Systems ◽

Meta Level

We study the semantics of propositional interference-based proof systems such as DRAT and DPR. These are characterized by modifying a CNF formula in ways that preserve satisfiability but not necessarily logical truth. We propose an extension of propositional logic called overwrite logic with a new construct which captures the meta-level reasoning behind interferences. We analyze this new logic from the point of view of expressivity and complexity, showing that while greater expressivity is achieved, the satisfiability problem for overwrite logic is essentially as hard as SAT, and can be reduced in a way that is well-behaved for modern SAT solvers. We also show that DRAT and DPR proofs can be seen as overwrite logic proofs which preserve logical truth. This much stronger invariant than the mere satisfiability preservation maintained by the traditional view gives us better understanding on these practically important proof systems. Finally, we showcase this better understanding by finding intrinsic limitations in interference-based proof systems.

Download Full-text