Navigation

satoku

satoku.py - SAT problem utilities

usage: satoku.py [OPTIONS] [filename]
or import satoku

Options

-s, –sort sort clause vectors (default for –matrix)
–no-sort do not sort clause vectors (default for –beautify)
–minimize minimize clauses (remove redundancies, resolve clauses)
–flatten expand each clause, converting a AND/OR/AND problem to a flat AND/OR problem.
–expand create full problem expansion (implies –sort)
–split split clause vectors into single-literal clauses (implied by –matrix)
-c, –conflicts maximize conflicts (implies –split, default for –matrix)
–no-conflicts do not maximize conflicts (default for –beautify)
–fast-conflicts maximize conflicts, fast conjunction cover (implies –conflicts)
–full-conflicts maximize conflicts, full conjunction cover (implies –conflicts)
–keep-min-problem keep minimal problem when maximizing conflicts (auto-detected by –fast-conflicts, –full_conflicts)
-x, –xor create XOR problem
–no-xor do not create XOR problem (default for –beautify)
-h, –header append HEADER (default)
–no-header do not append HEADER
-f, –footer append FOOTER (default)
–no-footer do not append FOOTER
-b, –beautify beautify clause vectors
-a, –annotate annotate clause vectors (AND/OR)
-m, –matrix create matrix (default)
–from-matrix parse matrix (implies –matrix)
–quick-convert dump Satoku Matrix after parsing and applying conversions (implies –matrix, –no-update)
-v, –variables map variables (default). With –from-matrix, it means that last region consists of mapped variables.
–no-variables do not map variables
–strip-variables dump Satoku Matrix without variables
-u, –update update state rows (default)
–no-update do not update state rows (disables several removal/solver options)
–immediate-zeroes immediately follow zero updates (default)
–delay-zeroes delay zero updates
–drop-1-states delete 1-state cell-matrix rows after requirement update (default for –update)
–keep-1-states do not delete 1-state cell-matrix rows after requirement update (default without –update)
–keep-2-states keep non-variable 2-state cell-matrix rows after requirement update (default)
–drop-2-states remove non-variable 2-state cell-matrix rows after requirement update (usually used with –update, –variables)
–drop-killed delete killed state rows (default)
–keep-killed do not delete killed state rows
-r, –redundant remove redundant cell-matrix rows (default)
–no-redundant do not remove redundant cell-matrix rows
–no-bin-conflicts do not combine binary conflict cell states (default)
–bin-conflicts combine binary conflict cell states (default)
–no-reduce-cells do not reduce cells (default)
–reduce-cells reduce cells (implies –bin-conflicts)
–strictly-less reduction must be strictly less space
–allow-equal reduction may use equal amount of space
–drop-uncombined drop uncombined cell states (default)
–keep-uncombined keep uncombined cell states
–no-minor-ccrs do not check minor conflict cell rows (default).
–check-minor-ccrs check minor conflict cell rows. Max. 2 possible states + min. 1 impossible state. Possibly re-triggers –reduce-cells.
-q, –quiet suppress warnings
-v, –verbose verbose test output
-d, –debug[=NUM] show debug information
-h, –help display this help message
–template list show available templates.
–eide[=COMM] Emacs IDE template list (implies –template list).
–template[=NAME] extract named template to standard output. Default NAME is -.
–extract[=DIR] extract adhoc files to directory DIR (default: .)
–explode[=DIR] explode script with adhoc in directory DIR (default __adhoc__)
–implode implode script with adhoc
-t, –test run doc tests

Obsolete Options:

–drop-snf-conflicts remove 2-states (deprecated, use –drop-2-states)

Module

See SatokuMatrix for examples.

Exports

>>> for ex in __all__:
...     printf(sformat('from {0} import {1}', __name__, ex))
from satoku import SatokuError
from satoku import SatokuUnsatisfied
from satoku import SatokuSatisfied
from satoku import SatokuDone
from satoku import ClauseVector
from satoku import Clause
from satoku import OrClause
from satoku import AndClause
from satoku import Problem
from satoku import SelRow
from satoku import SMRegion
from satoku import SMRegionIterator
from satoku import SMClause
from satoku import SMStats
from satoku import SatokuMatrix
from satoku import LoopMark
from satoku import parse_clauses_
from satoku import clean_clauses
from satoku import parse_clauses
from satoku import permute_cols
from satoku import dump_regions
exception satoku.SatokuError[source]
exception satoku.SatokuUnsatisfied[source]
exception satoku.SatokuSatisfied[source]
exception satoku.SatokuDone[source]
class satoku.ClauseVector(*args, **kwargs)[source]
>>> cv = ClauseVector('  [ 0 - - 1 - 0 ] // comment')
>>> printf(''.join((str(cv), cv.comment)))
0 _ _ 1 _ 0 // comment

>>> printf(cv.split())
[ 0 _ _ _ _ _ ]
[ _ _ _ 1 _ _ ]
[ _ _ _ _ _ 0 ]
annotate(clause_types=None)[source]

Index members.

Returns:self for chaining.
can_fold()[source]
Returns:True, if clause vector can fold. I.e., its used column count is 1.
conflicts_with(other)[source]
Returns:True, if self conflicts with other.
contains(other)[source]
Returns:True, if self contains other. 
>>> cv = ClauseVector('[ - 0 1 ]')

>>> ccv = ClauseVector('[ 1 0 1 ]')
>>> cv.contains(ccv)
True

>>> ccv = ClauseVector('[ 1 ]')
>>> cv.contains(ccv)
False

>>> cv = ccv
>>> ccv = ClauseVector('[ 1 0 1 ]')
>>> cv.contains(ccv)
True
copy()[source]
Returns:copy
equals(other)[source]
Returns:True, if self is equal to other. 
>>> cv = ClauseVector('[ - 0 1 ]')

>>> ccv = ClauseVector('[ 1 0 1 ]')
>>> cv.equals(ccv)
False

>>> ccv = ClauseVector('[ 1 ]')
>>> cv.equals(ccv)
False

>>> cv = ccv
>>> ccv = ClauseVector('[ 1 0 1 ]')
>>> cv.equals(ccv)
False

>>> cv = ccv
>>> cv.equals(ccv)
True
fold()[source]
Returns:ClauseVector.
has_one()[source]
Returns:True, if vector contains an unnegated variable. False otherwise.
has_zero()[source]
Returns:True, if vector has a negated variable. False otherwise.
index()[source]

Index members.

Returns:self for chaining.
key()[source]
Returns:sort key
max_conflicts()[source]

Maximize conflicts.

