5 citations · 5 across the 6 of their papers we have counts for
11 papers · 1 filter
On the proof complexity of MCSAT
Gereon Kremer, Erika Abraham, Vijay Ganesh
Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical pro…
On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee +5
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap…
CDCL(Crypto) SAT Solvers for Cryptanalysis
Saeed Nejati, Vijay Ganesh
Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems…
The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
Curtis Bright, Dragomir Ž. Đoković, Ilias Kotsireas +1
In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectu…
SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Curtis Bright, Ilias Kotsireas, Vijay Ganesh
Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling…
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…