> the intros really undersell how bad the experience of using SAT solvers directly is, the DIMACS sat file format makes me think of the year 1973
"MiniZinc" is the name of the Pythonic-ish-like syntax targeting (ie on-the-fly translating to) numerous different solvers (somewhere around half-a-dozen to a dozen or so, don't recall exactly =)
I had never used SAT before (was familiar with the concept) and recently wanted to avoid thinking, so I asked gemini (after a few test prompts):
"""Create a MiniZinc script to find the optimal E12-series resistor values for the base ($R_B$) and collector ($R_C$) of a PN2222A transistor switch.
Specifications:
Collector Voltage Supply ($V_{CC}$): 12V DC
Base (Input) Voltage ($V_{IN}$): 3.3V DC
Target Collector Current ($I_C$): Maximize, but do not exceed, 1W (1 watt).
The script must correctly model the circuit to ensure the transistor is in saturation and must execute without Gecode solver errors like 'Float::linear: Number out of limits"""
After a few more try-paste exception loops, that generated a lovely and readable MiniZinc script with variables I can adjust for other circuits. It was exciting to see that basically every constraint problem I learned in school ("at what angle should you swim across the river..." is just a matter of encoding the problem and running a solver (I still think people should learn the basics of constraint problems, but after a certain point the problems are just tricky enough that it makes more sense to teach people how solvers work, and how to encode problems for them...")
"MiniZinc" is the name of the Pythonic-ish-like syntax targeting (ie on-the-fly translating to) numerous different solvers (somewhere around half-a-dozen to a dozen or so, don't recall exactly =)