Kissat SAT Solver

http://fmv.jku.at/kissat/

by veselin • 6 years ago

111 60 6 years ago

fmv.jku.at

HPsquared2• 6 years ago

To save the unwashed masses (myself included) any further internet searches, this relates to the Boolean satisfiability problem, which according to Wikipiedia [0] is:

"the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable."

I originally thought it was an AI to solve college placement tests, which would also have been cool but in a different way.

[0] https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

wiz21c• 6 years ago

SAT solvers are really powerful machines. You can fit many problems in a Boolean formula and then ask the solver to work it out. Now, the solver is not always optimized for your task but sometimes it helps. Also, the exercise of turning a problem into a (usually huge) Boolean formula is interesting. For example, I solved the "find a longest path in a graph" with a SAT solver (TBH, I quickly replaced that with a specialized solver, but, well, that was fun !)

PaulHoule• 6 years ago

SAT is the prototypical NP-complete problem.

jamestenglish• 6 years ago

Thank you! I clicked all the links on the page and still had no idea what SAT or the SAT Competition was!

andrepd• 6 years ago

This is very exciting! It not only has much improved performance, but it's also clean code, easily extensible for embedding in other applications (I do such a thing myself). Sadly I can't use it yet due to lack of incremental solving.

thechao• 6 years ago

If anyone else is wondering how the hell to use this thing... the main API is here:

    https://github.com/arminbiere/kissat/blob/master/src/kissat.h

In particular all you need to add clauses is this single API entry point:

    void kissat_add (kissat * solver, int lit);

The solver consists of the conjunction of disjunctions (I hope I have that correct — maybe the other way around? I can never remember). Variables are assumed to be any non-zero integer:

    kissat_add(s, [N != 0]);

You create a clause by repeatedly calling kissat_add; the clause is terminated by a 0. For instance if {shirt=1, tie=2}, then "!shirt or tie" is:

    kissat_add(s, -1); kissat_add(s, 2); kissat_add(s, 0);

Once the solver is run, if there's a solution, you get the solution using `kissat_val`:

    kissat_val(s, 1);
    kissat_val(s, 2);

I hope.

throwawaygh• 6 years ago

It supports the DIMACS input format [1], which you can parse using the kissat_parse_dimacs function [2].

DIMACS is a pretty terrible format, but at least you don't have to build the clauses up yourself using kissat_add.

[1] http://www.cs.utexas.edu/users/moore/acl2/manuals/current/ma...

[2] https://github.com/arminbiere/kissat/blob/master/src/parse.h

amelius2• 6 years ago

How do you interrupt the computation, e.g. when it takes too long?

mgraczyk• 6 years ago

You could always fork the process and send SIGKILL to the child after a timeout.

jwilk4• 6 years ago

SAT solvers use CNF (conjuction of disjunctions).

DNF-SAT can be trivially solved in O(n), because each clause directly encodes a solution (except for clauses that are contradictory, of course). But there's no known way to "convert" arbitrary formulas to DNF in polynomial time, so such a solver is not useful.

gallerdude• 6 years ago

Question: in college, I was lead to believe that a polynomial time SAT solver would be a huge breakthrough in many fields. Why is that the case? I know 3SAT is a reduction to NP problems, but besides that I feel like it wouldn't be particularly useful on its own.

IanCal• 6 years ago

I think that's it. If you can reduce your NP problems to 3SAT and 3SAT is in P then all P=NP.

teraflop• 6 years ago

If 3SAT is solvable in polynomial time, then P=NP. Which means that any problem that can be solved by brute-forcing an exponential number of possibilities (and doing a polynomial amount of checking for each) can also be solved with an asymptotically much smaller (polynomial) amount of work.

This includes anything from complicated optimization problems, to theorem proving, to inverting cryptographic hash functions, to any other NP algorithm that hasn't been thought up yet.

Whether this would have any practical use would depend on the polynomial exponents and constant factors, of course. But even in a theoretical sense it would be very, very surprising to a lot of people if it were true.

schoen2• 6 years ago

Donald Knuth apparently believes, in a very unusual view for a computer scientist, that P=NP but that the best algorithm has such bad exponents and factors that it won't have relevance for our computational practices -- if we're even able to discover it.

