Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

SATisfying Solutions to Difficult Problems

vaibhavsagar.com

Post reply on HN
Print view View original

21–30 of 58 posts

Re: SATisfying Solutions to Difficult Problems

#21

Post by sirwhinesalot »

js8 wrote: post #20

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated idea…

I have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving.

CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF.

A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.

Re: SATisfying Solutions to Difficult Problems

#22

Post by isolay »

This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. My homegrown solver finds all valuations that make a proposition true and then can eliminate redundancies, such that `X or not X and Y` gets simplified to `X or Y`, just to mention one example (proof: truth tables are identical). Are there any other SAT solvers out there that do something like that? My own one suffers from combinatorial explosion in the simplification stage when expressions get "complex" enough. But then, the simplification is NP-complete, AFAICT.

Re: SATisfying Solutions to Difficult Problems

#24

Post by egl2020 »

roenxi wrote: post #6

I've always been fascinated by how linear programming seems to be applicable to every problem under the sun but SAT solvers only really seem to be good at Sudoku. In practice that are a bunch of problems that seem to be SAT, but they are either SAT at a scale where the solver still can't find a solution in any reasonable time or they turn out to not really be SAT because there is that one extra constraint that is qui…

"SAT solvers only really seem to be good at Sudoku": if you use conda or uv, you've used an SAT solver.

Re: SATisfying Solutions to Difficult Problems

#25

Post by sirwhinesalot »

zvr wrote: post #17
FreakLegion wrote: post #9

Earlier quoted context omitted.

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…

Many thanks to you and the parent comment for providing names to search when looking for implementations. A basic question, before searching these: are they "input compatible"? I mean, can a problem be formulated once and then be solved by a variety of solvers? Or does each one of them use its own input language?

For MILP there isn't one single standard, but multiple competing solutions.

Nearly every solver supports the MPS format, but that's a really old format straight from the era of punchcards, it sucks.

Many solvers support the nl format, which is a low level format spat out by the AMPL tool (commercial software for mathematical modeling).

Many solvers support the CPLEX lp format, which is a nice human readable and writable format.

Google OR-Tools includes an API for mathematical modeling that supports the relevant open source MIP solvers plus Gurobi I think and its own CP solver. There are Python and Julia packages that try to do the same (rather than calling the solver APIs directly they usually spit out a problem in nl format though).

MiniZinc supports various open source MILP solvers plus various CP solvers. Very nice language, very high level.

For MINLP the only standard I know of is OSiL but support for it is spotty, mostly supported by open source tools I think.

Re: SATisfying Solutions to Difficult Problems

#26

Post by emil-lp »

isolay wrote: post #22

This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. My homegrown solver finds all valuations that make a proposition true and then can eliminate redundancies, such that `X or not X and Y` gets simplified to `X or Y`, just to mention one example (proof: truth tables are identical). Are there any other SAT solvers out there that do something like that? M…

It's not very difficult to turn a CDCL solver into an ALL-SAT solver, and there are many publications available doing exactly that.

Re: SATisfying Solutions to Difficult Problems

#27

Post by emil-lp »

js8 wrote: post #20

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated idea…

> I don't understand why SAT solvers don't use gaussian elimination more.

These are the types of questions that can easily be answered by simply trying.

Re: SATisfying Solutions to Difficult Problems

#28

Post by pxx »

emil-lp wrote: post #10
roenxi wrote: post #8

Earlier quoted context omitted.

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

Because you can encode many (actually all) problems as a SAT instance, and the answer to that sat instance can be translated into an answer for the original problem.

"All" isn't right.

You can only encode decision problems in NP into a SAT instance of polynomially-balanced size. Sure, that's a lot of things, but there are things provably not in this set.

Re: SATisfying Solutions to Difficult Problems

#29

Post by js8 »

sirwhinesalot wrote: post #21
js8 wrote: post #20

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated idea…

I have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving. CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF. A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.

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.

Re: SATisfying Solutions to Difficult Problems

#30

Post by taeric »

roenxi wrote: post #6

I've always been fascinated by how linear programming seems to be applicable to every problem under the sun but SAT solvers only really seem to be good at Sudoku. In practice that are a bunch of problems that seem to be SAT, but they are either SAT at a scale where the solver still can't find a solution in any reasonable time or they turn out to not really be SAT because there is that one extra constraint that is qui…

I'm curious if you have examples of problems you don't think they are good at solving? Agreed that they are not a panacea of solving problems, but if you are able to somewhat naturally reduce your problem to a SAT statement, they are silly tough to beat.
Post reply on HN