Returns:maximized clause. 
(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
max_depth()[source]
Returns:0
max_max_conflicts(full=None)[source]

Maximize conflicts including AND.

Returns:maximized clause.
max_used()[source]
Returns:len(self.used_cols)
max_width()[source]
Returns:len(self)
negate()[source]
Returns:self for chaining
parse_string(string)[source]
Returns:self for chaining.
remove_redundant()[source]
Returns:self for chaining.
sdiff(other)[source]

Single difference column.

Returns:(single difference column, shorter, longer) or (-1, shorter, longer). 
>>> cv = ClauseVector('[ - 0 0 ]')

>>> ccv = ClauseVector('[ 1 ]')
>>> cv.sdiff(ccv)
(-1, [1], [-1, 0, 0])

>>> ccv = ClauseVector( '[ 1 0 1 ]')
>>> cv.sdiff(ccv)
(2, [-1, 0, 0], [1, 0, 1])

>>> ccv.sdiff(cv)
(2, [-1, 0, 0], [1, 0, 1])

>>> cv = ClauseVector( '[ 1 1 1 ]')
>>> cv.sdiff(ccv)
(1, [1, 1, 1], [1, 0, 1])

>>> cv = ClauseVector( '[ 1 1 1 ]')
>>> ccv = ClauseVector('[ 0 0 1 ]')
>>> cv.sdiff(ccv)
(-1, [1, 1, 1], [0, 0, 1])

>>> cv = ClauseVector( '[ 1 1 1 - ]')
>>> ccv = ClauseVector('[ - 0 1 0 ]')
>>> cv.sdiff(ccv)
(-1, [1, 1, 1, -1], [-1, 0, 1, 0])

>>> cv = ClauseVector( '[ 1 0 - 1 ]')
>>> ccv = ClauseVector('[ - 1 0 - ]')
>>> cv.sdiff(ccv)
(-1, [-1, 1, 0, -1], [1, 0, -1, 1])
set_width(width=-1)[source]

Set width.

Returns:self for chaining.
sort()[source]
Returns:self for chaining.
sort_by_index()[source]
Returns:self for chaining.
split()[source]
Returns:Clause.
update_cols()[source]
Returns:self for chaining.
xor_conflicts()[source]

XOR conflicts.

Returns:clause with XOR conflicts. 
(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
class satoku.Clause(*args, **kwargs)[source]

Clause of clause vectors.

Parameters:progress – progress output (keyword only!) 
>>> cl = Clause('1 - 0 - 0').fold().split()
>>> printf(cl)
[ 1 _ _ _ _ ]
[ _ _ 0 _ _ ]
[ _ _ _ _ 0 ]
add_cv(cv)[source]

Add copy of clause vector.

Returns:self for chaining.
annotate(clause_types=None)[source]

Index members.

Returns:self for chaining.
can_fold()[source]
Returns:True, if clause vector can fold. I.e., its used column count is 1.
conflicts_with(other)[source]
Returns:True, if self conflicts with other.
contains(other)[source]
Returns:True, if self contains other.
copy()[source]
Returns:copy
equals(other)[source]
Returns:True, if self contains other.
expand()[source]

Expand clause vectors in place.

Returns:distributive expansion of clause vectors. (AND(OR()) -> OR(AND()), OR(AND()) -> AND(OR())) 
>>> cl = Problem('[[1 0 - - - - ][ - - 1 0 - - ][ - - - - 1 0 ]]')[0]
>>> printf(cl)
[ 1 0 _ _ _ _ ]
[ _ _ 1 0 _ _ ]
[ _ _ _ _ 1 0 ]

>>> exp = cl.expand()
>>> printf(exp)
[ 1 _ 1 _ 1 _ ]
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ 1 _ ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]

>>> cl = Problem('[1 0 1 ]').split()[0]
>>> printf(cl)
[ 1 _ _ ]
[ _ 0 _ ]
[ _ _ 1 ]

>>> exp = cl.expand()
>>> printf(exp)
[ 1 0 1 ]

>>> cl = Problem('[[ 1 _ _ ][ 0 0 _ ][ 0 1 1 ]]').split()[0]
>>> printf(cl)
[ 1 _ _ ]
[ 0 0 _ ]
[ 0 1 1 ]

>>> exp = cl.expand()
>>> printf(exp)
[ 1 0 1 ]

>>> exp = exp.expand()
>>> printf(exp)
[ 1 _ _ ]
[ _ 0 _ ]
[ _ _ 1 ]
fold()[source]
Returns:folded ClauseVector.
has_one()[source]
Returns:True, if any sub-clause/vector has an unnegated variable. False otherwise.
has_zero()[source]
Returns:True, if any sub-clause/vector has a negated variable. False otherwise.
index()[source]

Index members.

Returns:self for chaining.
key()[source]
Returns:sort key
max_conflicts()[source]

Maximize conflicts.

Returns:maximized clause. 
(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
max_depth()[source]
Returns:max depth of sub-clauses/vectors 
>>> pr = Problem()
>>> printf(pr.max_depth())
0

>>> pr = Problem('[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ]')
>>> printf(pr.max_depth())
1

>>> pr = Problem('[[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ]]')
>>> printf(pr.max_depth())
2

>>> pr = Problem('[[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ] [[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ]]]')
>>> printf(pr.max_depth())
3
max_max_conflicts(full=None)[source]

Maximize conflicts including clauses.

Returns:maximized clause. 
(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
  ((l0 & l1) | (l2 & l3) | (l4 & l5))
= ((l0 & l1) |
   (!l0 & l2 & l3) | (!l1 & l2 & l3) |
   (!l0 & !l2 & l4 & l5) | (!l1 & !l2 & l4 & l5) |
   (!l0 & !l3 & l4 & l5) | (!l1 & !l3 & l4 & l5))

[
  [ 1 1 _ _ _ _ ]
  [ _ _ 1 1 _ _ ]
  [ _ _ _ _ 1 1 ]
]

=>

[
  [ 1 1 _ _ _ _ ]
  [ 0 _ 1 1 _ _ ]
  [ _ 0 1 1 _ _ ]
  [ 0 _ 0 _ 1 1 ]
  [ 0 _ _ 0 1 1 ]
  [ _ 0 0 _ 1 1 ]
  [ _ 0 _ 0 1 1 ]
]
>>> pr = Problem('[ 1 1 1 ] [0 _ 1 1 ]')
>>> ign = pr.max_max_conflicts()
>>> printf(pr)
[
  [ 1 _ _ ]
  [ 0 1 _ ]
  [ 0 0 1 ]
]
[
  [ 0 _ _ _ ]
  [ 1 _ 1 _ ]
  [ 1 _ 0 1 ]
]

>>> pr = Problem('[[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ]]')
>>> printf(pr)
[
  [ 1 1 _ _ _ _ ]
  [ _ _ 1 1 _ _ ]
  [ _ _ _ _ 1 1 ]
]

>>> ign = pr.max_max_conflicts()
>>> printf(pr)
[
  [ 1 1 _ _ _ _ ]
  [ 0 _ 1 1 _ _ ]
  [ _ 0 1 1 _ _ ]
  [ 0 _ 0 _ 1 1 ]
  [ 0 _ _ 0 1 1 ]
  [ _ 0 0 _ 1 1 ]
  [ _ 0 _ 0 1 1 ]
]

>>> pr = Problem('[[ 1 1 _ _ _ _ ] [ _ _ 1 1 _ _ ] [ _ _ _ _ 1 1 ]]')
>>> ign = pr.max_max_conflicts(full=True)
>>> printf(pr)
[
  [ 1 1 _ _ _ _ ]
  [ 0 0 1 1 _ _ ]
  [ 0 1 1 1 _ _ ]
  [ 1 0 1 1 _ _ ]
  [ 0 0 0 0 1 1 ]
  [ 0 0 0 1 1 1 ]
  [ 0 0 1 0 1 1 ]
  [ 0 1 0 0 1 1 ]
  [ 0 1 0 1 1 1 ]
  [ 0 1 1 0 1 1 ]
  [ 1 0 0 0 1 1 ]
  [ 1 0 0 1 1 1 ]
  [ 1 0 1 0 1 1 ]
]

>>> pr = Problem('[[ 1 1 _ _ ] [ _ 1 1 _ ] [ _ _ 1 1 ]]')
>>> ign = pr.max_max_conflicts()
>>> printf(pr)
[
  [ 1 1 _ _ ]
  [ 0 1 1 _ ]
  [ 0 0 1 1 ]
  [ _ 0 1 1 ]
]

>>> pr = Problem('[[ 1 1 _ _ ] [ _ 0 1 _ ] [ _ 0 _ _ 1 ]]').set_width()
>>> printf(pr)
[
  [ 1 1 _ _ _ ]
  [ _ 0 1 _ _ ]
  [ _ 0 _ _ 1 ]
]
Conflicting negations: duplicate
Conflicting merges: drop
keep longest!
>>> mpr = pr.copy().max_max_conflicts()
>>> printf(mpr)
[
  [ 1 1 _ _ _ ]
  [ 0 0 1 _ _ ]
  [ _ 0 1 _ _ ]
  [ 0 0 0 _ 1 ]
  [ _ 0 _ _ 1 ]
  [ _ 0 0 _ 1 ]
]

old:

[
  [ 1 1 _ _ _ ]
  [ 0 0 1 _ _ ]
  [ _ 0 1 _ _ ]
  [ 0 0 0 _ 1 ]
  [ _ 0 0 _ 1 ]
]
----------
[ 1 1 _ _ _ _ ]

[ 0 _ _ _ _ _ ]
[ _ 0 _ _ _ _ ]

----------
[ _ 0 1 _ _ _ ]

[ _ 1 _ _ _ _ ]
[ _ _ 0 _ _ _ ]

----------
[ _ 0 _ _ 1 _ ]

[ _ 1 _ _ _ _ ]
[ _ _ _ _ 0 _ ]
----------
[ 1 1 _ _ _ _ ]

[ 0 _ _ _ _ _ ]
[ _ 0 _ _ _ _ ]

----------
[ 0 0 1 _ _ _ ]
[ _ 0 1 _ _ _ ]

[ 0 1 _ _ _ _ ]
[ 0 _ 0 _ _ _ ]
[ _ 0 _ _ _ _ ]
[ _ 1 _ _ _ _ ]
[ _ 0 0 _ _ _ ]

----------

[ 0 0 0 _ 1 _ ]
[ _ 0 _ _ 1 _ ]
[ _ 0 0 _ 1 _ ]
>>> mpr = pr.copy().max_max_conflicts(full=True)
>>> printf(mpr)
[
  [ 1 1 _ _ _ ]
  [ 0 0 1 _ _ ]
  [ 1 0 1 _ _ ]
  [ 0 0 1 _ 1 ]
  [ 0 0 0 _ 1 ]
  [ 1 0 0 _ 1 ]
  [ 1 0 1 _ 1 ]
]

old:

[
  [ 1 1 _ _ _ ]
  [ 0 0 1 _ _ ]
  [ 1 0 1 _ _ ]
]
----------
[ 1 1 _ _ _ _ ]

[ 0 0 _ _ _ _ ]
[ 0 1 _ _ _ _ ]
[ 1 0 _ _ _ _ ]

----------
[ _ 0 1 _ _ _ ]

[ 0 0 1 _ _ _ ]
[ 1 0 1 _ _ _ ]

[ 0 0 0 _ _ _ ]
[ 0 0 1 _ _ _ ]
[ 0 1 1 _ _ _ ]
[ 0 0 1 _ _ _ ]

[ 0 1 0 _ _ _ ]
[ 0 0 0 _ _ _ ]
[ 0 1 1 _ _ _ ]
[ 0 0 1 _ _ _ ]
[ 0 1 1 _ _ _ ]

[ 1 0 0 _ _ _ ]
[ 1 0 1 _ _ _ ]
[ 1 0 1 _ _ _ ]
[ 1 1 1 _ _ _ ]

=>

[ 0 0 0 _ _ _ ]
[ 0 0 1 _ _ _ ]
[ 0 1 0 _ _ _ ]
[ 0 1 1 _ _ _ ]
[ 1 0 0 _ _ _ ]
[ 1 0 1 _ _ _ ]
[ 1 1 1 _ _ _ ]

----------
[ _ 0 _ _ 1 _ ]

[ 0 0 0 _ 1 _ ]
[ 0 0 1 _ 1 _ ]
[ 1 0 0 _ 1 _ ]
[ 1 0 1 _ 1 _ ]
max_used()[source]
Returns:max number of used columns in sub-clauses/vectors
max_width()[source]
Returns:max width of sub-clauses/vectors
minimize(sort=None)[source]

Minimize in place.

Returns:self for chaining.
Parameters:sort – if True, also sort clause. 
>>> cl = Problem('[ _ 1 _ 1 1 ][ 1 - 0 1 ][ 1 0 1 ][ 0 0 ][ 1 0 1 ][ - - 0 1 ][ 1 - 0 0 ][ - - 1 1 ]')
>>> printf(cl)
[ _ 1 _ 1 1 ]
[ 1 _ 0 1 ]
[ 1 0 1 ]
[ 0 0 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]
[ _ _ 1 1 ]

>>> printf(cl.copy().remove_redundant())
[ _ 1 _ 1 1 ]
[ 0 0 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]
[ _ _ 1 1 ]

>>> printf(cl.minimize())
[ 0 0 ]
[ _ 0 1 ]
[ 1 _ 0 _ ]
[ _ _ _ 1 ]

>>> cl = Problem('[ 0 0 0 ][ 0 0 1 ][ 0 1 0 ][ 0 1 1 ][ 1 0 0 ][ 1 0 1 ][ 1 1 0 ][ 1 1 1 ]')
>>> printf(cl)
[ 0 0 0 ]
[ 0 0 1 ]
[ 0 1 0 ]
[ 0 1 1 ]
[ 1 0 0 ]
[ 1 0 1 ]
[ 1 1 0 ]
[ 1 1 1 ]

>>> printf(cl.copy().remove_redundant())
[ 0 0 0 ]
[ 0 0 1 ]
[ 0 1 0 ]
[ 0 1 1 ]
[ 1 0 0 ]
[ 1 0 1 ]
[ 1 1 0 ]
[ 1 1 1 ]

>>> printf(cl.minimize()) 
Traceback (most recent call last):
...
SatokuUnsatisfied: UNSAT: while minimizing 4 [ _ 0 _ ], 6 [ _ 1 _ ]
minimize_()[source]

Minimize in place.

Returns:number of minimized clauses.
negate()[source]
Returns:self for chaining
progress(message, **kwargs)[source]
Returns:self for chaining.
remove_duplicates(sort=None)[source]

Remove duplicate clauses in place.

Returns:self for chaining.
Parameters:sort – if True, also sort clause. 
>>> cl = Problem('[ 1 - 0 1 ][ 1 0 1 ][ 0 1 ][ 1 0 1 ][ - - 0 1 ][ 1 - 0 0 ]')
>>> printf(cl)
[ 1 _ 0 1 ]
[ 1 0 1 ]
[ 0 1 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]

>>> printf(cl.remove_duplicates())
[ 1 _ 0 1 ]
[ 0 1 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]
remove_redundant(sort=None)[source]

Remove redundant clauses in place.

Returns:self for chaining.
Parameters:sort – if True, also sort clause. 
>>> cl = Problem('[ 1 - 0 1 ][ 1 0 1 ][ 0 1 ][ 1 0 1 ][ - - 0 1 ][ 1 - 0 0 ]')
>>> printf(cl)
[ 1 _ 0 1 ]
[ 1 0 1 ]
[ 0 1 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]

>>> printf(cl.remove_redundant())
[ 0 1 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]
remove_redundant_min(sort=None)[source]

Remove redundant minimal clauses in place.

Returns:self for chaining.
Parameters:sort – if True, also sort clause.

Keep longest clause vectors.

>>> cl = Problem('[ 1 - 0 1 ][ 1 0 1 ][ 0 1 ][ 1 0 1 ][ - - 0 1 ][ 1 - 0 0 ]')
>>> printf(cl)
[ 1 _ 0 1 ]
[ 1 0 1 ]
[ 0 1 ]
[ 1 0 1 ]
[ _ _ 0 1 ]
[ 1 _ 0 0 ]

>>> printf(cl.remove_redundant_min())
[ 1 _ 0 1 ]
[ 1 0 1 ]
[ 0 1 ]
[ 1 _ 0 0 ]
set_width(width=-1)[source]

Set width.

Returns:self for chaining.
Parameters:width – if < 0, set width to max_width().
sort()[source]
Returns:self for chaining.
sort_by_index()[source]
Returns:self for chaining.
split()[source]
Returns:self for chaining.
xor_conflicts()[source]

XOR conflicts.

Returns:XOR clause. 
(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
class satoku.OrClause(*args, **kwargs)[source]
class satoku.AndClause(*args, **kwargs)[source]
class satoku.Problem(*args, **kwargs)[source]
>>> pr = Problem(TEST_PROBLEM)
>>> printf(pr)
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[ 1 0 1 _ _ ]
[ 0 1 0 _ _ ]
[ _ 1 0 1 ]
[ _ _ 0 1 1 ]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]

>>> printf(pr.split())
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ _ 0 _ _ _ ]
  [ _ _ 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ _ 1 _ _ _ ]
  [ _ _ 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ _ 0 _ ]
  [ _ _ _ 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ _ 1 _ ]
  [ _ _ _ _ 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]

>>> printf(pr.split())
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ _ 0 _ _ _ ]
  [ _ _ 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ _ 1 _ _ _ ]
  [ _ _ 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ _ 0 _ ]
  [ _ _ _ 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ _ 1 _ ]
  [ _ _ _ _ 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]

>>> printf(pr.max_conflicts())
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ 0 0 _ _ _ ]
  [ 0 1 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ 1 1 _ _ _ ]
  [ 1 0 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ 0 0 _ ]
  [ _ 0 1 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ 1 1 _ ]
  [ _ _ 1 0 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]

