| Name | rustsat JSON |
| Version |
0.4.3
JSON |
| download |
| home_page | None |
| Summary | This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance. |
| upload_time | 2024-02-23 08:25:56 |
| maintainer | None |
| docs_url | None |
| author | Christoph Jabs <christoph.jabs@helsinki.fi> |
| requires_python | >=3.7 |
| license | MIT |
| keywords |
sat
satisfiability
encodings
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
[](https://github.com/chrjabs/rustsat/actions/workflows/rustsat.yml)
[](https://crates.io/crates/rustsat)
[](https://docs.rs/rustsat)
[](https://pypi.org/project/rustsat)
[](./LICENSE)
<!-- cargo-rdme start -->
# rustsat - A Comprehensive SAT Library for Rust
`rustsat` is a collection of interfaces and utilities for working with the boolean satisfiability problem in Rust.
This library aims to provide implementations of elements commonly used in the development of software in the area of satisfiability solving.
The focus of the library is to provide as much ease of use without giving up on performance.
## Example
```rust
let mut instance: SatInstance = SatInstance::new();
let l1 = instance.new_lit();
let l2 = instance.new_lit();
instance.add_binary(l1, l2);
instance.add_binary(!l1, l2);
instance.add_unit(l1);
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_cnf(instance.as_cnf().0).unwrap();
let res = solver.solve().unwrap();
assert_eq!(res, SolverResult::Sat);
let sol = solver.full_solution().unwrap();
assert_eq!(sol[l1.var()], TernaryVal::True);
assert_eq!(sol[l2.var()], TernaryVal::True);
```
## Crates
The RustSAT project is split up into multiple crates that are all contained in [this repository](https://github.com/chrjabs/rustsat/).
These are the crates the project consists of:
| Crate | Description |
| --- | --- |
| `rustsat` | The main library, containing basic types, traits, encodings, parsers, and more. |
| `rustsat-tools` | A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see [this directory](https://github.com/chrjabs/rustsat/tree/main/tools/src/bin) with short descriptions of the tools in the headers of the files. |
| `rustsat-<satsolver>` | Interfaces to SAT solvers that can be used alongside `rustsat`. Currently interfaces are available for `cadical`, `kissat`, `glucose`, and `minisat`. |
## Installation
To use the RustSAT library as a dependency in your project, simply run `cargo add rustsat`.
To use an SAT solver interface in your project, run `cargo add rustsat-<satsolver>`.
Typically, the version of the SAT solver can be selected via crate features, refer to the documentation of the respective SAT solver crate for details.
To install the binary tools in `rustsat-tools` run `cargo install rustsat-tools`.
## Features
| Feature name | Description |
| --- | --- |
| `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |
| `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |
| `ipasir` | Include and link the IPASIR solver interface. |
| `optimization` | Include optimization (MaxSAT) data structures etc. |
| `multiopt` | Include data structures etc. for multi-objective optimization. |
| `compression` | Enable parsing and writing compressed input. |
| `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
| `rand` | Enable randomization features. (Shuffling clauses etc.) |
## Examples
For example usage refer to the small example tools in the [`rustsat-tools`
crate](https://crates.io/crates/rustsat_tools) at `tools/src/bin`. For a bigger
example you can look at this [multi-objective optimization
solver](https://github.com/chrjabs/scuttle).
For an example of how to use the C-API, see `rustsat/examples/capi*.cpp`.
Similarly, for an example of using the Python API, see `rustsat/examples/pyapi*.py`.
<!-- cargo-rdme end -->
Raw data
{
"_id": null,
"home_page": null,
"name": "rustsat",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.7",
"maintainer_email": null,
"keywords": "sat,satisfiability,encodings",
"author": "Christoph Jabs <christoph.jabs@helsinki.fi>",
"author_email": "Christoph Jabs <christoph.jabs@helsinki.fi>",
"download_url": "https://files.pythonhosted.org/packages/d1/e4/e3f8206c63cde25c87c817b155eaa91ba296c7d58812c345e00339ebb25c/rustsat-0.4.3.tar.gz",
"platform": null,
"description": "[](https://github.com/chrjabs/rustsat/actions/workflows/rustsat.yml)\n[](https://crates.io/crates/rustsat)\n[](https://docs.rs/rustsat)\n[](https://pypi.org/project/rustsat)\n[](./LICENSE)\n\n<!-- cargo-rdme start -->\n\n# rustsat - A Comprehensive SAT Library for Rust\n\n`rustsat` is a collection of interfaces and utilities for working with the boolean satisfiability problem in Rust.\nThis library aims to provide implementations of elements commonly used in the development of software in the area of satisfiability solving.\nThe focus of the library is to provide as much ease of use without giving up on performance.\n\n## Example\n\n```rust\nlet mut instance: SatInstance = SatInstance::new();\nlet l1 = instance.new_lit();\nlet l2 = instance.new_lit();\ninstance.add_binary(l1, l2);\ninstance.add_binary(!l1, l2);\ninstance.add_unit(l1);\nlet mut solver = rustsat_minisat::core::Minisat::default();\nsolver.add_cnf(instance.as_cnf().0).unwrap();\nlet res = solver.solve().unwrap();\nassert_eq!(res, SolverResult::Sat);\nlet sol = solver.full_solution().unwrap();\nassert_eq!(sol[l1.var()], TernaryVal::True);\nassert_eq!(sol[l2.var()], TernaryVal::True);\n```\n\n## Crates\n\nThe RustSAT project is split up into multiple crates that are all contained in [this repository](https://github.com/chrjabs/rustsat/).\nThese are the crates the project consists of:\n\n| Crate | Description |\n| --- | --- |\n| `rustsat` | The main library, containing basic types, traits, encodings, parsers, and more. |\n| `rustsat-tools` | A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see [this directory](https://github.com/chrjabs/rustsat/tree/main/tools/src/bin) with short descriptions of the tools in the headers of the files. |\n| `rustsat-<satsolver>` | Interfaces to SAT solvers that can be used alongside `rustsat`. Currently interfaces are available for `cadical`, `kissat`, `glucose`, and `minisat`. |\n\n## Installation\n\nTo use the RustSAT library as a dependency in your project, simply run `cargo add rustsat`.\nTo use an SAT solver interface in your project, run `cargo add rustsat-<satsolver>`.\nTypically, the version of the SAT solver can be selected via crate features, refer to the documentation of the respective SAT solver crate for details.\n\nTo install the binary tools in `rustsat-tools` run `cargo install rustsat-tools`.\n\n## Features\n\n| Feature name | Description |\n| --- | --- |\n| `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |\n| `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |\n| `ipasir` | Include and link the IPASIR solver interface. |\n| `optimization` | Include optimization (MaxSAT) data structures etc. |\n| `multiopt` | Include data structures etc. for multi-objective optimization. |\n| `compression` | Enable parsing and writing compressed input. |\n| `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |\n| `rand` | Enable randomization features. (Shuffling clauses etc.) |\n\n## Examples\n\nFor example usage refer to the small example tools in the [`rustsat-tools`\ncrate](https://crates.io/crates/rustsat_tools) at `tools/src/bin`. For a bigger\nexample you can look at this [multi-objective optimization\nsolver](https://github.com/chrjabs/scuttle).\n\nFor an example of how to use the C-API, see `rustsat/examples/capi*.cpp`.\nSimilarly, for an example of using the Python API, see `rustsat/examples/pyapi*.py`.\n\n<!-- cargo-rdme end -->\n\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance.",
"version": "0.4.3",
"project_urls": {
"Source Code": "https://github.com/chrjabs/rustsat"
},
"split_keywords": [
"sat",
"satisfiability",
"encodings"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "3445436f9285b71a3d52679113bdec8374973860feef1096eb03de36aa8151b1",
"md5": "5c5a7ffe424ad86a2039af006ec7dc33",
"sha256": "eeb8ed3b0f1537cc7fb07fed42a6cf2a49e31d6cc218ea9d30473f7fe4cdf819"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-macosx_10_12_x86_64.whl",
"has_sig": false,
"md5_digest": "5c5a7ffe424ad86a2039af006ec7dc33",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 352658,
"upload_time": "2024-02-23T08:25:54",
"upload_time_iso_8601": "2024-02-23T08:25:54.892626Z",
"url": "https://files.pythonhosted.org/packages/34/45/436f9285b71a3d52679113bdec8374973860feef1096eb03de36aa8151b1/rustsat-0.4.3-cp37-abi3-macosx_10_12_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "dbaa345a7314b322a63bf7f5b83b5391fca41577bb0a8964a8f342cfbe1d2660",
"md5": "148e8de69311ddbf6f4bd583e7385e60",
"sha256": "ecbd058363d058cd433aca07e7aee0348f73e68217e405af60a851e02d17c7f9"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-macosx_11_0_arm64.whl",
"has_sig": false,
"md5_digest": "148e8de69311ddbf6f4bd583e7385e60",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 342925,
"upload_time": "2024-02-23T08:25:52",
"upload_time_iso_8601": "2024-02-23T08:25:52.984552Z",
"url": "https://files.pythonhosted.org/packages/db/aa/345a7314b322a63bf7f5b83b5391fca41577bb0a8964a8f342cfbe1d2660/rustsat-0.4.3-cp37-abi3-macosx_11_0_arm64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "e01e63d8e0532536a9ceb8183b203ffa5b8db56e002299c55288a7dc4fc7f365",
"md5": "d77c7f442657b89b1aafd56615f54be2",
"sha256": "51111b535ae3fd1cd931852db6653759be9c9814aad7fa9cc26595e9cb3ea97f"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl",
"has_sig": false,
"md5_digest": "d77c7f442657b89b1aafd56615f54be2",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1116700,
"upload_time": "2024-02-23T08:25:41",
"upload_time_iso_8601": "2024-02-23T08:25:41.375475Z",
"url": "https://files.pythonhosted.org/packages/e0/1e/63d8e0532536a9ceb8183b203ffa5b8db56e002299c55288a7dc4fc7f365/rustsat-0.4.3-cp37-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "64545608b765f7779b2726ed080af29ee312c64ded599f8a0be2e817a2e7392d",
"md5": "7ed6d3db8aaba8103962f95ca65ece36",
"sha256": "bddef20ab58f93717c305feecd0ca68ea7ea0d12e150c96380b3cfb25360420d"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_17_armv7l.manylinux2014_armv7l.whl",
"has_sig": false,
"md5_digest": "7ed6d3db8aaba8103962f95ca65ece36",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1134267,
"upload_time": "2024-02-23T08:25:43",
"upload_time_iso_8601": "2024-02-23T08:25:43.500319Z",
"url": "https://files.pythonhosted.org/packages/64/54/5608b765f7779b2726ed080af29ee312c64ded599f8a0be2e817a2e7392d/rustsat-0.4.3-cp37-abi3-manylinux_2_17_armv7l.manylinux2014_armv7l.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "9dcba3eb474d0405134214e702a49fe932719dc3ad41c7373dd913369426cbcc",
"md5": "7d33c3bb90eb6fc11215c64e611ed6c3",
"sha256": "20317a1c2b85ea953986a35cd60c8eee68dfeadfacae5f338c2e2ccd9cb78648"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl",
"has_sig": false,
"md5_digest": "7d33c3bb90eb6fc11215c64e611ed6c3",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1240573,
"upload_time": "2024-02-23T08:25:45",
"upload_time_iso_8601": "2024-02-23T08:25:45.473747Z",
"url": "https://files.pythonhosted.org/packages/9d/cb/a3eb474d0405134214e702a49fe932719dc3ad41c7373dd913369426cbcc/rustsat-0.4.3-cp37-abi3-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "18848efa17303ab941598115dcf4daf1ca8d47b9cfe8142e95cce25ac20f691d",
"md5": "a28d6a60badbd80088ca0a92cbc79c75",
"sha256": "0ddd11b0571b2649f57de4d705674701139d29ad0bebb9dcf21c590465abc8c7"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_17_s390x.manylinux2014_s390x.whl",
"has_sig": false,
"md5_digest": "a28d6a60badbd80088ca0a92cbc79c75",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1291962,
"upload_time": "2024-02-23T08:25:47",
"upload_time_iso_8601": "2024-02-23T08:25:47.398631Z",
"url": "https://files.pythonhosted.org/packages/18/84/8efa17303ab941598115dcf4daf1ca8d47b9cfe8142e95cce25ac20f691d/rustsat-0.4.3-cp37-abi3-manylinux_2_17_s390x.manylinux2014_s390x.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "ff9690c858a01d96f12dc5b2b176f8c2e382de9d11f8e80efad39fa70b7dacaa",
"md5": "0579413957867a4ef737780011e763f6",
"sha256": "ddefabcde32024549dae2b6d9c0fc8198b60aaa335eaf3c956e27b92fe615842"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"has_sig": false,
"md5_digest": "0579413957867a4ef737780011e763f6",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1134410,
"upload_time": "2024-02-23T08:25:51",
"upload_time_iso_8601": "2024-02-23T08:25:51.635020Z",
"url": "https://files.pythonhosted.org/packages/ff/96/90c858a01d96f12dc5b2b176f8c2e382de9d11f8e80efad39fa70b7dacaa/rustsat-0.4.3-cp37-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "36e5d26eb44e65dc905c4a0b531d6489ea4f561e890e6fecf097441f10b6b4e5",
"md5": "a6cb7c8334a8cb227fcdd4b40a6c26b9",
"sha256": "a2f2c21b6cf84d8f7ef117e24387a13bc5dcebbda4d755d7be6986a658fd481d"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-manylinux_2_5_i686.manylinux1_i686.whl",
"has_sig": false,
"md5_digest": "a6cb7c8334a8cb227fcdd4b40a6c26b9",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 1156661,
"upload_time": "2024-02-23T08:25:49",
"upload_time_iso_8601": "2024-02-23T08:25:49.374747Z",
"url": "https://files.pythonhosted.org/packages/36/e5/d26eb44e65dc905c4a0b531d6489ea4f561e890e6fecf097441f10b6b4e5/rustsat-0.4.3-cp37-abi3-manylinux_2_5_i686.manylinux1_i686.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "1652b525e4bf9db75063c5c980dcf4730a4cb3ebc7d7b1e7f540bcdf85d96513",
"md5": "773d8c6b12047692e5e8f5db7e55a042",
"sha256": "5a800e700cd12a557d8eb6dc30f802f8057d0fecedfa54e8705f270612591c22"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-win32.whl",
"has_sig": false,
"md5_digest": "773d8c6b12047692e5e8f5db7e55a042",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 213944,
"upload_time": "2024-02-23T08:26:00",
"upload_time_iso_8601": "2024-02-23T08:26:00.659015Z",
"url": "https://files.pythonhosted.org/packages/16/52/b525e4bf9db75063c5c980dcf4730a4cb3ebc7d7b1e7f540bcdf85d96513/rustsat-0.4.3-cp37-abi3-win32.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "bec0d29e20a43ab9e3123f3e9965b1a7f7c4adacf6d021ad7a900067ad6b2dae",
"md5": "a5bfce8ad7611cf1eeabddbab1530383",
"sha256": "9b7695f1bac694f517ab5792cfaa8c2b9c42db0c4e0731c15c93f1ff5838428a"
},
"downloads": -1,
"filename": "rustsat-0.4.3-cp37-abi3-win_amd64.whl",
"has_sig": false,
"md5_digest": "a5bfce8ad7611cf1eeabddbab1530383",
"packagetype": "bdist_wheel",
"python_version": "cp37",
"requires_python": ">=3.7",
"size": 229476,
"upload_time": "2024-02-23T08:25:59",
"upload_time_iso_8601": "2024-02-23T08:25:59.489239Z",
"url": "https://files.pythonhosted.org/packages/be/c0/d29e20a43ab9e3123f3e9965b1a7f7c4adacf6d021ad7a900067ad6b2dae/rustsat-0.4.3-cp37-abi3-win_amd64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "d1e4e3f8206c63cde25c87c817b155eaa91ba296c7d58812c345e00339ebb25c",
"md5": "a6dcd5359269381de94c22fe6baa540e",
"sha256": "238d1b7c379802a21e4fe5c365b51e66f6485b18bac857d9970569344f6fcfe8"
},
"downloads": -1,
"filename": "rustsat-0.4.3.tar.gz",
"has_sig": false,
"md5_digest": "a6dcd5359269381de94c22fe6baa540e",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.7",
"size": 8463109,
"upload_time": "2024-02-23T08:25:56",
"upload_time_iso_8601": "2024-02-23T08:25:56.897358Z",
"url": "https://files.pythonhosted.org/packages/d1/e4/e3f8206c63cde25c87c817b155eaa91ba296c7d58812c345e00339ebb25c/rustsat-0.4.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-02-23 08:25:56",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "chrjabs",
"github_project": "rustsat",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "rustsat"
}
