Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer

DOI10.1007/978-3-319-40970-2_15zbMath1403.68226arXiv1605.00723OpenAlexW2345876752WikidataQ55969534 ScholiaQ55969534MaRDI QIDQ2818017

Victor W. Marek, Marijn J. H. Heule, Oliver Kullmann

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1605.00723

Mathematics Subject Classification ID

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (47)

Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture ⋮ A proof system for graph (non)-isomorphism verification ⋮ Online over time processing of combinatorial problems ⋮ Inductive logic programming at 30 ⋮ Nonexistence Certificates for Ovals in a Projective Plane of Order Ten ⋮ Optimal-depth sorting networks ⋮ Optimal bounds for the no-show paradox via SAT solving ⋮ Ramsey properties of nonlinear Diophantine equations ⋮ How to get more out of your oracles ⋮ Foundations for the Working Mathematician, and for Their Computer ⋮ Additive averages of multiplicative correlation sequences and applications ⋮ Formally proving size optimality of sorting networks ⋮ Square Coloring Planar Graphs with Automatic Discharging ⋮ Computer-aided constructions of commafree codes ⋮ Simulating strong practical proof systems with extended resolution ⋮ Truth Assignments as Conditional Autarkies ⋮ New ways to multiply \(3 \times 3\)-matrices ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ Finding Effective SAT Partitionings Via Black-Box Optimization ⋮ Finding the Hardest Formulas for Resolution ⋮ Optimal symmetry breaking for graph problems ⋮ Preprocessing of propagation redundant clauses ⋮ On propositional coding techniques for the distinguishability of objects in finite sets ⋮ Unnamed Item ⋮ Rado's criterion over squares and higher powers ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ The resolution of Keller's conjecture ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Strong extension-free proof systems ⋮ Computing Maximum Unavoidable Subgraphs Using SAT Solvers ⋮ Non-clausal redundancy properties ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ Unnamed Item ⋮ Incompleteness, Undecidability and Automated Proofs ⋮ DRAT Proofs for XOR Reasoning ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords ⋮ Covered clauses are not propagation redundant ⋮ The resolution of Keller's conjecture ⋮ Preprocessing of propagation redundant clauses ⋮ Say no to case analysis: automating the drudgery of case-based proofs ⋮ Deep cooperation of CDCL and local search for SAT ⋮ Investigating the existence of Costas Latin squares via satisfiability testing ⋮ XOR local search for Boolean Brent equations

Uses Software

Cites Work

This page was built for publication: Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer