Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Sebastian Fischer <sebf <at> informatik.uni-kiel.de>
Subject: ANN: incremental-sat-solver
Newsgroups: gmane.comp.lang.haskell.cafe
Date: Wednesday 28th January 2009 20:32:16 UTC (over 8 years ago)
Simple, Incremental SAT Solving as a Library
============================================

This Haskell library provides an implementation of the Davis-Putnam- 
Logemann-Loveland algorithm (cf. <http://en.wikipedia.org/wiki/DPLL_algorithm

 >) for the boolean satisfiability problem. It not only allows to  
solve boolean formulas in one go but also to add constraints and query  
bindings of variables incrementally.

The implementation is not sophisticated at all but uses the basic DPLL  
algorithm with unit propagation.

The package is available at:

   <http://hackage.haskell.org/cgi-bin/hackage-scripts/package/incremental-sat-solver

 >

Unlike 'sat' and 'sat-micro-hs' it is a library, and unlike 'libsat'  
it provides an interface for incremental solving. On the other hand,  
the implementation is much simpler (and probably less efficient) than  
'libsat's. You are invited to improve on that, if you like. The code  
is on github:

   <http://github.com/sebfisch/incremental-sat-solver>

Cheers,
Sebastian
 
CD: 3ms