>>> printf(pr.split())
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ 0 0 _ _ _ ]
  [ 0 1 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ 1 1 _ _ _ ]
  [ 1 0 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ 0 0 _ ]
  [ _ 0 1 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ 1 1 _ ]
  [ _ _ 1 0 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]

>>> printf(pr.max_conflicts())
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ 0 0 _ _ _ ]
  [ 0 1 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ 1 1 _ _ _ ]
  [ 1 0 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ 0 0 _ ]
  [ _ 0 1 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ 1 1 _ ]
  [ _ _ 1 0 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]
flatten()[source]

Flatten problem in place.

Returns:distributive expansion of each clause. (OR(AND()) -> AND(OR())) 
>>> pr = Problem('[[1 0 - - - - ][ - - 1 0 - - ][ - - - - 1 0 ]] [[1 1 - - - - ][ - 0 1 - - - ][ - 0 - - 1 - ]]')
>>> cpr = pr.copy().flatten()
>>> printf(pr)
[
  [ 1 0 _ _ _ _ ]
  [ _ _ 1 0 _ _ ]
  [ _ _ _ _ 1 0 ]
]
[
  [ 1 1 _ _ _ _ ]
  [ _ 0 1 _ _ _ ]
  [ _ 0 _ _ 1 _ ]
]

>>> printf(cpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]

>>> pr = Problem('[ 1 _ 1 _ _ 0 ][ 1 _ _ 0 1 _ ][ 1 0 _ _ _ _ ][ 1 _ _ 0 _ 0 ]')
>>> cpr = pr.copy().flatten()
>>> printf(pr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]
[ 1 _ _ 0 _ 0 ]

>>> printf(cpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]
[ 1 _ _ 0 _ 0 ]

>>> rpr = cpr.copy().remove_redundant()
>>> printf(rpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]
[ 1 _ _ 0 _ 0 ]

>>> mpr = cpr.copy().minimize()
>>> printf(mpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]
[ 1 _ _ 0 _ 0 ]

>>> fpr = cpr.copy().flatten()
>>> printf(fpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]
[ 1 _ _ 0 _ 0 ]

>>> ccpr = cpr.copy().expand()
>>> printf(ccpr)
[ 1 _ _ _ _ _ ]
[ _ 0 1 0 _ _ ]
[ _ 0 _ 0 _ 0 ]
[ _ 0 _ _ 1 0 ]

>>> cccpr = ccpr.copy().expand()
>>> printf(cccpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 0 _ _ _ _ ]

>>> pr = Problem('[[1 0 - - - - ][ - - 1 0 - - ][ - - - - 1 0 ]] [[1 1 - - - - ][ - 0 1 - - - ][ - 0 - - 1 - ]]')
>>> printf(pr)
[
  [ 1 0 _ _ _ _ ]
  [ _ _ 1 0 _ _ ]
  [ _ _ _ _ 1 0 ]
]
[
  [ 1 1 _ _ _ _ ]
  [ _ 0 1 _ _ _ ]
  [ _ 0 _ _ 1 _ ]
]

>>> mpr = pr.max_max_conflicts(full=True)
>>> printf(mpr)
[
  [ 1 0 _ _ _ _ ]
  [ 0 0 1 0 _ _ ]
  [ 0 1 1 0 _ _ ]
  [ 1 1 1 0 _ _ ]
  [ 0 0 0 0 1 0 ]
  [ 0 0 0 1 1 0 ]
  [ 0 0 1 1 1 0 ]
  [ 0 1 0 0 1 0 ]
  [ 0 1 0 1 1 0 ]
  [ 0 1 1 1 1 0 ]
  [ 1 1 0 0 1 0 ]
  [ 1 1 0 1 1 0 ]
  [ 1 1 1 1 1 0 ]
]
[
  [ 1 1 _ _ _ _ ]
  [ 0 0 1 _ _ _ ]
  [ 1 0 1 _ _ _ ]
  [ 0 0 1 _ 1 _ ]
  [ 0 0 0 _ 1 _ ]
  [ 1 0 0 _ 1 _ ]
  [ 1 0 1 _ 1 _ ]
]

>>> min_pr = mpr.minimize().sort()
>>> printf(min_pr)
[
  [ 1 0 _ _ _ _ ]
  [ _ _ 1 0 _ _ ]
  [ _ _ _ _ 1 0 ]
]
[
  [ 1 1 _ _ _ _ ]
  [ _ 0 1 _ _ _ ]
  [ _ 0 _ _ 1 _ ]
]

>>> cpr = min_pr.copy().flatten()
>>> printf(cpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]

>>> cpr = mpr.copy().flatten()
>>> printf(cpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]

>>> max_pr = cpr.copy().max_max_conflicts(full=True)
>>> printf(max_pr)
[
  [ 1 _ _ _ _ _ ]
  [ 0 _ 1 _ _ _ ]
  [ 0 _ 0 _ _ 0 ]
]
[
  [ 1 _ _ _ _ _ ]
  [ 0 _ _ 0 _ _ ]
  [ 0 _ _ 1 1 _ ]
]
[
  [ 1 _ _ _ _ _ ]
  [ 0 _ _ 0 _ _ ]
  [ 0 _ _ 1 _ 0 ]
]
[
  [ _ 0 _ _ _ _ ]
  [ _ 1 1 _ _ _ ]
  [ _ 1 0 _ _ 0 ]
]
[
  [ _ 0 _ _ _ _ ]
  [ _ 1 _ 0 _ _ ]
  [ _ 1 _ 1 1 _ ]
]
[
  [ _ 0 _ _ _ _ ]
  [ _ 1 _ 0 _ _ ]
  [ _ 1 _ 1 _ 0 ]
]
[
  [ 1 _ _ _ _ _ ]
  [ 0 0 _ _ _ _ ]
]
[
  [ _ _ 1 _ _ _ ]
  [ _ _ 0 _ 1 _ ]
]

>>> fpr = max_pr.copy().flatten()
>>> printf(fpr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]

>>> min_pr = fpr.copy().minimize().sort()
>>> printf(min_pr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]

>>> sol_pr = min_pr.copy().expand().sort()
>>> printf(sol_pr)
[ 1 0 1 _ _ _ ]
[ 1 0 _ _ 1 _ ]
[ 1 _ 1 0 _ _ ]
[ 1 _ _ _ 1 0 ]
[ _ 0 1 0 _ _ ]
[ _ 0 _ _ 1 0 ]

>>> cmp_pr = sol_pr.copy().expand().sort()
>>> printf(cmp_pr)
[ 1 _ 1 _ _ 0 ]
[ 1 _ _ 0 1 _ ]
[ 1 _ _ 0 _ 0 ]
[ _ 0 1 _ _ 0 ]
[ _ 0 _ 0 1 _ ]
[ _ 0 _ 0 _ 0 ]
[ 1 0 _ _ _ _ ]
[ _ _ 1 _ 1 _ ]
fold()[source]
Returns:self for chaining.
max_conflicts()[source]

Maximize conflicts.

