5 citations · 7 across the 4 of their papers we have counts for
4 papers
Conflict-Driven XOR-Clause Learning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Modern conflict-driven clause learning (CDCL) SAT solvers are very good in solving conjunctive normal form (CNF) formulas. However, some application problems involve lots of parity…
Classifying and Propagating Parity Constraints (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Parity constraints, common in application domains such as circuit verification, bounded model checking, and logical cryptanalysis, are not necessarily most efficiently solved if tr…
Simulating Parity Reasoning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. However, in some applicatio…
Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instanc…