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

11–20 of 58 posts

Re: SATisfying Solutions to Difficult Problems

#11

Post by tannhaeuser »

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.

Before you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer into your original domain language as you say).

Even simple goal-directed block's world-like robotic planning problems where the number of moves and the items to pickup/putdown are variable are much easier formulated and solved using Prolog.

Re: SATisfying Solutions to Difficult Problems

#12

Post by sirwhinesalot »

FreakLegion wrote: post #9
sirwhinesalot wrote: post #5

Earlier quoted context omitted.

Both are severely underused for sure. But it didn't help that for a long time open source MILP solvers were pretty mediocre. HiGHS didn't exist, SCIP was "non-commercial", CBC was ok but they've been having development struggles for awhile, GLPK was never even remotely close to commercial offerings. I think if something like Gurobi or Hexaly were open source, you'd see a lot more use since both their capabilities and…

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…

Didn't know about Randomized rounding. Is there any solver with built-in support for that? To turn a strong NLP solver into a fast but approximate MINLP solver?

Re: SATisfying Solutions to Difficult Problems

#13

Post by sirwhinesalot »

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 are rarely used directly, they're usually a core component of a more expressive solver type like an LCG solver or an SMT solver.

And if not that, then they are used as the core component of a custom solver that speaks some higher level domain language.

Encoding things in CNF is a pain (even with higher level APIs like PySAT). But it's not usually something you should be doing unless you are developing a solver of some sort yourself.

Re: SATisfying Solutions to Difficult Problems

#14

Post by fjfaase »

If you convert a sudoku to an exact cover you can usually solve it by finding colums that are a subset from another column and remove all rows that are only in one of them.

Sudokus that can be solved with reasoning alone, can be solved in polynomial time.

I recently discovered that solving exact covers, and probably also with SAT, using a generic strategy, does not always result in the most efficient way for finding solutions. There are problems that have 10^50 solutions, yer finding a solution can take a long time.

Re: SATisfying Solutions to Difficult Problems

#15

Post by ViscountPenguin »

muragekibicho wrote: post #4
ViscountPenguin wrote: post #3

I love SAT solvers, but way more underappreciated by software engineers are MILP solvers. MILPs (Mixed Integer Linear Programs) are basically sets of linear constraints, along with a linear optimization functions, where your variables can either be reals or ints. Notably, you can easily encode any SAT problem as a MILP, but it's much easier to encode optimization problems, or problems with "county" constraints as MIL…

SATs are cool but MILPs are cooler IMO. Lol I've been trying to train a neural network over a finite field, not the reals and oh my god MILPs are God's gift to us.

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.

Re: SATisfying Solutions to Difficult Problems

#17

Post by zvr »

FreakLegion wrote: post #9
sirwhinesalot wrote: post #5

Earlier quoted context omitted.

Both are severely underused for sure. But it didn't help that for a long time open source MILP solvers were pretty mediocre. HiGHS didn't exist, SCIP was "non-commercial", CBC was ok but they've been having development struggles for awhile, GLPK was never even remotely close to commercial offerings. I think if something like Gurobi or Hexaly were open source, you'd see a lot more use since both their capabilities and…

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?

Re: SATisfying Solutions to Difficult Problems

#18

Post by pfdietz »

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…

When I've tried using SAT (or SMT) solvers I've had issues with scalability. The solution times, even if they didn't increase exponentially, tended to go up as some higher polynomial (like, cubic) in the size of the initial problems I was trying them on.

Re: SATisfying Solutions to Difficult Problems

#19

Post by maweki »

tannhaeuser wrote: post #11
emil-lp wrote: post #10

Earlier quoted context omitted.

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.

Before you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer…

Incremental automatic grounding to SAT works fine for ASP.

Re: SATisfying Solutions to Difficult Problems

#20

Post by js8 »

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 ideal is all polynomials, the system is unsatisfiable (that's Nullstellenansatz). I don't understand how we can get high degree polynomials when running Grobner basis algorithm that specifically prefers low degree polynomials. It intuitively doesn't make sense.

Post reply on HN