https://www.informit.com/articles/article.aspx?p=2213858&ran...

X6S1x6Okd1st• 6 years ago

It'd be a breakthrough, but only for problems big enough that the cost (polynomial & constant) of translating to and from SAT would be worth it for the problem at hand.

Also P=NP would be a very big deal.

tgflynn4• 6 years ago

I don't think the cost of the reduction is usually the problem. Most reductions to 3-SAT I've seen are either linear or can be made linear with a little work. For example any boolean circuit can be reduced to a <=3-SAT instance with a number of variables proportional to the number of gates.

The problem is that current solvers are heuristic and may fail or take too long (ie. degrade to exponential time) on any particular instance.

If a polynomial-time algorithm is ever discovered for all 3-SAT instances (ie. P = NP) then of course its actual complexity would be the determining factor.

xfer• 6 years ago

3SAT is a NP-complete problem which means if you can solve(not just check the solution) it in polynomial time, then you can solve all NP problems in polynomial time.

7373737373• 6 years ago

I wonder how big of an economic impact such improved algorithms have. Must be in the billions of dollars in the long run...

hinkley2• 6 years ago

Are there any software development problems we should be solving with SAT solvers instead of using heuristics?

klyrs• 6 years ago

Various sorts of scheduling problems come to mind... for example compilers can make good use of a fast sat solver; but typically you want a failover heuristic so you won't spend forever on large or unsolvable problems

dragontamer4• 6 years ago

Any problem that works.

IIRC: SAT Solvers regularly solve 30,000+ nodes of traveling salesman problem in just seconds (Or something along that magnitude. I forget exactly...). Yeah, its NP complete, but that doesn't mean its worthless.

It will take some experimentation to figure out if your problem is within the "feasible" category of SAT solving. I don't think there's any method aside from "try it, and if it works, be happy. If not, be sad".

If we knew which problems were easily solved with SAT-solvers, we probably would be well on our way to proving N == NP ?? So just guess and check.

--------------

Honestly, people may forget that brute-force solvers can be incredibly useful. When I was playing with a hash-algorithm I was inventing (just for fun on the side...) I searched the entire 32-bit space for the best integer that best mixed-up the bits from input to output. The brute-force solver took only seconds to try every 32-bit number.

We can brute-force a surprising number of "intractable" problems from our college years. Yeah, its inefficient, but who cares if its solved in seconds or minutes?

There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that).

jwilk4• 6 years ago

There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that).

Huh?

hinkley2• 6 years ago

You have to revalidate your assumptions from time to time.

I proved to a vendor they had screwed up CSPRNG seeding by doing a scatterplot of the first result from a large number of seeds. It ran so fast I bumped the loop counter up to max_int and it still ran in a minute or two on a laptop from 10 years ago.

When you can fit everything in cache, a CPU can sure run a lot of arithmetic in no time at all.

Iwan-Zotow• 6 years ago

So you could convert TSP to SAT, solve it in SAT and get result back as optimal path?

any link?

mhh__• 6 years ago

Not quite a problem as per se but it would be nice to have some kind of SMT solver inside a compiler to verify well-behaved-ness of certain functions. I'm not exactly sure whether you'd need something a bit more advanced for control flow analysis but beyond simple variable assignment checking (imagine Ada style bounds) I would quite like a language with a verifier like eBPF uses to reduce bug surface area (i.e. Not all code needs to be Turing complete). I think there are langauges with features like that but none aimed at mainstream use beyond research and/or defence etc.

I would like to write a language like that but I don't know enough about computer logic / hard ai etc. to know where to go in terms of the internals of the compiler (Bolting complicated analysis onto an existing compiler is really really ugly if there is a lot of global state - e.g. some parts of the D compiler although that's still WIP to be fair to the programmers)

vrnvu• 6 years ago

In recent years there has been a lot of improvement in refinement types which is, from what I understood, what you are describing. See for example Liquid Haskell that uses Z3 solver for static verification.

https://ucsd-progsys.github.io/liquidhaskell-blog/

I'd say that when dependent + refinement types get more mature and get pass the basic prototype idea in research languages/environments, these ideas could easily transfer to mainstream static typed languages and be a new module of future compilers.

