]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8fc7908) | patch
Add a sorting network implementation. This code is not currently enabled so this...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 11 Aug 2010 00:58:57 +0000 (00:58 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 11 Aug 2010 00:58:57 +0000 (00:58 +0000)
commitf2e22c0cd74a767aa166d5de3c36897263eb5aae
tree8b58a264fa43921fe7596ffef86357744f3b8a5atree | snapshot
parent8fc7908d294994ad1111b905b4fb03add25b5934commit | diff
Add a sorting network implementation. This code is not currently enabled so this patch should do nothing.

Sorting networks should have better propagation (at higher cost) than addition networks (which we currently encode multiplication to).

In my experiments the sorting networks aren't clearly better than the addition networks.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@979 e59a4935-1847-0410-ae03-e826735625c1
src/to-sat/BitBlaster.cpp diff | blob | history
src/to-sat/BitBlaster.h diff | blob | history
STP Constraint Solver.