Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
From MaRDI portal
Publication:2360872
Recommendations
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- The SAT+CAS method for combinatorial search with applications to best matrices
- A SAT attack on the Erdős discrepancy conjecture
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
Cites work
- A Decision Procedure for Bit-Vectors and Arrays
- A SAT attack on the Erdős discrepancy conjecture
- Alloy*: a general-purpose higher-order relational constraint solver
- Compression of periodic complementary sequences and applications
- Connectivity of matching graph of hypercube
- CP(Graph): Introducing a Graph Computation Domain in Constraint Programming
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Engineering an efficient canonical labeling tool for large and sparse graphs
- Exploiting symmetry in SMT problems
- Fundamentals of parameterized complexity
- Hadamard ideals and Hadamard matrices with two circulant cores
- Hadamard matrices and their applications
- Hadamard matrices of the Williamson type of order 4\(\cdot m\), \(m=p\cdot q\) an exhaustive search for \(m=33\)
- Hadamard's determinant theorem and the sum of four squares
- Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
- scientific article; zbMATH DE number 3485806 (Why is no real title available?)
- scientific article; zbMATH DE number 1292563 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem
- Isabelle/HOL. A proof assistant for higher-order logic
- Lazy satisfiability modulo theories
- Logic for Programming, Artificial Intelligence, and Reasoning
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- On hypercube labellings and antipodal monochromatic paths
- On Orthogonal Matrices
- Perfect matchings extend to Hamilton cycles in hypercubes
- Perfect matchings extending on subcubes to Hamiltonian cycles of hypercubes
- Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity
- SAT modulo graphs: acyclicity
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- The CRC handbook of combinatorial designs
- The Magma algebra system. I: The user language
- Theory and Applications of Satisfiability Testing
- Williamson matrices of order \(4n\) for \(n = 33, 35, 39\)
Cited in
(12)- Extending perfect matchings to Gray codes with prescribed ends
- Investigating the existence of Costas Latin squares via satisfiability testing
- 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
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
- scientific article; zbMATH DE number 7056222 (Why is no real title available?)
- Matchings in hypercubes extend to long cycles
- SAT and lattice reduction for integer factorization
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
Describes a project that uses
Uses Software
This page was built for publication: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2360872)
