simple-sat, 在 python 中,編寫了簡單的遞歸和迭代SAT求解器

分享于 

3分钟阅读

GitHub

  简体 双语
Simple recursive and iterative SAT solver written in Python.
  • 源代码名称:simple-sat
  • 源代码网址:http://www.github.com/sahands/simple-sat
  • simple-sat源代码文档
  • simple-sat源代码下载
  • Git URL:
    git://www.github.com/sahands/simple-sat.git
    Git Clone代码到本地:
    git clone http://www.github.com/sahands/simple-sat
    Subversion代码到本地:
    $ svn co --depth empty http://www.github.com/sahands/simple-sat
    Checked out revision 1.
    $ cd repo
    $ svn up trunk
    
    简单 SAT: 简单 python SAT求解器

    这个项目是一个简单的递归和迭代实现的回溯,基于观察的,SAT求解器。 代码基本上是基于knuth程序的,可以在这里找到 迭代代码的版本更接近于 knuth,但稍微复杂一点。 递归的版本相当简单。 主要是作为一个学习工具。

    附带的文章可以在 http://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html 找到。

    用法

    
    usage: sat.py [-h] [-v] [-a] [-b] [--output_filter OUTPUT_FILTER] [-r]
    
    
     [-i INPUT]
    
    
    
    Solve SAT instance by reading from stdin using an iterative or recursive
    
    
    watchlist-based backtracking algorithm. Iterative algorithm is used by
    
    
    default, unless the -r flag is given. Empty lines and lines starting with a #
    
    
    will be ignored.
    
    
    
    optional arguments:
    
    
     -h, --help show this help message and exit
    
    
     -v, --verbose verbose output.
    
    
     -a, --all output all possible solutions.
    
    
     -b, --brief brief output for assignemnts: outputs variables
    
    
     assigned 1.
    
    
     --output_filter OUTPUT_FILTER
    
    
     only output variables with namesstring with given
    
    
     string.
    
    
     -r, --recursive use the recursive backtracking algorithm.
    
    
     -i INPUT, --input INPUT
    
    
     read from given file instead of stdin.
    
    
    
    
    

    示例用法

    
    $ python sat.py -v --input tests/simple/02.in
    
    
    Current watchlist:
    
    
    1: 1 2 3, 1 ~2
    
    
    ~1:
    
    
    2:
    
    
    ~2:
    
    
    3:
    
    
    ~3: ~1 ~3
    
    
    Current assignment: ~1 ~2 ~3
    
    
    Clause ~1 ~3 contradicted.
    
    
    Found satisfying assignment.
    
    
    ~1 ~2 3
    
    
    
    
    

    相关文章