Data

Tools

Indexes

Applications

Experiments

Open Source Science

satinterface

Library to formulate SAT problems in .NET

https://github.com/sfiruch/satinterface

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Committers with academic emails
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (8.1%) to scientific vocabulary
Last synced: 8 months ago · JSON representation ·

Repository

Library to formulate SAT problems in .NET

Basic Info
  • Host: GitHub
  • Owner: sfiruch
  • License: mit
  • Language: C#
  • Default Branch: master
  • Size: 26.3 MB
Statistics
  • Stars: 6
  • Watchers: 3
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created over 9 years ago · Last pushed over 1 year ago
Metadata Files
Readme License Citation

README.md

License: MIT Build Status NuGet Package

SATInterface

SATInterface is a .NET library to formulate SAT problems

Installation

Add a reference to the NuGet Package deiruch.SATInterface.

Features

  • Maximize or minimize linear objective functions (3 strategies)
  • Enumerate all solutions
  • Supports linear combinations
  • Convenient .NET operator overloading
  • Simplify Boolean formulas
  • Translate Boolean formulas to CNF
  • Includes algorithms for
    • Counting (Totalizer)
    • At-most-one-constraints (7 implementations)
    • Exactly-one-constraints (9 implementations)
    • Exactly-k-constraints (4 implementations)
    • Unsigned integer arithmetic (Addition, Subtraction, Multiplication, Shifting)
  • Export to DIMACS files
  • Includes Kissat (https://github.com/arminbiere/kissat), CaDiCaL (https://github.com/arminbiere/cadical) and CryptoMiniSAT (see https://github.com/msoos/cryptominisat)

Usage example: Sudoku

~~~~cs using System; using System.Linq; using SATInterface;

using var m = new Model(); m.Configuration.Solver = InternalSolver.CaDiCaL; m.Configuration.Verbosity = 2;

var v = m.AddVars(9, 9, 9);

//fix the first number to 1 v[0, 0, 0] = true;

//here's alternative way to set the second number m.AddConstr(v[1, 0, 1]);

//assign one number to each cell for (var y = 0; y < 9; y++) for (var x = 0; x < 9; x++) m.AddConstr(m.Sum(Enumerable.Range(0, 9).Select(n => v[x, y, n])) == 1);

//each number occurs once per row (alternative formulation) for (var y = 0; y < 9; y++) for (var n = 0; n < 9; n++) m.AddConstr(m.ExactlyOneOf(Enumerable.Range(0, 9).Select(x => v[x, y, n])));

//each number occurs once per column (configured formulation) for (var x = 0; x < 9; x++) for (var n = 0; n < 9; n++) m.AddConstr(m.ExactlyOneOf(Enumerable.Range(0, 9).Select(y => v[x, y, n]), Model.ExactlyOneOfMethod.PairwiseTree));

//each number occurs once per 3x3 block for (var n = 0; n < 9; n++) for (var y = 0; y < 9; y += 3) for (var x = 0; x < 9; x += 3) m.AddConstr(m.Sum( v[x + 0, y + 0, n], v[x + 1, y + 0, n], v[x + 2, y + 0, n], v[x + 0, y + 1, n], v[x + 1, y + 1, n], v[x + 2, y + 1, n], v[x + 0, y + 2, n], v[x + 1, y + 2, n], v[x + 2, y + 2, n]) == 1);

m.Solve();

if (m.State == State.Satisfiable) for (var y = 0; y < 9; y++) { for (var x = 0; x < 9; x++) for (var n = 0; n < 9; n++) if (v[x, y, n].X) Console.Write($" {n + 1}"); Console.WriteLine(); } ~~~~

Owner

  • Name: Simon Felix
  • Login: sfiruch
  • Kind: user
  • Location: Switzerland
  • Company: Ateleris GmbH

Citation (CITATION.cff) 

cff-version: 1.2.0
title: SATInterface
message: Please cite this software using these metadata.
type: software
authors:
  - given-names: Simon
    family-names: Felix
    email: de@iru.ch
    orcid: 'https://orcid.org/0000-0002-3979-128X'
url: "https://github.com/deiruch/SATInterface"

GitHub Events

Total
  • Watch event: 1
Last Year
  • Watch event: 1

Committers

Last synced: almost 2 years ago

All Time
  • Total Commits: 289
  • Total Committers: 3
  • Avg Commits per committer: 96.333
  • Development Distribution Score (DDS): 0.007
Past Year
  • Commits: 87
  • Committers: 2
  • Avg Commits per committer: 43.5
  • Development Distribution Score (DDS): 0.011
Top Committers
Name Email Commits
Simon Felix de@i****h 287
Simon Felix sf@i****h 1
de de@C****0 1
Committer Domains (Top 20 + Academic)
iru.ch: 2

Issues and Pull Requests

Last synced: 8 months ago

All Time
  • Total issues: 0
  • Total pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Total issue authors: 0
  • Total pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 0
  • Pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
Top Labels
Issue Labels
Pull Request Labels

Dependencies

SATInterface/SATInterface.csproj nuget
  • ErrorProne.NET.CoreAnalyzers 0.4.0-beta.1 development
  • ErrorProne.NET.Structs 0.4.0-beta.1 development
  • Microsoft.Windows.CsWin32 0.1.691-beta development
Tests/Tests.csproj nuget
  • coverlet.collector 3.1.2 development
  • MSTest.TestAdapter 2.2.10
  • MSTest.TestFramework 2.2.10
  • Microsoft.NET.Test.Sdk 17.2.0
.github/workflows/dotnet.yml actions
  • actions/checkout v2 composite
  • actions/setup-dotnet v1 composite