Satisfying Solutions to Difficult Problems

Huh, that's an interesting idea.

If you get sick of MILPs, maybe you could use a representation of your finite field instead of the field itself? That way you could do everything in C^n, and preserve differentiability to use SGD or something like it.

SCIP going Apache definitely improved the landscape, but Couenne (global MINLP), Bonmin (local MINLP), and IPOPT (local NLP, but e.g. [1] gets you MINLP) are solid and have been around for a long time. And anecdotally, I've seen a lot more issues with SCIP (presolvers and tolerances, mostly) than with other solvers. Still it's replaced Couenne in my toolbox, and Minotaur has replaced Bonmin, but IPOPT remains king of its domain.

1. E.g. https://en.wikipedia.org/wiki/Randomized_rounding.

    def objective(model: WtaModel) -> SumExpression:
        return sum(
            model.target_values[t_j]
            * prod(
                model.survival_rates[w_i][t_j]
                ** model.target_selected[w_i, t_j]
                for w_i in model.weapon_types
            )
            for t_j in model.targets
        )

At doing what, though? Why are they solving the SAT problem?

My experience is they respond yes/no very quickly for lots of problems, but as the problem approaches "probably narrowly solvable" the runtime goes exponential.

Are there open source examples of usage for real world problems, for example train scheduling or something else than software engineering practicioners might find relatable?

I confess I would expect a lot of those would be linear programming more than sat? Mixed integer would not surprise me.

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...")

I coded the paper Sinkhorn Solves Sudoku. Lol the most bizarre algorithms can solve sudoku. https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku

One way to recover XORs from 3SAT (AFAIK unfortunately DIMACS doesn't support XOR natively) is to use the formula:

(a | b | c) = ((a ^ ~x) | b) & (x | c)

where x is a variable that can be chosen. The LHS is satisfiable iff RHS is satisfiable. This gives you extra variable per clause, but you can eliminate some of them using GE. (Probably not an ideal approach to easy problems, but IMHO worth trying for the hard ones.)

Then you get a set of clauses that have what I call "generalized literals" - essentially a linear combination of literals - in clauses that only have 1 OR (I call this 2-XORSAT). These can be trivially transformed to intersection of XORSAT and 2SAT.

Another thing that DIMACS is missing, it's not very modular. So you cannot represent a bunch of conditions using already pre-solved XORSAT portion, and apply that to a new problem. (For example, we could encode a generic multiplier in SAT, relating inputs and outputs. Then we could presolve the XORSAT portion of the multiplier. Then we want to factorize a number. Well, just add a bunch of constants specifying output that needs to be satisfied and you don't need to solve the XORSAT for the multiplier again.)

Or, you can convert the 2-XORSAT into quadratic polynomials over Z_2 that all need to be equal to 0. Then you can use the Grobner basis algorithm to find whether these polynomials can be linearly combined (using polynomials as coefficients) to give 1 (i.e. they generate an ideal which contains the whole ring of polynomials), meaning the contradictory equation 1=0 has to be satisfied, and so the problem is unsatisfiable.

What I would really like to understand, how it can happen, if you are running the Grobner basis algorithm and keep an eye on the degree, that you build the degree up from low degree polynomials. It seems to me, if the problem is unsatisfiable, you should be always able to get by with polynomials of low degree, because why carry extra variables if you're gonna eliminate the terms anyway? (If low degree polynomials are sufficient for the Grobner basis, it would imply P=NP by the way, because there is only polynomial number of polynomials of a given maximum degree.)

But yeah CryptoMiniSAT looks somewhat promising.

Author of CryptoMiniSat here :) XOR+CNF is indeed supported by CryptoMiniSat. Which is cool, but if you _really_ think about it, the resolution operator over these two are gonna give you multivariate polynomials over GF(2). So resolution is poor in CryptoMiniSat, because it only encodes one of the constraints that this polynomial implies (i.e. one that can be encoded in a single disjunctive clause). And if you wanna do the _real_ deal, i.e. "properly" solve multivariate polynomials over GF(2) then you are in for a ride -- the all-powerful, much-feared, Grobner basis algorithms, and I am not touching those with a 100m pole, because they are hell on wheels :) I mean... it's possible to contribute to them, and I know of two people who did: https://theory.stanford.edu/~barrett/fmcad/slides/5_Kaufmann... and of course, https://link.springer.com/chapter/10.1007/978-3-031-37703-7_... i.e. Daniela and Alex. It's... rough :D

Just my 2 cents.

I agree they can be answered, but easily - no. The Grobner basis algorithm has been known for longer than NP problems, so it's not obvious why it wasn't used to solve SAT problems.

Surely. Maybe you can give me a counterexample. Let's just consider GF(2). Give me a set of generators with polynomials of degree <=2 over n variables, such that, 1 is a member of the ideal (i.e. generators generate the whole ring of polynomials) - so if I understand this correctly, Grobner basis is just 1, and, during the construction of the Grobner basis, you need to construct a polynomial of an arbitrarily high degree (or let's say degree 7). And there is no way to avoid this (or same degree) polynomial during the basis construction by finding a lower degree polynomial first.

See my problem? Somehow, I feel these syzygies need to be constructed from the degree 2 polynomials (the initial set), but then we can probably only work with the polynomials of the low degree instead, from which those syzygies are constructed.

To me, this is a very interesting question. Because if we can find the Grobner basis (even for just those ideals that coincide with the whole ring) in GF(2) in a way that we only need to construct polynomials of bounded degree, then there is a polynomial algorithm for SAT. Since most people believe there isn't such algorithm, I would really like to see a counterexample to this situation.

There is no catch - I even describe the reduction in another comment below. You can convert a 3SAT clause to a combination of XORSAT and 2SAT clauses. I am not mistaken, either, I used this reduction many times on practical problems, so I know it works. I encourage you to try it.

Unfortunately, putting the algorithms for XORSAT and 2SAT together is not trivial at all, they are quite different (but Grobner bases over GF(2) seem very promising in that).

But I agree that the fact that both XORSAT and 2SAT have polynomial algorithms is quite a strong indicator that full SAT has a one too. :-) (On the other hand, there is IMHO only very little actual evidence for P!=NP.)

I would also add that #SAT solvers, aiming at counting the number of solutions, are often implicitly solving the ALL-SAT in a more efficient manner than what you would have with modified CDCL solvers because they use other caching and decomposability techniques. Check knowledge compiler d4 for example https://github.com/crillab/d4v2 that can build some kind of circuits representing every solution in a factorized yet tractable way.

For problems with a very large number of solutions this quickly becomes inefficient. The blocking clauses will bog down the solver hard and waste tons of memory.

A more clever approach is to emulate depth-first search using a stack of assumption literals. The solver still retains learned conflict clauses so it's more efficient than naive DPLL.