Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
From MaRDI portal
Publication:2360872
DOI10.1007/s10817-016-9396-yzbMath1410.68413OpenAlexW2558199011WikidataQ123112521 ScholiaQ123112521MaRDI QIDQ2360872
Krzysztof Czarnecki, Vijay Ganesh, Curtis Bright, Edward Zulkoski, Albert Heinle, Ilias S. Kotsireas
Publication date: 29 June 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9396-y
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Nonexistence Certificates for Ovals in a Projective Plane of Order Ten ⋮ Extending perfect matchings to Gray codes with prescribed ends ⋮ Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords ⋮ Investigating the existence of Costas Latin squares via satisfiability testing
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Fundamentals of parameterized complexity
- Perfect matchings extending on subcubes to Hamiltonian cycles of hypercubes
- Hadamard matrices of the Williamson type of order 4\(\cdot m\), \(m=p\cdot q\) an exhaustive search for \(m=33\)
- The Magma algebra system. I: The user language
- Isabelle/HOL. A proof assistant for higher-order logic
- Williamson matrices of order \(4n\) for \(n = 33, 35, 39\)
- Alloy*: a general-purpose higher-order relational constraint solver
- Compression of periodic complementary sequences and applications
- Perfect matchings extend to Hamilton cycles in hypercubes
- On hypercube labellings and antipodal monochromatic paths
- Hadamard ideals and Hadamard matrices with two circulant cores
- Hadamard's determinant theorem and the sum of four squares
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- SAT Modulo Graphs: Acyclicity
- Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
- A SAT Attack on the Erdős Discrepancy Conjecture
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
- CP(Graph): Introducing a Graph Computation Domain in Constraint Programming
- Connectivity of Matching Graph of Hypercube
- On Orthogonal Matrices
- Exploiting Symmetry in SMT Problems
- Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs
- Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
- Theory and Applications of Satisfiability Testing
- A Decision Procedure for Bit-Vectors and Arrays
- Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity
- Logic for Programming, Artificial Intelligence, and Reasoning
- Hadamard matrices and their applications
This page was built for publication: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
