PropLogic::Sat4j
Using Sat4j solver to boost PropLogic, to practical level.
Note: This gem works only on JRuby.
Installation
Add this line to your application's Gemfile:
gem 'prop_logic-sat4j'And then execute:
$ bundle
Or install it yourself as:
$ gem install prop_logic-sat4j
Usage
This gem internally require PropLogic gem, and automatically replaces PropLogic.sat_sovler to this gem's PropLogic::Sat4j::Solver.
Once loaded, you can benefit from Sat4j speed without rewriting codes for PropLogic.
Incremental solver
In PropLogic.sat_loop and PropLogic::Term#each_sat, PropLogic::Sat4j::IncrementalSolver#add performs real incremental addition,
keeping learnt clauses.
Development
After checking out the repo, run bin/setup to install dependencies. Then, run bin/console for an interactive prompt that will allow you to experiment.
To install this gem onto your local machine, run bundle exec rake install. To release a new version, update the version number in version.rb, and then run bundle exec rake release to create a git tag for the version, push git commits and tags, and push the .gem file to rubygems.org.
Versioning
This gem is versioned respecting Sat4j's: Ver. a.b.c.d includes Sat4j Ver. a.b.c .
Contributing
- Fork it ( https://github.com/jkr2255/prop_logic-sat4j/fork )
- Create your feature branch (
git checkout -b my-new-feature) - Commit your changes (
git commit -am 'Add some feature') - Push to the branch (
git push origin my-new-feature) - Create a new Pull Request
License
The same license as Sat4j (EPL 1.0/LGPL >= 2.1) is applied to this gem.
This gem includes Sat4j Ver. 2.3.5 binary with no modifications. The source code of Sat4j is available at Sat4j project site.
