本文整理汇总了Python中sat.SAT_solver类的典型用法代码示例。如果您正苦于以下问题：Python SAT_solver类的具体用法？Python SAT_solver怎么用？Python SAT_solver使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了SAT_solver类的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_CustomGraphOneTwoCollors
def test_CustomGraphOneTwoCollors(self):
solver = SAT_solver()
graph = [[0, 1, 1, 1, 1], [1, 0, 1, 1, 0], [1, 1, 0, 1, 0], [1, 1, 1, 0, 1], [1, 0, 0, 1, 0]]
colors = 2
formula = graph_coloring(graph, colors)
solution = solver.solve(formula)
self.assertFalse(solution[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:8，代码来源:test_sat.py
示例2: test_completeGraphTwoCollors
def test_completeGraphTwoCollors(self):
solver = SAT_solver()
graph = [[1, 1, 1], [1, 1, 1], [1, 1, 1]]
colors = 2
formula = graph_coloring(graph, colors)
solution = solver.solve(formula)
self.assertFalse(solution[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:8，代码来源:test_sat.py
示例3: test_CustomGraphOneFourCollors
def test_CustomGraphOneFourCollors(self):
solver = SAT_solver()
graph = [[0, 1, 1, 1, 1], [1, 0, 1, 1, 0], [1, 1, 0, 1, 0], [1, 1, 1, 0, 1], [1, 0, 0, 1, 0]]
colors = 4
formula = graph_coloring(graph, colors)
solution = solver.solve(formula)
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:9，代码来源:test_sat.py
示例4: test_completeGraphThreeCollors
def test_completeGraphThreeCollors(self):
solver = SAT_solver()
graph = [[1, 1, 1], [1, 1, 1], [1, 1, 1]]
colors = 3
formula = graph_coloring(graph, colors)
solution = solver.solve(formula)
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:10，代码来源:test_sat.py
示例5: test_OddCicleGraphTwoCollors
def test_OddCicleGraphTwoCollors(self):
solver = SAT_solver()
graph = [
[0, 1, 1],
[1, 0, 1],
[1, 1, 0],
]
colors = 2
formula = graph_coloring(graph, colors)
solution = solver.solve(FlatCNF(formula))
self.assertFalse(solution[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:13，代码来源:test_sat_flat.py
示例6: test_EvenCicleGraphTwoCollors
def test_EvenCicleGraphTwoCollors(self):
solver = SAT_solver()
graph = [
[0, 1, 0, 1],
[1, 0, 1, 0],
[0, 1, 0, 1],
[1, 0, 1, 0],
]
colors = 2
formula = graph_coloring(graph, colors)
solution = solver.solve(FlatCNF(formula))
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:15，代码来源:test_sat_flat.py
示例7: test_SudokuCustom
def test_SudokuCustom(self):
solver = SAT_solver()
board=[[4, 8, None, 1, 6, None, None, None, 7],
[1, None, 7, 4, None, 3, 6, None, None],
[3, None, None, 5, None, None, 4, 2, None],
[None, 9, None, None, 3, 2, 7, None, 4],
[None, None, None, None, None, None, None, None, None],
[2, None, 4, 8, 1, None, None, 6, None],
[None, 4, 1, None, None, 8, None, None, 6],
[None, None, 6, 7, None, 1, 9, None, 3],
[7, None, None, None, 9, 6, None, 4, None]]
formula = sudoku(board)
solution = solver.solve(formula,True)
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:18，代码来源:test_sat_mt.py
示例8: test_SudokuMedium
def test_SudokuMedium(self):
solver = SAT_solver()
board=[[None, None, 9, None, 6, 4, None, None, 1],
[None, None, None, None, 5, None, None, None, None],
[4, 6, None, 1, None, 7, None, None, 8],
[None, None, None, None, None, None, None, 9, None],
[None, None, None, None, 3, None, None, 1, None],
[3, None, None, None, None, None, None, 4, None],
[None, 4, 8, None, None, None, 2, None, None],
[2, None, 7, None, 4, 5, None, 8, 6],
[5, None, None, None, None, None, None, None, None]]
formula = sudoku(board)
solution = solver.solve(FlatCNF(formula))
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:18，代码来源:test_sat_flat.py
示例9: test_SudokuEasy
def test_SudokuEasy(self):
solver = SAT_solver()
board=[[None, None, None, 4, None, None, None, 5, None],
[None, None, None, None, 1, None, 3, 6, None],
[None, None, 8, None, None, 6, 9, 4, 7],
[1, None, 2, None, None, None, None, 9, 5],
[None, 9, None, 2, None, 1, None, None, None],
[None, None, None, 5, 9, 3, None, None, None],
[4, None, None, None, None, None, 1, 7, 9],
[7, 2, None, 1, None, None, None, None, None],
[None, 8, None, None, None, 9, None, 2, None]]
formula = sudoku(board)
solution = solver.solve(FlatCNF(formula))
self.assertTrue(solution[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(solution[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:18，代码来源:test_sat_flat.py
示例10: SAT_solver
#!/usr/bin/env python
import sys
sys.path.append("./src")
from sat import SAT_solver
from sudoku import sudoku, printSudoku, processResult
print "================================================="
print "SUDOKU"
print "================================================="
solver = SAT_solver()
# define board as follows.
# board is array with nine arrays (rows).
# rows are arrays of nine elements.
# elements are None or int in [1,9].
# None - empty square.
board = [
[None, 8, None, 1, 6, None, None, None, 7],
[1, None, 7, 4, None, 3, 6, None, None],
[3, None, None, 5, None, None, 4, 2, None],
[None, 9, None, None, 3, 2, 7, None, 4],
[None, None, None, None, None, None, None, None, None],
[2, None, 4, 8, 1, None, None, 6, None],
[None, 4, 1, None, None, 8, None, None, 6],
[None, None, 6, 7, None, 1, 9, None, 3],
[7, None, None, None, 9, 6, None, 4, None],
]
开发者ID:urska19，项目名称:LVR-sat，代码行数:30，代码来源:sudoku_example.py
示例11: test_contradiction
def test_contradiction(self):
solver = SAT_solver()
formula = And([Var("A"), Not(Var("A"))])
result = solver.solve(formula)
self.assertFalse(result[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:5，代码来源:test_sat.py
示例12: test_Or
def test_Or(self):
solver = SAT_solver()
formula = Or([Var("A"), Var("B")])
result = solver.solve(formula)
self.assertTrue(result[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(result[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:6，代码来源:test_sat.py
示例13: test_variableNegation
def test_variableNegation(self):
solver = SAT_solver()
formula = Not(Var("A"))
result = solver.solve(formula)
self.assertTrue(result[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(result[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:6，代码来源:test_sat.py
示例14: test_false
def test_false(self):
solver = SAT_solver()
self.assertFalse(solver.solve(false())[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:3，代码来源:test_sat.py
示例15: test_true
def test_true(self):
solver = SAT_solver()
self.assertTrue(solver.solve(true())[0])
开发者ID:urska19，项目名称:LVR-sat，代码行数:3，代码来源:test_sat.py
示例16: SAT_solver
#!/usr/bin/env python
import sys
sys.path.append("./src")
from graphColoring import graph_coloring, printGraph, processResult
from sat import SAT_solver, FlatCNF
#instance of sat solver
solver = SAT_solver()
#graph represented with adjacency matrix
graph = [
[1, 1, 1],
[1, 1, 1],
[1, 1, 1],
]
#number of colors for graph coloring
colors = 3
#construct formula for certain graph and number of colors
formula = graph_coloring(graph, colors)
#solve formula
solution = solver.solve(formula)
#solve2 formula
solution2 = solver.solve(formula,True)
#flatcnf solution
solution3 = solver.solve(FlatCNF(formula))
开发者ID:urska19，项目名称:LVR-sat，代码行数:31，代码来源:graphColoring_example.py
示例17: unicode
print "Expression (p->True): " + unicode(newexpr2)
print "Expression (z->True): " + unicode(newexpr3)
print "================================================="
print "Testing deduplicate method."
print "================================================="
dedupexpr = And([ Or([Var("x1"), Var("x2")]) ])
print "Expession: " + unicode(dedupexpr) + " -> " + unicode(dedupexpr.deduplicate())
dedupexpr = And([ Or([Var("x1"), Var("x1")]) ])
print "Expession: " + unicode(dedupexpr) + " -> " + unicode(dedupexpr.deduplicate())
print "================================================="
print "================================================="
print "SAT Solver Testing"
print "================================================="
solver = SAT_solver()
for i in globals().keys():
if i[:4] == "expr":
print i, ":", unicode(globals()[i]), "->", solver.solve(globals()[i])
print unicode(true()), "->", solver.solve(true())
print "================================================="
print "sudoku"
board=[[4, 8, None, 1, 6, None, None, None, 7],
[1, None, 7, 4, None, 3, 6, None, None],
[3, None, None, 5, None, None, 4, 2, None],
[None, 9, None, None, 3, 2, 7, None, 4],
[None, None, None, None, None, None, None, None, None],
[2, None, 4, 8, 1, None, None, 6, None],
[None, 4, 1, None, None, 8, None, None, 6],
开发者ID:urska19，项目名称:LVR-sat，代码行数:31，代码来源:test.py
示例18: test_variable
def test_variable(self):
solver = SAT_solver()
formula = Var("A")
result = solver.solve(FlatCNF(formula))
self.assertTrue(result[0])
self.assertEqual("true", formula.nnf().cnf().evaluate(result[1]).__class__.__name__)
开发者ID:urska19，项目名称:LVR-sat，代码行数:6，代码来源:test_sat_flat.py
示例19: test_false
def test_false(self):
solver = SAT_solver()
self.assertFalse(solver.solve(FlatCNF(false()))[0],True)
开发者ID:urska19，项目名称:LVR-sat，代码行数:3，代码来源:test_sat_flat.py
示例20: test_true
def test_true(self):
solver = SAT_solver()
self.assertTrue(solver.solve(FlatCNF(true()))[0],True)
开发者ID:urska19，项目名称:LVR-sat，代码行数:3，代码来源:test_sat_flat.py
注：本文中的sat.SAT_solver类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论