dhash• 6 years ago

Stainless [0] does this well for Scala. You augment function definitions and return statements with `require()` and `assert()` respectivley.

[0] https://stainless.epfl.ch/

currymj• 6 years ago

here's a cool example from somebody at Microsoft:

https://medium.com/@ahelwer/checking-firewall-equivalence-wi...

it's not a pure SAT problem, but Z3 works (in a way I don't understand) by reducing constraint problems involving integers and even more complicated domains into SAT problems.

MaxBarraclough• 6 years ago

SMT solvers [0] like Z3 are very powerful things. They're used to power deductive software verification tools. We're discussing one such at [1].

[0] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

[1] https://news.ycombinator.com/item?id=23997128

Scaevolus• 6 years ago

Dart's package manager (Pub) uses an SAT solver to find possible solutions, and even more impressively, to describe why a dependency can't be fulfilled:

    Because dropdown >=2.0.0 depends on icons >=2.0.0 and root depends
  on icons <2.0.0, dropdown >=2.0.0 is forbidden.

    And because menu >=1.1.0 depends on dropdown >=2.0.0, menu >=1.1.0
  is forbidden.

    And because menu <1.1.0 depends on dropdown >=1.0.0 <2.0.0 which
  depends on intl <4.0.0, every version of menu requires intl
  <4.0.0.

    So, because root depends on both menu >=1.0.0 and intl >=5.0.0,
  version solving failed.

https://medium.com/@nex3/pubgrub-2fb6470504f

AegirLeet• 6 years ago

PHP's dependency manager, Composer, uses this approach too.

ufo• 6 years ago

If you have a combinatorial problem that your first inclination is to use a brute-force backtracking-based search then maybe you could you a SAT solver instead. It is a declarative way to solve the problem and good SAT solvers employ some very clever heuristics such as non-chronological backtracking and clause learning, which you might not get if you try to write the backtracking search yourself.

One example that I like is that some Linux package managers have switched to using a SAT solver to satisfy package version constraints.

caf• 6 years ago

woodruffw• 6 years ago

It depends on how you define "software development problem," but:

* SAT (more specifically, SMT) has been applied with some success to automated vulnerability discovery via symbolic execution. Underconstrained symex has cropped up more recently as a strategy for minimizing state space explosions.

* Others have mentioned register allocation, but SAT/SMT is broadly applicable to compilation problems: instruction selection and superoptimization[1] come to mind.

[1] https://github.com/google/souper

zimpenfish• 6 years ago

Not strictly software development but in the general area: routing cables between devices in a rack

https://web.archive.org/web/20190415054049/https://yurichev....

Inspired by that, I tried to use Z3 to solve the "best arrangement of letters on a linear typewriter" problem but never got a good answer because the solution space is far too large (26! which is seven hundred ninety-eight trillion, seven hundred twenty billion, nine hundred fifty-two million, one hundred seventy-six thousand, seven hundred and forty-five years at 16000 iterations a second.)

tgflynn4• 6 years ago

The idea is that for many problem instances the heuristic solvers can find a solution far more quickly than by exhaustive search, but maybe that wasn't the case for your particular problem.

ipnon• 6 years ago

Computational logic seems to be a more popular research subject in Europe than in the United States.

throwmemoney• 6 years ago

SAT Solvers are used in software that is used in creating the very complex Silicon Chips. Known as Formal in the semiconductor design industry.

schoen2• 6 years ago

For obscure reasons I know that this is the Finnish word for 'cats', and I wondered if there was any connection there. Apparently the answer is yes

https://github.com/arminbiere/kissat

or at least the developers have already noticed this coincidence for themselves.

psandersen• 6 years ago

I've been looking to get my feet wet with SAT and/or SMT solvers; can anyone recommend any short courses that I could start with to get a practical feel where where & how to use them? Python would be preferred.

Maybe this https://www.coursera.org/learn/automated-reasoning-sat would be a good start?

Ideally I would like to be able to take predicted outputs from ML plus business requirements to solve allocation problems; and more pie in the sky I would like to know enough to get inspiration for how to link a neural network with a sat solver, such as perhaps replacing or augmenting beam search in sequence decoding tasks.

Kissat SAT Solver

Related Stories