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.
SATisfying Solutions to Difficult Problems
31–40 of 58 posts
Re: SATisfying Solutions to Difficult Problems
#32This 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
#33This 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…
> This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true.
Most, if not all, current SAT solvers are incremental. They allow you to add clauses on the fly.So, when you find the solution, you can add a (long!) clause that blocks that solution from appearing again and then run solver again.
Most, if not all, SAT solvers have a command line option for that enumeration done behind the scenes, for picosat it is "picosat --all".
Re: SATisfying Solutions to Difficult Problems
#34Earlier quoted context omitted.
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.…
The problem with this kind of constraints is that they are not local and really disturb CDCL based SAT solvers because you cannot remove the constraint unless you have fixed all its variables. Now, cryptominisat has a specific focus on this kind of constraints and implements ad-hoc routines to exploit this routine. cryptominisat is hence focused toward applications where this kind of constraint naturally appears, be it circuit synthesis or cryptography.
Now, CDCL solver is another beast. Gaussian elimination / Grobner basis are not implemented in these solvers simply because it is "too costly". One way of understanding why is just to reframe what one call SAT solver. This is not really a tool to solve SAT (hell, they can't even deal with the pigeon hole principle without preprocessing), the purpose of a SAT solver is to quickly solve instances coming from natural encoding of constraint systems. In this framework, unit propagation and clause learning are basically extremely efficient because they uncover hidden structure in the way, us human, encode constraint problems. Hence (CDCL) SAT solvers are highly efficient in many applications. But it is easy to kill one with a few variables by simply going out of this framework. For example, they are killers in solving packages dependencies because the structure of these problems matches this approach, CDCL solvers are then just an extremely refined way of bruteforcing your way through the search space.
Now, if your application heavily contains XOR-constraints, then it is likely a (CDCL) SAT solver is not the right approach. For circuit synthesis, some people use BDD based approach (where parity can be efficiently encoded) but sometimes you will simply have to develop your dedicated solver or use other solvers for other NP-complete problem that will have a different area of specialization (as already observed in many comments).
Re: SATisfying Solutions to Difficult Problems
#35This 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…
> This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. Most, if not all, current SAT solvers are incremental. They allow you to add clauses on the fly. So, when you find the solution, you can add a (long!) clause that blocks that solution from appearing again and then run solver again. Most, if not all, SAT solvers have a command line option for that en…
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.
Re: SATisfying Solutions to Difficult Problems
#36I 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.
Just my 2 cents.
Re: SATisfying Solutions to Difficult Problems
#37I'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…
PS: Yes, I develop a propositional SAT solver that used to be SOTA [1]. I nowadays develop a propositional model counter (for computing probabilities), that is currently SOTA [2]
[1] https://github.com/msoos/cryptominisat/ [2] https://github.com/meelgroup/ganak/
Re: SATisfying Solutions to Difficult Problems
#38Earlier quoted context omitted.
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 writa…
Re: SATisfying Solutions to Difficult Problems
#39Earlier quoted context omitted.
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.…
To efficiently encode XOR-constraint you will necessarily need extra variables (as you proposed) because we know that no bounded depth and polynomial size Boolean circuit can encode parity ("parity is not in AC0"). The problem with this kind of constraints is that they are not local and really disturb CDCL based SAT solvers because you cannot remove the constraint unless you have fixed all its variables. Now, cryptom…
Re: SATisfying Solutions to Difficult Problems
#40Earlier 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?
[1] https://jump.dev/ [2] https://jump.dev/JuMP.jl/stable/installation/#Supported-solv...