Ising home status

SAT Solver

Introduction

The solver is an augmented electronic Ising machine for 3-SAT with bi-stable capacitive nodes and support for cubic interaction. Moreover, the solver runs our proposed semantic-aware annealing heuristic called tanh-make-break (TMB). Users can select between TMB or a biased random walk (BRW) heuristic. Please cite the paper in your publications if it helps your research:

Anshujit Sharma, Matthew Burns and Michael Huang, "Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT", in International Conference on Theory and Applications of Satisfiability Testing (SAT) 2023.

The solver is only for evaluation use.

Data and Benchmarks used in the SAT23 paper

Usage & Limitation

The input file should be in DIMACS CNF-SAT format ↗. A valid input file can be downloaded via this link ↗. When using the online solver, you can submit up to 10 repetitions for each task. You'll receive an email with the results once the task is completed.

Please consider adding hi@isingmodel.org to your contact list to prevent the email from being marked as spam.

Version history

Submit

Advanced parameters