(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
Returns:self for chaining.
max_max_conflicts(full=None)[source]

Maximize conflicts in place.

(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
Returns:self for chaining.
parse_file(filename=None)[source]
Returns:self for chaining.
parse_string(string)[source]
Returns:self for chaining.
split()[source]
Returns:self for chaining.
xor_conflicts()[source]

Xorimize conflicts.

(l0 | l1 | l2 ) = ( l0 | (!l0 & l1) | (!l0 & !l1 & l2))

[ 1 1 1 ]  =  [[ 1 _ _ ]      [[ 1 _ _ ]
               [ _ 1 _ ]   =   [ 0 1 _ ]
               [ _ _ 1 ]]      [ 0 0 1 ]]
Returns:self for chaining.
class satoku.SelRow(*args, **kwargs)[source]
Parameters:size – initial size of row (keyword only).
dump(matrix, indx, regions=None)[source]
Returns:string representation.
expand(size)[source]
Returns:self for chaining.
fix_ones(matrix)[source]

Fix hard ones in row.

class satoku.SMRegion(ofs=None, size=None, **kwargs)[source]

Satoku matrix region.

Parameters:
  • ofs – is the clause number offset, where the region starts.
  • size – is the clause count inside the region.
class satoku.SMRegionIterator(*regions)[source]

Region iterator supporting dynamic changes to regions.

>>> riter = SMRegionIterator(SMRegion(2, 4), SMRegion(8, 3), SMRegion(11, 2))

>>> [indx for indx in riter]
[2, 3, 4, 5, 8, 9, 10, 11, 12]

>>> [indx for indx in riter]
[]

>>> [indx for indx in riter.at(6)]
[8, 9, 10, 11, 12]

>>> for indx in riter.at(4): break
>>> indx
4

>>> riter.offset
5

>>> riter.regions[0].size -= 2

Now, the region does no longer support offset 5:

>>> for indx in riter: break
>>> indx
8
region

Programmatic property.

class satoku.SMClause(indx=None, ofs=None, clause=None, matrix=None, size=None, **kwargs)[source]

Satoku matrix clause.

clause

Weak reference.

matrix

Weak reference.

next_ofs()[source]
Returns:self for chaining.
class satoku.SMStats(*args, **kwargs)[source]
>>> sms = SMStats()
>>> printf(sms)
{
    "satisfiable": true,
    "init_clauses": 0,
    "init_variables": 0,
    "init_synthesized": 0,
    "init_rows": 0,
    "clauses": 0,
    "variables": 0,
    "synthesized": 0,
    "rows": 0,
    "cells": 0,
    "clauses_deleted": 0,
    "rows_deleted": 0,
    "row_kills": 0,
    "duplicate_kills": 0,
    "zero_changes": 0,
    "soft_changes": 0,
    "zero_update_passes": 0,
    "row_update_passes": 0,
    "superset_update_passes": 0,
    "zero_updates": 0,
    "row_updates": 0,
    "superset_updates": 0,
    "max_zero_updates": 0,
    "max_row_updates": 0,
    "max_superset_updates": 0,
    "pending_zero_updates": 0,
    "pending_row_updates": 0,
    "pending_superset_updates": 0,
    "row_checks": 0,
    "row_merges": 0,
    "state_combines": 0,
    "cell_combines": 0,
    "message": ""
}
class satoku.SatokuMatrix(problem=None, with_variables=None, no_conflicts=None, delay_zero_updates=None, progress=None, **kwargs)[source]

Satoku Matrix.

Parameters:
  • problem – problem to be mapped. Default: self.problem.
  • with_variables – also map variables. Default: do not map variables.
  • no_conflicts – do not map conflicts. Default: map conflicts.
  • delay_zero_updates – delay mirror cell zero changes conflicts. Default: set mirrored zero changes immediately.
 
>>> pr = Problem(TEST_PROBLEM_NOCFL).split()
>>> sm = SatokuMatrix(None)

Map Problem Without Variables

>>> ign = sm.map_problem(pr, with_variables=False, no_conflicts=True)

Check Regions

>>> printf(dump_regions(sm.regions))
r0: 0, 6 / r1: 6, 0 / r2: 6, 0

>>> region = sm.regions[-3] # the one before variables
>>> region2 = sm.add_region(at=-2) # add before variables
>>> region.size -= 1
>>> region2.ofs -= 1
>>> region2.size += 1

>>> printf(dump_regions(sm.regions))
r0: 0, 5 / r1: 5, 1 / r2: 6, 0 / r3: 6, 0

Manually Set Conflicts

>>> ign = sm.zero_change(1, 1, 0, 2)
>>> ign = sm.zero_change(2, 0, 0, 1, True)
>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     0 |   0 || | || 1 * * | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || * 1 * | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || * * 1 | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     1 |   0 || | || _ _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ 0 | * 1 * | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     2 |   0 || | || _ 0 _ | _ _ _ | 1 * * | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | * 1 * | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     3 |   0 || | || _ _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     4 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     5 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 1 * * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || * 1 * |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+

Update Pending Zero Changes

>>> ign = sm.update_zeroes()
>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     0 |   0 || | || 1 * * | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || * 1 * | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || * * 1 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     1 |   0 || | || _ _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ 0 | * 1 * | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     2 |   0 || | || _ 0 _ | _ _ _ | 1 * * | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | * 1 * | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     3 |   0 || | || _ _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     4 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     5 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 1 * * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || * 1 * |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+

Slowly Kill Row s[2, 0]

>>> ign = sm.zero_change(2, 0, 0, 0)
>>> ign = sm.zero_change(2, 0, 0, 2)
>>> ign = sm.update_zeroes()
>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || * 1 * | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || * * 1 | _ 0 _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     1 |   0 || | || _ _ _ | 1 * * | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ 0 | * 1 * | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | * * 1 | 0 _ _ | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     2 |   0 || | || 0 0 0 | 0 0 0 | 1 * * | 0 0 0 | 0 0 0 || 0 0 0 |
// |       |   1 || | || _ _ _ | _ _ _ | * 1 * | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     3 |   0 || | || _ _ _ | _ _ _ | 0 _ _ | 1 * * | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | 0 _ _ | * 1 * | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | 0 _ _ | * * 1 | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     4 |   0 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | 1 * * || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | * 1 * || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | * * 1 || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     5 |   0 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || 1 * * |
// |       |   1 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || * 1 * |
// |       |   2 || | || _ _ _ | _ _ _ | 0 _ _ | _ _ _ | _ _ _ || * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+

Make Problem Unsatisfiable

>>> ign = sm.kill_row(2, 1)
>>> ign = sm.kill_row(2, 2) 
Traceback (most recent call last):
...
SatokuUnsatisfied: UNSAT s(2, 2)

>>> ign = sm.dump(immediate=True)
// |       ||  X || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || * 1 * | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || * * 1 | _ 0 _ | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     1 |   0 || | || _ _ _ | 1 * * | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ 0 | * 1 * | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | * * 1 | 0 0 0 | _ _ _ | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     2 |   0 || | || 0 0 0 | 0 0 0 | 1 * * | 0 0 0 | 0 0 0 || 0 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | * 1 * | 0 0 0 | 0 0 0 || 0 0 0 |
// |       |   2 || | || 0 0 0 | 0 0 0 | * * 1 | 0 0 0 | 0 0 0 || 0 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     3 |   0 || | || _ _ _ | _ _ _ | 0 0 0 | 1 * * | _ _ _ || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | 0 0 0 | * 1 * | _ _ _ || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | 0 0 0 | * * 1 | _ _ _ || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     4 |   0 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | 1 * * || _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | * 1 * || _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | * * 1 || _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+
// |     5 |   0 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || 1 * * |
// |       |   1 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || * 1 * |
// |       |   2 || | || _ _ _ | _ _ _ | 0 0 0 | _ _ _ | _ _ _ || * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------++-------+

Problem With Variables

Problem:

((a ∧ d) ∨ (¬a ∧ b) ∨ (¬a ∧ ¬b ∧ c)) ∧
( a ∨ ¬b ∨  c) ∧
(¬a ∨  b ∨ ¬c) ∧
( b ∨ ¬c ∨  d) ∧
(¬c ∨  d ∨  e) ∧
(¬b ∨ (b ∧ d) ∨ (b ∧ ¬d ∧ ¬e))
>>> pr = Problem(TEST_PROBLEM).split()
>>> printf(str(pr) + '\n    a b c d e')
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ _ 0 _ _ _ ]
  [ _ _ 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ _ 1 _ _ _ ]
  [ _ _ 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ _ 0 _ ]
  [ _ _ _ 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ _ 1 _ ]
  [ _ _ _ _ 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]
    a b c d e

Map Problem

>>> sm = SatokuMatrix(None)
>>> ign = sm.map_problem(pr, with_variables=True)

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || _ 0 | _ _ | _ _ | 0 _ | _ _ |
// |       |   1 || | || * 1 * | 0 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ || 0 _ | _ 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | _ 0 0 | 0 0 _ | 0 _ _ | _ 0 0 || 0 _ | 0 _ | _ 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || _ 0 0 | 1 * * | 0 _ _ | _ _ _ | _ _ _ | _ _ _ || _ 0 | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ | _ _ _ | _ 0 0 || _ _ | 0 _ | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ | 0 _ _ | _ _ _ || _ _ | _ _ | _ 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ || 0 _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ | _ _ _ | 0 _ _ || _ _ | _ 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ 0 | _ _ 0 | * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | 0 _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * | _ _ _ | 0 _ _ || _ _ | _ 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ 0 | _ _ 0 | _ _ _ | * 1 * | _ _ _ | _ _ _ || _ _ | _ _ | 0 _ | _ _ | _ _ |
// |       |   2 || | || 0 _ _ | _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || _ _ 0 | _ _ 0 | _ _ _ | _ _ _ | 1 * * | _ _ _ || _ _ | _ _ | 0 _ | _ _ | _ _ |
// |       |   1 || | || 0 _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ 0 || _ _ | _ _ | _ _ | _ 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ 0 || _ _ | _ _ | _ _ | _ _ | _ 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 * * || _ _ | 0 _ | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 _ 0 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ | * 1 * || _ _ | _ 0 | _ _ | _ 0 | _ _ |
// |       |   2 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ 0 | _ 0 0 | * * 1 || _ _ | _ 0 | _ _ | 0 _ | 0 _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || _ 0 0 | _ _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ || 1 * | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || * 1 | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | _ 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ _ || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || _ _ 0 | _ _ 0 | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | * 1 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | 1 * | _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ 0 _ | _ 0 _ || _ _ | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              5
// init synthesized            0
// init rows                  28
// clauses                     6
// variables                   5
// synthesized                 0
// rows                       28
// cells                     784
// clauses deleted             0
// rows deleted                0
// row kills                   0
// duplicate kills             0
// zero changes              106
// soft changes                0
// zero update passes          0
// row update passes           0
// superset update passes      0
// zero updates                0
// row updates                 0
// superset updates            0
// max zero updates            0
// max row updates             0
// max superset updates        0
// pending zero updates        0
// pending row updates        20
// pending superset updates    0
// row checks                  0
// row merges                  0
// state combines              0
// cell combines               0
// message
// ======================== ====

Update Rows

>>> ign = sm.update_zeroes()
>>> ign = sm.update_rows()

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 | _ 0 _ | 0 _ _ | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 | 0 0 1 | 0 _ _ | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ | _ _ _ | 1 0 0 || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || _ _ | _ _ | 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ 0 _ | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ | _ _ _ | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * | _ _ _ | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | * 1 * | _ 0 _ | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 _ _ | 0 _ _ | _ _ 0 | * * 1 | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 | 1 * * | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | * 1 * | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 | _ 0 _ | 0 _ _ | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 * | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              5
// init synthesized            0
// init rows                  28
// clauses                     6
// variables                   5
// synthesized                 0
// rows                       28
// cells                     784
// clauses deleted             0
// rows deleted                0
// row kills                   0
// duplicate kills             0
// zero changes              190
// soft changes               47
// zero update passes          0
// row update passes           4
// superset update passes      3
// zero updates                0
// row updates                53
// superset updates           19
// max zero updates            0
// max row updates            20
// max superset updates       16
// pending zero updates        0
// pending row updates         0
// pending superset updates    0
// row checks                107
// row merges                 97
// state combines              0
// cell combines               0
// message
// ======================== ====

Maximize Conflicts

>>> pr = Problem(TEST_PROBLEM).max_conflicts()
>>> printf(str(pr) + '\n    a b c d e')
[
  [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ]
]
[
  [ 1 _ _ _ _ ]
  [ 0 0 _ _ _ ]
  [ 0 1 1 _ _ ]
]
[
  [ 0 _ _ _ _ ]
  [ 1 1 _ _ _ ]
  [ 1 0 0 _ _ ]
]
[
  [ _ 1 _ _ ]
  [ _ 0 0 _ ]
  [ _ 0 1 1 ]
]
[
  [ _ _ 0 _ _ ]
  [ _ _ 1 1 _ ]
  [ _ _ 1 0 1 ]
]
[
  [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ]
]
    a b c d e

>>> sm = SatokuMatrix(None)
>>> ign = sm.map_problem(pr, with_variables=True)
>>> ign = sm.update_rows()

>>> sm.dump_bound()

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 1 0 | 1 0 0 | 0 0 1 | 0 1 0 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ | _ _ 0 | 1 0 0 | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 0 1 | * 1 * | 1 0 0 | 0 0 1 | 0 1 0 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 0 1 0 | * * 1 | 1 0 0 | 1 0 0 | 0 1 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ 0 _ | 0 1 0 | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | 1 0 0 | * 1 * | 1 0 0 | 1 0 0 | 0 0 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// |       |   2 || | || 1 0 0 | 1 0 0 | * * 1 | 0 1 0 | 1 0 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ 0 | 1 * * | _ _ 0 | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | 1 0 0 | 0 0 1 | * 1 * | 1 0 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 0 1 | 0 1 0 | 1 0 0 | * * 1 | 0 1 0 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 * * | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | 1 0 0 | _ 0 _ | * 1 * | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | * * 1 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 | 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 1 0 | 1 0 0 | 1 0 0 | * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | _ 0 _ || 1 * | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | 1 0 0 | _ 0 _ | 0 1 0 | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ 0 | 1 0 0 | _ _ 0 | 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 | 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || 0 _ _ | 0 _ _ | 1 0 0 | _ 0 _ | 0 1 0 | _ _ 0 || 0 1 | _ _ | 1 * | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | 1 0 0 | _ 0 _ | 0 1 0 | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | _ 0 _ || 1 0 | _ _ | 0 1 | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ 0 _ | _ _ _ | _ _ 0 | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              5
// init synthesized            0
// init rows                  28
// clauses                     6
// variables                   5
// synthesized                 0
// rows                       28
// cells                     784
// clauses deleted             0
// rows deleted                0
// row kills                   1
// duplicate kills             0
// zero changes              308
// soft changes               91
// zero update passes          0
// row update passes           3
// superset update passes      2
// zero updates                0
// row updates                63
// superset updates           22
// max zero updates            0
// max row updates            23
// max superset updates       18
// pending zero updates        0
// pending row updates         0
// pending superset updates    0
// row checks                127
// row merges                129
// state combines              0
// cell combines               0
// message
// ======================== ====

Delete Redundant Clauses

>>> ign = sm.delete_redundant_clauses(strictly_inside=False)
>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 0 _ _ | _ _ 0 | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 1 0 0 | 0 0 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 0 _ _ | 1 * * | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | * 1 * | 1 0 0 | 0 0 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// |       |   2 || | || 1 0 0 | * * 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || _ 0 _ | _ _ 0 | 1 * * | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | 0 0 1 | * 1 * | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 1 0 | 1 0 0 | * * 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | 0 _ _ | 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 0 1 0 | 1 0 0 | * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | 0 _ _ | _ _ 0 | _ 0 _ || 1 * | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ 0 | 1 0 0 | 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | 0 _ _ | 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 * | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | 0 _ _ | _ _ 0 | _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | 0 _ _ | _ _ 0 | _ 0 _ || 1 0 | _ _ | 0 1 | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ 0 _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              5
// init synthesized            0
// init rows                  28
// clauses                     4
// variables                   5
// synthesized                 0
// rows                       22
// cells                     484
// clauses deleted             2
// rows deleted                0
// row kills                   1
// duplicate kills             0
// zero changes              308
// soft changes               91
// zero update passes          0
// row update passes           3
// superset update passes      2
// zero updates                0
// row updates                63
// superset updates           22
// max zero updates            0
// max row updates            23
// max superset updates       18
// pending zero updates        0
// pending row updates         0
// pending superset updates    0
// row checks                127
// row merges                129
// state combines              0
// cell combines               0
// message
// ======================== ====

Extract solutions

Get row with longest variable binding s[1,1]:

// |       |   1 || | || 1 0 0 | * 1 * | 1 0 0 | 0 0 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |

Disable row:

// |       ||  P || | || _ _ _ | _ 0 _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 0 0 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 1 0 0 | 0 0 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 0 _ _ | 1 * * | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | * 1 * | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 1 0 0 | * * 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 0 1 | 1 0 0 | 1 * * | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | 0 0 1 | * 1 * | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 1 0 | 1 0 0 | * * 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | 0 _ _ | 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 0 0 0 | 0 0 0 | 0 0 0 | * * 1 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | 0 0 1 | 0 1 0 | 1 0 0 || 1 * | 0 1 | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 * | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | 0 _ _ | 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 * | 1 0 | _ _ |
// |       |   1 || | || 1 0 0 | 0 0 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | 0 0 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ 0 _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ 0 _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+

Get row with longest variable binding s[0,0]:

// |     0 |   0 || | || 1 * * | 0 0 1 | 0 1 0 | 1 0 0 || 1 0 | 0 1 | 0 1 | 0 1 | _ _ |

Disable row:

// |       ||  P || | || 0 _ _ | _ 0 0 | _ 0 _ | _ _ 0 || 0 _ | _ _ | _ 0 | _ 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || * 1 * | 1 0 0 | 0 0 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 0 _ _ | 1 * * | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | * 1 * | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | * * 1 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 0 1 | 1 0 0 | 1 * * | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | * 1 * | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 1 0 | 1 0 0 | * * 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || 0 1 0 | 1 0 0 | 0 0 1 | 1 * * || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 0 0 0 | 0 0 0 | 0 0 0 | * * 1 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 1 * | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 * | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 1 0 | 1 0 0 | 0 0 1 | 1 0 0 || 0 1 | * 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 * | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | * 1 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * 1 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | 1 * |
// |       |   1 || | || 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+

Get row with longest variable binding s[0,1]:

// |       |   1 || | || * 1 * | 1 0 0 | 0 0 1 | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |

Disable row:

// |       ||  P || | || 0 0 _ | _ 0 0 | _ 0 0 | 0 _ 0 || 0 _ | _ 0 | _ 0 | _ 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || * 1 * | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || * * 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 0 0 1 | 1 * * | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | * 1 * | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | * * 1 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 0 1 | 1 0 0 | 1 * * | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | * 1 * | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | 0 0 0 | * * 1 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 1 * * || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 0 0 0 | 0 0 0 | 0 0 0 | * * 1 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 1 * | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || * 1 | 1 0 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 * | 1 0 | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | * 1 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 * | 1 0 | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | * 1 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 * | _ _ |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * 1 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | 1 * |
// |       |   1 || | || 0 0 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+

Get row with longest variable binding s[0,2]:

// |       |   2 || | || * * 1 | 1 0 0 | 1 0 0 | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |

Disable row:

// |       ||  P || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || * 1 * | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || * * 1 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 0 0 0 | 1 * * | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | * 1 * | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | * * 1 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 0 0 | 0 0 0 | 1 * * | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | * 1 * | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | 0 0 0 | * * 1 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 1 * * || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | * 1 * || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   2 || | || 0 0 0 | 0 0 0 | 0 0 0 | * * 1 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 1 * | 0 0 | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || * 1 | 0 0 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 1 * | 0 0 | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | * 1 | 0 0 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 1 * | 0 0 | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | * 1 | 0 0 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 1 * | 0 0 |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * 1 | 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 1 * |
// |       |   1 || | || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-----+-----+-----+-----+-----+

Solutions (DNF clause vectors):

[ 1 1 0 0 0 ]
[ 1 0 0 0 _ ]
[ 0 0 1 1 _ ]
[ 0 1 1 1 _ ]
  a b c d e

Original Problem:

[ [ 1 _ _ 0 _ ]
  [ 0 1 _ _ _ ]
  [ 0 0 1 _ _ ] ]
[ [ 1 _ _ _ _ ]
  [ _ 0 _ _ _ ]
  [ _ _ 1 _ _ ] ]
[ [ 0 _ _ _ _ ]
  [ _ 1 _ _ _ ]
  [ _ _ 0 _ _ ] ]
[ [ _ 1 _ _ ]
  [ _ _ 0 _ ]
  [ _ _ _ 1 ] ]
[ [ _ _ 0 _ _ ]
  [ _ _ _ 1 _ ]
  [ _ _ _ _ 1 ] ]
[ [ _ 0 _ _ _ ]
  [ _ 1 _ 1 _ ]
  [ _ 1 _ 0 0 ] ]
    a b c d e
add_clause(clause)[source]
Returns:self for chaining.
add_region(ofs=None, size=None, at=None)[source]
Returns:new region.
add_variables(problem=None)[source]
Returns:self for chaining.
cell_rows(si, sg, normalized=None)[source]
Returns:
cell_rows_(this, that, normalized=None)[source]
Returns:
check_minor_ccrs(vert_regions=None, horz_regions=None, min_height=None)[source]
Returns:number of rows killed
clear_superset_updates()[source]

Clear superset updates.

Returns:self for chaining.
combine_bin_conflicts(vert_regions=None, horz_regions=None, full=None, keep_uncombined=None)[source]
Returns:number of cells combined
combine_cells(si, sg, keep_uncombined=None, template_only=None, relaxed=None)[source]
Returns:combined cell
combine_cells_(this, that, keep_uncombined=None, template_only=None, relaxed=None)[source]
Returns:

combined cell
Parameters:
  • this – SMClause instance.
  • that – SMClause instance or None. If None, a single clause is copied or moved.
combine_reducable_cells(vert_regions=None, horz_regions=None, allow_equal=None, full=None, keep_uncombined=None)[source]
Returns:number of cells combined
combine_states(si, sj, sg, sh)[source]
Returns:combined cell
combine_states_(this, sj, that, sh)[source]
Returns:combined cell
delete_2_state_cell_rows()[source]
Returns:self for chaining.
delete_clause(si)[source]
Returns:self for chaining.
delete_clauses(start, end)[source]

Delete a region of clauses.

Returns:

self for chaining.
Parameters:
  • start – start clause index.
  • end – end clause index.
 
>>> pr = Problem()
>>> cv = ClauseVector('1 1')
>>> pr.extend([cv.copy() for i in xrange( 5 + 3 + 2 + 5 + 0)])
>>> sm = SatokuMatrix(pr)
>>> ign = sm.set_region(0, 5)
>>> ign = sm.set_region(5, 3)
>>> ign = sm.set_region(8, 2)
>>> ign = sm.set_region(10, 5)
>>> ign = sm.add_region(at=-2)

>>> printf(dump_regions(sm.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 2 / r3: 10, 5 / r4: 15, 0 / r5: 15, 0 / r6: 15, 0

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || * 1 | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     1 |   0 || | || _ _ | 1 * | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | * 1 | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     2 |   0 || | || _ _ | _ _ | 1 * | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | * 1 | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ | _ _ | _ _ | 1 * | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | * 1 | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     4 |   0 || | || _ _ | _ _ | _ _ | _ _ | 1 * || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | * 1 || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || 1 * | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || * 1 | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     6 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | 1 * | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | * 1 | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | 1 * || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | * 1 || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || 1 * | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || * 1 | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |     9 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | 1 * || _ _ | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | * 1 || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || 1 * | _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || * 1 | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |    11 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |    12 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | * 1 | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |    13 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | 1 * | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+
// |    14 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ || _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----+-----+-----++-----+-----++-----+-----+-----+-----+-----+

Verify Matrix Copy

>>> smt = sm.copy()
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 2 / r3: 10, 5 / r4: 15, 0 / r5: 15, 0 / r6: 15, 0

Case 1: start < 0, end < 0

>>> smt = sm.copy().delete_clauses(-1, -5)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 2 / r3: 10, 5 / r4: 15, 0 / r5: 15, 0 / r6: 15, 0

Case 2: start > len(clauses), end > len(clauses)

>>> smt = sm.copy().delete_clauses(18, 20)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 2 / r3: 10, 5 / r4: 15, 0 / r5: 15, 0 / r6: 15, 0

Case 3: begin inside clause, end inside different clause, intermediate clauses covered

>>> smt = sm.copy().delete_clauses(6, 11)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 1 / r2: 6, 4 / r3: 10, 0 / r4: 10, 0 / r5: 10, 0

>>> ign = smt.dump(immediate=True)
// |       ||  P || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     0 |   0 || | || 1 * | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || * 1 | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     1 |   0 || | || _ _ | 1 * | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | * 1 | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     2 |   0 || | || _ _ | _ _ | 1 * | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | * 1 | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     3 |   0 || | || _ _ | _ _ | _ _ | 1 * | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | * 1 | _ _ || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     4 |   0 || | || _ _ | _ _ | _ _ | _ _ | 1 * || _ _ || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | * 1 || _ _ || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     5 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || 1 * || _ _ | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || * 1 || _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     6 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     7 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | * 1 | _ _ | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     8 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | 1 * | _ _ |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+
// |     9 |   0 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ | _ _ | _ _ | _ _ | _ _ || _ _ || _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-----+-----+-----+-----+-----++-----++-----+-----+-----+-----+

Case 4: begin inside clause, end inside different clause, no intermediate clauses

>>> smt = sm.copy().delete_clauses(7, 9)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 2 / r2: 7, 1 / r3: 8, 5 / r4: 13, 0 / r5: 13, 0 / r6: 13, 0

Case 5: begin inside clause, end at end of same clause

>>> smt = sm.copy().delete_clauses(7, 8)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 2 / r2: 7, 2 / r3: 9, 5 / r4: 14, 0 / r5: 14, 0 / r6: 14, 0

Case 6: begin at start of clause, end inside same clause

>>> smt = sm.copy().delete_clauses(8, 9)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 1 / r3: 9, 5 / r4: 14, 0 / r5: 14, 0 / r6: 14, 0

Case 7: begin at start of clause, end at end of same clause

>>> smt = sm.copy().delete_clauses(5, 8)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 2 / r2: 7, 5 / r3: 12, 0 / r4: 12, 0 / r5: 12, 0

| 0 <- 5 -> | 5 <- 3 -> | 8 <- 2 -> | 10 <- 5 -> | 15 <- 0 -> | 15

                6                        11
                      7           9
                      7   8
                          8       9
              5           8
>>> smt = sm.copy().delete_clauses(8, 10)
>>> printf(dump_regions(smt.regions))
r0: 0, 5 / r1: 5, 3 / r2: 8, 5 / r3: 13, 0 / r4: 13, 0 / r5: 13, 0
delete_killed_rows()[source]
Returns:self for chaining.
delete_redundant_clauses(vert_regions=None, horz_regions=None, strictly_inside=None)[source]
Returns:self for chaining.
delete_rows(si, sj, sx)[source]

Delete rows from a clause.

Returns:

self for chaining.
Parameters:
  • si – cell index
  • sj – start row offset.
  • sx – end row offset.
 
>>> pr = Problem()
>>> cv = ClauseVector('1 1 1')
>>> pr.extend([cv.copy() for i in xrange(2 + 3)])
>>> cv = ClauseVector('1 1 1 1')
>>> pr.extend([cv.copy() for i in xrange(5)])
>>> cv = ClauseVector('1 1 1 1 1 1')
>>> pr.extend([cv.copy() for i in xrange(2)])

>>> sm = SatokuMatrix(pr)
>>> ign = sm.set_region(0, 2)
>>> ign = sm.set_region(2, 3)
>>> ign = sm.set_region(5, 5)
>>> ign = sm.set_region(10, 2)

>>> printf(dump_regions(sm.regions))
r0: 0, 2 / r1: 2, 3 / r2: 5, 5 / r3: 10, 2 / r4: 12, 0 / r5: 12, 0

>>> ign = sm.zero_change(0, 0, 1, 0, immediate=None)
>>> ign = sm.zero_change(0, 1, 2, 1, immediate=None)
>>> ign = sm.zero_change(0, 2, 3, 2, immediate=None)

>>> ign = sm.zero_change(1, 0, 2, 0, immediate=None)
>>> ign = sm.zero_change(1, 1, 3, 1, immediate=None)
>>> ign = sm.zero_change(1, 2, 4, 2, immediate=None)

>>> ign = sm.delete_rows( 0, 0, 1)
>>> ign = sm.delete_rows( 1, 0, 1)
>>> ign = sm.delete_rows(10, 0, 1)

>>> smt = sm.copy()
>>> ign = smt.dump(immediate=True)
// |       ||  P || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     0 |   0 || | || 1 * | _ _ || _ 0 _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || * 1 | _ _ || _ _ _ | _ _ 0 | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     1 |   0 || | || _ _ | 1 * || _ _ _ | _ 0 _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | * 1 || _ _ _ | _ _ _ | _ _ 0 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     2 |   0 || | || _ _ | _ _ || 1 * * | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || * 1 * | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || * * 1 | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     3 |   0 || | || _ _ | _ _ || _ _ _ | 1 * * | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | * 1 * | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | * * 1 | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     4 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | 1 * * || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | * 1 * || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | * * 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     5 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || 1 * * * | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || * 1 * * | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || * * 1 * | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || * * * 1 | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     6 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | 1 * * * | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | * 1 * * | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | * * 1 * | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | * * * 1 | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     7 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | 1 * * * | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | * 1 * * | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | * * 1 * | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | * * * 1 | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     8 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | 1 * * * | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * 1 * * | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * 1 * | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * * 1 | _ _ _ _ || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     9 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | 1 * * * || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | * 1 * * || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | * * 1 * || _ _ _ _ _ | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | * * * 1 || _ _ _ _ _ | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |    10 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || 1 * * * * | _ _ _ _ _ _ |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || * 1 * * * | _ _ _ _ _ _ |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || * * 1 * * | _ _ _ _ _ _ |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || * * * 1 * | _ _ _ _ _ _ |
// |       |   4 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || * * * * 1 | _ _ _ _ _ _ |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |    11 |   0 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | 1 * * * * * |
// |       |   1 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | * 1 * * * * |
// |       |   2 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | * * 1 * * * |
// |       |   3 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | * * * 1 * * |
// |       |   4 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | * * * * 1 * |
// |       |   5 || | || _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ || _ _ _ _ _ | * * * * * 1 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+

  • case 1: zero line at beginning of 2-state

    >>> ign = smt.kill_row(0, 0)

  • case 2: zero line at end of 2-state

    >>> ign = smt.kill_row(1, 1)

  • case 3: 2 zero lines at beginning of 3-state

    >>> ign = smt.kill_row(2, 0)
>>> ign = smt.kill_row(2, 1)

  • case 4: 2 zero lines at end of 3-state

    >>> ign = smt.kill_row(3, 1)
>>> ign = smt.kill_row(3, 2)

  • case 5: 1 zero lines at beg. of 3-state, 1 zero lines at end of 3-state

    >>> ign = smt.kill_row(4, 0)
>>> ign = smt.kill_row(4, 2)

  • case 6: 2 zero lines at beginning of 4-state

    >>> ign = smt.kill_row(5, 0)
>>> ign = smt.kill_row(5, 1)

  • case 7: 2 zero lines at end of 4-state

    >>> ign = smt.kill_row(6, 2)
>>> ign = smt.kill_row(6, 3)

  • case 8: 2 zero lines in the middle of 4-state

    >>> ign = smt.kill_row(7, 1)
>>> ign = smt.kill_row(7, 2)

  • case 9: 2 zero lines at beginning of 4-state, 1 at end

    >>> ign = smt.kill_row(8, 0)
>>> ign = smt.kill_row(8, 1)
>>> ign = smt.kill_row(8, 3)

  • case 10: 2 zero lines at end of 4-state, 1 at beg.

    >>> ign = smt.kill_row(9, 0)
>>> ign = smt.kill_row(9, 2)
>>> ign = smt.kill_row(9, 3)

  • case 11: 2 zero lines at beginning of 5-state + 2 at end

    >>> ign = smt.kill_row(10, 0)
>>> ign = smt.kill_row(10, 1)
>>> ign = smt.kill_row(10, 3)
>>> ign = smt.kill_row(10, 4)

  • case 12: 2 zero lines at beginning of 6-state + 2 at end

    >>> ign = smt.kill_row(11, 0)
>>> ign = smt.kill_row(11, 1)
>>> ign = smt.kill_row(11, 4)
>>> ign = smt.kill_row(11, 5)

>>> ign = smt.dump(immediate=True)
// |       ||  P || | || 0 1 | 1 0 || 0 0 1 | 1 0 0 | 0 1 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 1 0 | 0 1 0 0 || 0 0 1 0 0 | 0 0 _ _ 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     0 |   0 || | || 1 * | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || * 1 | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     1 |   0 || | || 0 _ | 1 * || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   1 || | || 0 0 | * 1 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     2 |   0 || | || 0 0 | 0 0 || 1 * * | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || 0 0 | 0 0 || * 1 * | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   2 || | || 0 _ | _ 0 || * * 1 | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     3 |   0 || | || 0 _ | _ 0 || 0 0 _ | 1 * * | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | * 1 * | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   2 || | || 0 0 | 0 0 || 0 0 0 | * * 1 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     4 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 1 * * || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | * 1 * || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   2 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | * * 1 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     5 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 1 * * * | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || * 1 * * | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   2 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || * * 1 * | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   3 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || * * * 1 | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     6 |   0 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | 1 * * * | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | * 1 * * | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   2 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | * * 1 * | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   3 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | * * * 1 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     7 |   0 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | 1 * * * | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | * 1 * * | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   2 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | * * 1 * | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   3 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | * * * 1 | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     8 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 1 * * * | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | * 1 * * | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   2 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | * * 1 * | 0 _ 0 0 || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   3 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | * * * 1 | 0 0 0 0 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |     9 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 1 * * * || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | * 1 * * || 0 0 _ 0 0 | 0 0 _ _ 0 0 |
// |       |   2 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | * * 1 * || 0 0 0 0 0 | 0 0 0 0 0 0 |
// |       |   3 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | * * * 1 || 0 0 0 0 0 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |    10 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 1 * * * * | 0 0 0 0 0 0 |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || * 1 * * * | 0 0 0 0 0 0 |
// |       |   2 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || * * 1 * * | 0 0 _ _ 0 0 |
// |       |   3 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || * * * 1 * | 0 0 0 0 0 0 |
// |       |   4 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || * * * * 1 | 0 0 0 0 0 0 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+
// |    11 |   0 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | 1 * * * * * |
// |       |   1 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | * 1 * * * * |
// |       |   2 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | * * 1 * * * |
// |       |   3 || | || 0 _ | _ 0 || 0 0 _ | _ 0 0 | 0 _ 0 || 0 0 _ _ | _ _ 0 0 | _ 0 0 _ | 0 0 _ 0 | 0 _ 0 0 || 0 0 _ 0 0 | * * * 1 * * |
// |       |   4 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | * * * * 1 * |
// |       |   5 || | || 0 0 | 0 0 || 0 0 0 | 0 0 0 | 0 0 0 || 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 || 0 0 0 0 0 | * * * * * 1 |
// +-------+-----++-+-++-----+-----++-------+-------+-------++---------+---------+---------+---------+---------++-----------+-------------+

>>> ign = smt.delete_killed_rows()

>>> ign = smt.dump(immediate=True)
// |       ||  P || | || 0 1 | 1 0 || 0 1 | 1 0 | 0 1 || _ _ | _ _ | _ _ | 0 1 | 0 1 || 0 1 | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     0 |   0 || | || 1 * | 0 0 || 0 0 | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 0 0 | 0 0 |
// |       |   1 || | || * 1 | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     1 |   0 || | || 0 _ | 1 * || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// |       |   1 || | || 0 0 | * 1 || 0 0 | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 0 0 | 0 0 |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     2 |   0 || | || 0 0 | 0 0 || 1 * | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 0 0 | 0 0 |
// |       |   1 || | || 0 _ | _ 0 || * 1 | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     3 |   0 || | || 0 _ | _ 0 || 0 _ | 1 * | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// |       |   1 || | || 0 0 | 0 0 || 0 0 | * 1 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 0 0 | 0 0 |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     4 |   0 || | || 0 0 | 0 0 || 0 0 | 0 0 | 1 * || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 0 0 | 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | * 1 || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     5 |   0 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || 1 * | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || * 1 | _ _ | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     6 |   0 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | 1 * | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | * 1 | _ _ | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     7 |   0 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | 1 * | 0 _ | 0 _ || 0 _ | _ _ |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | * 1 | 0 _ | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     8 |   0 || | || 0 0 | 0 0 || 0 0 | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 1 * | 0 0 || 0 0 | 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | * 1 | 0 _ || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |     9 |   0 || | || 0 0 | 0 0 || 0 0 | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 1 * || 0 0 | 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | * 1 || 0 _ | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |    10 |   0 || | || 0 0 | 0 0 || 0 0 | 0 0 | 0 0 || 0 0 | 0 0 | 0 0 | 0 0 | 0 0 || 1 * | 0 0 |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || * 1 | _ _ |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+
// |    11 |   0 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | 1 * |
// |       |   1 || | || 0 _ | _ 0 || 0 _ | _ 0 | 0 _ || _ _ | _ _ | _ _ | 0 _ | 0 _ || 0 _ | * 1 |
// +-------+-----++-+-++-----+-----++-----+-----+-----++-----+-----+-----+-----+-----++-----+-----+

>>> printf(dump_regions(sm.regions))
r0: 0, 2 / r1: 2, 3 / r2: 5, 5 / r3: 10, 2 / r4: 12, 0 / r5: 12, 0
delete_single_clues()[source]
Returns:self for chaining.
dump(immediate=False, regions=None, **kwargs)[source]
Returns:string representation, if immediate is False, self otherwise.
dump_bound(regions=None)[source]
Returns:dump all bound clause conflict sub-matrixes.
dump_minor_ccrs(vert_regions=None, horz_regions=None, min_height=None)[source]
Returns:dump all minor_ccr clause conflict sub-matrixes.
dump_stats()[source]
Returns:string representation.
eval_problem_commands(commands)[source]
find_bin_conflicts(vert_regions=None, horz_regions=None, full=None)[source]
Returns:list of cell index tuples (this, that)
find_reducable_cells(vert_regions=None, horz_regions=None, allow_equal=None, full=None)[source]
Returns:list of cell index tuples (this, that)
fmt_cell_row(si, sj, sg, dump=None)[source]

Format cell row reference.

Returns:formatted cell row reference
fmt_cell_row_abs(si, sj, sg, dump=None, ri=None, ci=None)[source]

Format cell row reference.

Returns:

formatted cell row reference
Parameters:
  • dump – if True, dump the cell row contents.
  • ri – if negative, do not add absolute reference. if None, calculate absolute row index.
  • ci – if None or negative, calculate absolute column index.
fmt_state_row(si, sj)[source]

Format state row reference.

Returns:formatted state row reference
fmt_state_row_abs(si, sj, ri=None)[source]

Format state row reference.

Returns:formatted state row reference
Parameters:ri – if negative, do not add absolute reference. if None, calculate absolute row index.
image(output=None, format_=None, no_save=None, width=None, height=None)[source]
Returns:PIL image. 
>>> pr = Problem(TEST_PROBLEM)
>>> sm = SatokuMatrix(pr)
>>> ign = sm.update_rows()

>>> sm.image(None, 'PPM') 
P6
199 199
255
...
is_bound(row, sg)[source]
Returns:(True, ofs), if there is at most a single one (hard or soft) in the segment.
is_bound_(row, astate_ofs, size)[source]
Returns:(True, ofs), if there is at most a single one (hard or soft) in the segment.
is_minor_ccr(row, sg)[source]

Is this a minor conflict cell row.

Returns:(True, ofs, ofs), if there is at least one impossible state and at most two possible states in the segment.
is_minor_ccr_(row, astate_ofs, size)[source]

Is this row section a minor conflict cell row.

Returns:(True, ofs, ofs), if there is at least one impossible state and at most two possible states in the segment.
kill_row(si, sj)[source]
Returns:self for chaining.
map_conflicts(delay_zero_updates=None)[source]

Map clause conflicts.

Returns:self for chaining.
Parameters:delay_zero_updates – delay mirror cell zero changes conflicts. Default: set mirrored zero changes immediately.
map_problem(problem=None, with_variables=None, no_conflicts=None, delay_zero_updates=None)[source]

Map a problem into satoku matrix.

Returns:

self for chaining.
Parameters:
  • problem – problem to be mapped. Default: self.problem.
  • with_variables – also map variables. Default: do not map variables.
  • no_conflicts – do not map conflicts. Default: map conflicts.
  • delay_zero_updates – delay mirror cell zero changes conflicts. Default: set mirrored zero changes immediately.
 
>>> pr = Problem(TEST_PROBLEM)
>>> sm = SatokuMatrix(pr, delay_zero_updates=True)

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ |
// |       |   1 || | || * 1 * | 0 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | _ 0 0 | 0 0 _ | 0 _ _ | _ 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     1 |   0 || | || _ _ _ | 1 * * | 0 _ _ | _ _ _ | _ _ _ | _ _ _ |
// |       |   1 || | || _ _ _ | * 1 * | _ 0 _ | 0 _ _ | _ _ _ | _ 0 0 |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ | 0 _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     2 |   0 || | || _ _ _ | _ _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | * 1 * | _ _ _ | _ _ _ | 0 _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     3 |   0 || | || _ _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ | 0 _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ _ | _ _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     4 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ 0 |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     5 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              0
// init synthesized            0
// init rows                  18
// clauses                     6
// variables                   0
// synthesized                 0
// rows                       18
// cells                     324
// clauses deleted             0
// rows deleted                0
// row kills                   0
// duplicate kills             0
// zero changes               28
// soft changes                0
// zero update passes          0
// row update passes           0
// superset update passes      0
// zero updates                0
// row updates                 0
// superset updates            0
// max zero updates            0
// max row updates             0
// max superset updates        0
// pending zero updates       28
// pending row updates         3
// pending superset updates    0
// row checks                  0
// row merges                  0
// state combines              0
// cell combines               0
// message
// ======================== ====

>>> ign = sm.update_zeroes()
>>> ign = sm.clear_superset_updates()
>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ |
// |       |   1 || | || * 1 * | 0 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | _ 0 0 | 0 0 _ | 0 _ _ | _ 0 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     1 |   0 || | || _ 0 0 | 1 * * | 0 _ _ | _ _ _ | _ _ _ | _ _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ | _ _ _ | _ 0 0 |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ | 0 _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ | _ _ _ | 0 _ _ |
// |       |   2 || | || _ _ 0 | _ _ 0 | * * 1 | _ _ _ | _ _ _ | _ _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * | _ _ _ | 0 _ _ |
// |       |   1 || | || _ _ 0 | _ _ 0 | _ _ _ | * 1 * | _ _ _ | _ _ _ |
// |       |   2 || | || 0 _ _ | _ _ _ | _ _ _ | * * 1 | _ _ _ | _ _ 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     4 |   0 || | || _ _ 0 | _ _ 0 | _ _ _ | _ _ _ | 1 * * | _ _ _ |
// |       |   1 || | || 0 _ _ | _ _ _ | _ _ _ | _ _ _ | * 1 * | _ _ 0 |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 * * |
// |       |   1 || | || 0 _ 0 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ | * 1 * |
// |       |   2 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ 0 | _ 0 0 | * * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------+

>>> printf(sm.dump_stats())
// ======================== ====
//       Satoku Statistics
// ======================== ====
// satisfiable              True
// init clauses                6
// init variables              0
// init synthesized            0
// init rows                  18
// clauses                     6
// variables                   0
// synthesized                 0
// rows                       18
// cells                     324
// clauses deleted             0
// rows deleted                0
// row kills                   0
// duplicate kills             0
// zero changes               56
// soft changes                0
// zero update passes          1
// row update passes           0
// superset update passes      0
// zero updates               28
// row updates                 0
// superset updates            0
// max zero updates           28
// max row updates             0
// max superset updates        0
// pending zero updates        0
// pending row updates         6
// pending superset updates    0
// row checks                  0
// row merges                  0
// state combines              0
// cell combines               0
// message
// ======================== ====

>>> pr = Problem(TEST_PROBLEM_REGIONS)
>>> sm = SatokuMatrix(pr, with_variables=True)
>>> ign = sm.update_rows()
>>> pr.commands
[('r', '3 2 1 5 9 10')]

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ || _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ || _ _ 0 | _ 0 _ || _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 || _ 0 _ | 0 _ _ || 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 || 0 0 1 | 0 _ _ || 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ || _ _ 0 | _ 0 _ || _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ || 0 _ _ | _ _ _ || 1 0 0 || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 || _ 0 _ | 0 _ _ || _ _ 0 || _ _ | _ _ | 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * || _ 0 _ | 0 _ _ || _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * || _ _ _ | _ _ _ || 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 || _ _ 0 | _ 0 _ || _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ || 1 * * | _ _ _ || 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ || * 1 * | _ 0 _ || _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 _ _ | 0 _ _ | _ _ 0 || * * 1 | 0 _ _ || _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ 0 | 0 _ _ || _ _ 0 | 1 * * || _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 || _ 0 _ | * 1 * || _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ | * * 1 || _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 0 |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ || 0 _ _ | _ _ _ || 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 || _ 0 _ | 0 _ _ || * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ || _ _ 0 | 1 0 0 || * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ || _ _ 0 | _ 0 _ || _ 0 _ || 1 * | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 || _ 0 _ | 0 _ _ || _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ || _ _ _ | _ _ _ || 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ || 0 _ _ | _ _ _ || 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 || _ 0 _ | 0 _ _ || _ _ 0 || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ || _ _ 0 | _ 0 _ || _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 || _ 0 _ | 0 _ _ || _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ || _ _ 0 | _ 0 _ || _ 0 _ || 1 0 | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ || _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ 0 || _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------++-------+-------++-------++-----+-----+-----+-----+-----+

>>> ign = sm.dump(immediate=True, regions=[_r for _i, _r in enumerate(sm.regions) if _i not in (1,)])
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ || _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 || 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 || 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ || _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ || 1 0 0 || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 || _ _ 0 || _ _ | _ _ | 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * || _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * || 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 || _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ || 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 || * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ || * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ || _ 0 _ || 1 * | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 || _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ || 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ || 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || _ _ _ | _ _ _ | _ _ 0 || _ _ 0 || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ || _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 || _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ || _ 0 _ || 1 0 | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ _ || _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ || _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------++-------++-----+-----+-----+-----+-----+
minor_ccr_default_param(vert_regions=None, horz_regions=None, min_height=None)[source]
Returns:(vert_regions, horz_regions, min_height)
next_bound(si=None, sg=None, vert_regions=None, horz_regions=None, strictly_inside=None)[source]
Returns:[si, sg] for next fully bound CCSM.
next_minor_ccr(si=None, sj=None, sg=None, vert_regions=None, horz_regions=None, min_height=None)[source]
Returns:[si, sj, sg, one_sh_0, one_sh_1] for next fully minor_ccr CCSM.
one_count(row, sf)[source]
Returns:soft_count, hard_count, soft_ones, hard_ones
one_count_quick(row, sf)[source]
Returns:one counts (soft, hard)
parse_file(filename=None, has_variables=None, delay_zero_updates=None)[source]
Returns:self for chaining.
problem

Weak reference.

progress(message, **kwargs)[source]
Returns:self for chaining.
rebuild_clauses_and_maps(reason=None)[source]

Rebuild clauses and clause maps.

required_selection(row, sf)[source]
Returns:offset for required selection (hard one) or -1
required_selection_(row, ci, size)[source]
Returns:offset for required selection (hard one) or -1
row_update_request(si, sj)[source]
Returns:self for chaining.
selection_request(row, sf)[source]
Returns:offset for selection request (soft one) or -1
selection_request_(row, ci, size)[source]
Returns:offset for selection request (soft one) or -1
set_region(ofs, size=None, keep_empty=None)[source]

Set a region.

Returns:self for chaining. 
>>> pr = Problem(TEST_PROBLEM)
>>> sm = SatokuMatrix(None)
>>> ign = sm.map_problem(pr, with_variables=True)
>>> ign = sm.update_rows()

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 | _ 0 _ | 0 _ _ | 0 1 0 || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 | 0 0 1 | 0 _ _ | 1 0 0 || 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ | _ _ _ | 1 0 0 || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || _ _ | _ _ | 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ 0 _ | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ | _ _ _ | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * | _ _ _ | 0 _ _ || _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | * 1 * | _ 0 _ | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 _ _ | 0 _ _ | _ _ 0 | * * 1 | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 | 1 * * | _ 0 _ || 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | * 1 * | _ _ 0 || 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | * * 1 | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 0 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 * * || _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 | _ 0 _ | 0 _ _ | * 1 * || 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 | 1 0 0 | * * 1 || 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 * | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ _ | _ _ _ | 0 _ _ || _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ | _ _ _ | 1 0 0 || _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ | 0 _ _ | _ _ 0 || 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 | _ 0 _ | _ 0 _ || 1 0 | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 || _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------+-------+-------++-----+-----+-----+-----+-----+

>>> ign = sm.set_region(4, 4)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 4 / r2: 8, 3 / r3: 11, 0

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ | _ _ || _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ || _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 | _ 0 _ || 0 _ _ | 0 1 0 | 0 1 | 1 0 || 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 | 0 0 1 || 0 _ _ | 1 0 0 | 0 1 | 0 1 || 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ || _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ || _ _ _ | 1 0 0 | _ _ | 0 1 || _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | _ _ | _ _ || 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ 0 _ || 0 _ _ | _ _ 0 | 0 1 | _ _ || 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ || _ _ _ | 0 _ _ | _ _ | 1 0 || _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ || 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * || _ _ _ | 0 _ _ | _ _ | 1 0 || _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | * 1 * || _ 0 _ | _ 0 _ | 1 0 | _ _ || 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 _ _ | 0 _ _ | _ _ 0 | * * 1 || 0 _ _ | _ _ 0 | 0 1 | _ _ || 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 || 1 * * | _ 0 _ | 1 0 | _ _ || 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || * 1 * | _ _ 0 | 0 1 | _ _ || 1 0 | 1 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 | _ _ 0 | _ _ | _ _ || _ _ | _ _ | 1 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ | 1 * * | _ _ | 0 1 || _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 | _ 0 _ || 0 _ _ | * 1 * | 0 1 | 1 0 || 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 || 1 0 0 | * * 1 | 1 0 | 1 0 || 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 * | _ _ || _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | * 1 | _ _ || 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ _ || _ _ _ | 0 _ _ | _ _ | 1 * || _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ | 1 0 0 | _ _ | * 1 || _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | _ _ | _ _ || 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ || * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | 0 1 | _ _ || 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ || _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ 0 | _ _ | _ _ || _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ 0 | _ _ _ | _ _ | _ _ || _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----++-----+-----+-----+

>>> ign = sm.set_region(4, 4)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 4 / r2: 8, 3 / r3: 11, 0

>>> ign = sm.set_region(4, 7)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 7 / r2: 11, 0 / r3: 11, 0

>>> ign = sm.set_region(4, 4)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 4 / r2: 8, 3 / r3: 11, 0 / r4: 11, 0

>>> ign = sm.set_region(0, 10)
>>> printf(dump_regions(sm.regions))
r0: 0, 10 / r1: 10, 1 / r2: 11, 0 / r3: 11, 0

>>> ign = sm.set_region(0, 11)
>>> printf(dump_regions(sm.regions))
r0: 0, 11 / r1: 11, 0 / r2: 11, 0

>>> ign = sm.set_region(0, 9)
>>> printf(dump_regions(sm.regions))
r0: 0, 9 / r1: 9, 2 / r2: 11, 0 / r3: 11, 0

>>> ign = sm.set_region(4, 4)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 4 / r2: 8, 1 / r3: 9, 2 / r4: 11, 0 / r5: 11, 0

>>> ign = sm.set_region(6, 2)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 2 / r2: 6, 2 / r3: 8, 1 / r4: 9, 2 / r5: 11, 0 / r6: 11, 0

>>> ign = sm.set_region(4, 4)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 4 / r2: 8, 1 / r3: 9, 2 / r4: 11, 0 / r5: 11, 0

>>> ign = sm.set_region(0, 10)
>>> printf(dump_regions(sm.regions))
r0: 0, 10 / r1: 10, 1 / r2: 11, 0 / r3: 11, 0

>>> ign = sm.set_region(4, 20)
>>> printf(dump_regions(sm.regions))
r0: 0, 4 / r1: 4, 7 / r2: 11, 0 / r3: 11, 0

>>> ign = sm.dump(immediate=True)
// |       ||  P || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ | _ _ | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     0 |   0 || | || 1 * * | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || * 1 * | 0 0 1 | _ _ 0 | _ 0 _ || 0 _ _ | 0 1 0 | 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || * * 1 | 0 _ _ | 1 0 0 | 0 0 1 || 0 _ _ | 1 0 0 | 0 1 | 0 1 | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     1 |   0 || | || 1 0 0 | 1 * * | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || _ 0 _ | * 1 * | _ 0 _ | 0 _ _ || _ _ _ | 1 0 0 | _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   2 || | || _ _ _ | * * 1 | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | _ _ | _ _ | 1 0 | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     2 |   0 || | || 0 _ _ | 0 _ _ | 1 * * | _ 0 _ || 0 _ _ | _ _ 0 | 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   1 || | || _ _ 0 | _ 0 _ | * 1 * | _ _ _ || _ _ _ | 0 _ _ | _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   2 || | || 1 0 0 | _ _ 0 | * * 1 | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     3 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | 1 * * || _ _ _ | 0 _ _ | _ _ | 1 0 | _ _ | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | * 1 * || _ 0 _ | _ 0 _ | 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   2 || | || 0 _ _ | 0 _ _ | _ _ 0 | * * 1 || 0 _ _ | _ _ 0 | 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     4 |   0 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 || 1 * * | _ 0 _ | 1 0 | _ _ | 0 1 | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || * 1 * | _ _ 0 | 0 1 | _ _ | 1 0 | 1 0 | _ _ |
// |       |   2 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 | _ _ 0 | _ _ | _ _ | _ _ | _ _ | 1 0 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     5 |   0 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ | 1 * * | _ _ | 0 1 | _ _ | _ _ | _ _ |
// |       |   1 || | || 0 1 0 | 0 0 1 | _ _ 0 | _ 0 _ || 0 _ _ | * 1 * | 0 1 | 1 0 | 1 0 | 1 0 | _ _ |
// |       |   2 || | || 1 0 0 | 1 0 0 | 0 _ _ | _ _ 0 || 1 0 0 | * * 1 | 1 0 | 1 0 | 0 1 | 0 1 | 0 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     6 |   0 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 * | _ _ | _ _ | 0 1 | _ _ |
// |       |   1 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | * 1 | _ _ | 1 0 | 1 0 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     7 |   0 || | || _ _ 0 | _ 0 _ | _ _ _ | _ _ _ || _ _ _ | 0 _ _ | _ _ | 1 * | _ _ | _ _ | _ _ |
// |       |   1 || | || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ | 1 0 0 | _ _ | * 1 | _ _ | _ _ | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     8 |   0 || | || _ _ _ | _ _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | _ _ | _ _ | 1 * | _ _ | _ _ |
// |       |   1 || | || 1 0 0 | _ _ 0 | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ | * 1 | 0 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |     9 |   0 || | || 0 _ _ | 0 _ _ | _ _ 0 | _ 0 _ || 0 _ _ | _ _ 0 | 0 1 | _ _ | 1 0 | 1 * | _ _ |
// |       |   1 || | || 1 0 0 | _ _ _ | 0 _ _ | _ _ 0 || _ 0 _ | _ 0 _ | 1 0 | _ _ | _ _ | * 1 | _ _ |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
// |    10 |   0 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ 0 | _ _ | _ _ | _ _ | _ _ | 1 * |
// |       |   1 || | || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ 0 | _ _ _ | _ _ | _ _ | _ _ | _ _ | * 1 |
// +-------+-----++-+-++-------+-------+-------+-------++-------+-------+-----+-----+-----+-----+-----+
superset_update_request(si, sj)[source]
Returns:self for chaining.
update_row(si, sj)[source]
Returns:row_changed
update_rows()[source]
Returns:self for chaining
update_superset_rows(si, sj)[source]
Returns:self for chaining
update_supersets()[source]
Returns:self for chaining
update_zeroes()[source]
Returns:self for chaining.
zero_change(si, sj, sg, sh, immediate=None)[source]
Returns:self for chaining.
zero_change_(si, sj, sg, sh, ri, ci, immediate=None)[source]
Returns:killed, changed.
class satoku.LoopMark(*args, **kwargs)[source]
satoku.parse_clauses_(string)[source]
>>> parse_clauses(TEST_PROBLEM)
([[[1, -1, -1, 0, -1], [0, 1, -1, -1, -1], [0, 0, 1, -1, -1]], [1, 0, 1, -1, -1], [0, 1, 0, -1, -1], [-1, 1, 0, 1], [-1, -1, 0, 1, 1], [[-1, 0, -1, -1, -1], [-1, 1, -1, 1, -1], [-1, 1, -1, 0, 0]]], [])

>>> parse_clauses(TEST_PROBLEM_NOCFL)
([[[1, -1, -1, 1, -1], [1, 1, -1, -1, -1], [1, 1, 1, -1, -1]], [1, 1, 1, -1, -1], [1, 1, 1, -1, -1], [-1, 1, 1, 1], [-1, -1, 1, 1, 1], [[-1, 1, -1, -1, -1], [-1, 1, -1, 1, -1], [-1, 1, -1, 1, 1]]], [])

>>> parse_clauses(TEST_PROBLEM_REGIONS)
([[[1, -1, -1, 0, -1], [0, 1, -1, -1, -1], [0, 0, 1, -1, -1]], [1, 0, 1, -1, -1], [0, 1, 0, -1, -1], [-1, 1, 0, 1], [-1, -1, 0, 1, 1], [[-1, 0, -1, -1, -1], [-1, 1, -1, 1, -1], [-1, 1, -1, 0, 0]]], [('r', '3 2 1 5 9 10')])
Returns:list of parsed clauses.
satoku.clean_clauses(string)[source]
>>> printf(clean_clauses(TEST_PROBLEM))
[[ 1 - - 0 - ]
[ 0 1 - - - ]
[ 0 0 1 - - ]]
[ 1 0 1 - - ]
[ 0 1 0 - - ]
- 1 0 1
- - 0 1 1
[ - 0 - - -
- 1 - 1 -
- 1 - 0 0 ]
Returns:list of parsed clauses.
satoku.parse_clauses(string)[source]
Returns:list of parsed clauses.
satoku.permute_cols(used_cols)[source]
Returns:clause with permuted columns. 
>>> printf(permute_cols([0, 2, 3]))
[ 0 _ 0 0 ]
[ 0 _ 0 1 ]
[ 0 _ 1 0 ]
[ 0 _ 1 1 ]
[ 1 _ 0 0 ]
[ 1 _ 0 1 ]
[ 1 _ 1 0 ]
[ 1 _ 1 1 ]
satoku.dump_regions(regions, start=None)[source]
Returns:string repr of regions

Copyright

Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.

Table Of Contents

Previous topic

Satoku Matrix

This Page

Navigation

© Copyright 2013, Wolfgang Scherer. Created using Sphinx 1.1.3.