satchmo (empty) → 1.0
raw patch · 19 files changed
+1283/−0 lines, 19 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, mtl, process
Files
- Satchmo/Binary.hs +128/−0
- Satchmo/Boolean.hs +14/−0
- Satchmo/Boolean/Data.hs +73/−0
- Satchmo/Boolean/Op.hs +41/−0
- Satchmo/Code.hs +39/−0
- Satchmo/Counting.hs +73/−0
- Satchmo/Data.hs +42/−0
- Satchmo/Internal.hs +50/−0
- Satchmo/Solve.hs +49/−0
- Setup.hs +2/−0
- TODO +8/−0
- gpl-2.0.txt +339/−0
- satchmo.cabal +30/−0
- test/Binary.hs +76/−0
- test/Cage.hs +58/−0
- test/HC.hs +76/−0
- test/Ramsey.hs +83/−0
- test/Schur.hs +65/−0
- test/VC.hs +37/−0
+ Satchmo/Binary.hs view
@@ -0,0 +1,128 @@+{-# language MultiParamTypeClasses #-}++module Satchmo.Binary ++( Number, width, number, fixed+, add, times+, equals+)++where++import Prelude hiding ( and, or, not )++import qualified Satchmo.Code as C+import Satchmo.Boolean+import Satchmo.Counting++type Booleans = [ Boolean ]++data Number = Number + { encode :: Booleans -- lsb first+ , decode :: C.Decoder Integer+ }++instance C.Decode Number Integer where+ decode = decode++width :: Number -> Int+width n = length $ encode n++-- | declare a number variable (bit width)+number :: Int -> SAT Number+number w = do+ xs <- sequence $ replicate w boolean+ return $ make xs++make :: [ Boolean ] -> Number+make xs = Number+ { encode = xs+ , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys+ }++fromBinary :: [ Bool ] -> Integer+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs++toBinary :: Int -> Integer -> [ Bool ]+toBinary 0 0 = []+toBinary b n | b > 0 = + let (d,m) = divMod n 2+ in toEnum ( fromIntegral m ) : toBinary (b-1) d++-- | declare a number constant (bit width, value)+fixed :: Int -> Integer -> SAT Number+fixed b n = do+ xs <- mapM constant $ toBinary b n+ return $ make xs++-- | result width is 1 + largest argument width+add :: Number -> Number -> SAT Number+add ( Number { encode = xs } ) ( Number { encode = ys } ) = do+ false <- constant False+ ( zs, carry ) <- add_with_carry false xs ys+ return $ make $ zs ++ [carry]++-- | result width is largest argument width+-- if overflow, then unsatisfiable+restricted_add :: Number -> Number -> SAT Number +restricted_add a b = do+ c <- add a b+ restricted ( max (width a) (width b)) c++-- | give only lower k bits, upper bits must be zero,+-- (else unsatisfiable)+restricted :: Int -> Number -> SAT Number+restricted w ( Number { encode = xs } ) = do+ let ( low, high ) = splitAt w xs+ sequence $ do x <- high ; return $ assert [ not x ]+ return $ make low++-- | result has max length of both inputs+add_with_carry :: Boolean + -> Booleans -> Booleans+ -> SAT ( Booleans, Boolean )+add_with_carry cin [] [] = return ( [], cin )+add_with_carry cin (x:xs) [] = do+ z <- xor [ cin, x ]+ c <- and [ cin, x ]+ ( zs, cout ) <- add_with_carry c xs []+ return ( z : zs, cout )+add_with_carry cin [] (y:ys) = do+ add_with_carry cin (y:ys) []+add_with_carry cin (x:xs ) (y:ys) = do+ z <- xor [ cin, x, y ]+ c <- atleast 2 [ cin, x, y ]+ ( zs, cout ) <- add_with_carry c xs ys+ return ( z : zs, cout )++times :: Number -> Number -> SAT Number+times ( Number { encode = [x] } ) ys = times1 x ys+times ( Number { encode = x:xs } ) ys = do+ xys <- times1 x ys+ xsys <- times (make xs) ys+ zs <- shift xsys+ add xys zs++-- | multiply by 2+shift :: Number -> SAT Number+shift ( Number { encode = xs } ) = do+ false <- constant False + return $ make $ false : xs++times1 :: Boolean -> Number -> SAT Number+times1 x ( Number { encode = ys } ) = do+ zs <- mapM ( \ y -> and [x,y] ) ys+ return $ make zs++equals :: Number -> Number -> SAT Boolean+equals ( Number { encode = xs } ) ( Number { encode = ys } ) = do+ equals' xs ys++equals' :: Booleans -> Booleans -> SAT Boolean+equals' [] [] = constant True+equals' (x:xs) (y:ys) = do+ z <- xor [x, y]+ rest <- equals' xs ys+ and [ not z, rest ]+equals' xs [] = and $ map not xs+equals' [] ys = and $ map not ys
+ Satchmo/Boolean.hs view
@@ -0,0 +1,14 @@+module Satchmo.Boolean ++( SAT+, module Satchmo.Boolean.Data+, module Satchmo.Boolean.Op+) ++where++import qualified Prelude++import Satchmo.Internal+import Satchmo.Boolean.Data+import Satchmo.Boolean.Op
+ Satchmo/Boolean/Data.hs view
@@ -0,0 +1,73 @@+{-# language MultiParamTypeClasses #-}++module Satchmo.Boolean.Data ++( Boolean, boolean, constant+, not, assert, monadic+)++where++import Prelude hiding ( not )+import qualified Prelude++import qualified Satchmo.Code as C++import Satchmo.Data +import Satchmo.Internal++import Data.Map ( Map )+import qualified Data.Map as M+import Data.Maybe ( fromJust )+import Data.List ( partition )++import Control.Monad.Reader++data Boolean = Boolean+ { encode :: Literal+ , decode :: C.Decoder Bool+ }+ | Constant { value :: Bool }++isConstant :: Boolean -> Bool+isConstant ( Constant {} ) = True+isConstant _ = False++instance C.Decode Boolean Bool where + decode b = case b of+ Boolean {} -> decode b+ Constant {} -> return $ value b++boolean :: SAT Boolean+boolean = do+ x <- fresh+ return $ Boolean + { encode = x+ , decode = asks $ \ fm -> fromJust $ M.lookup x fm+ }++constant :: Bool -> SAT Boolean+constant v = do+ return $ Constant { value = v } ++not :: Boolean -> Boolean+not b = case b of+ Boolean {} -> Boolean + { encode = nicht $ encode b+ , decode = do x <- decode b ; return $ Prelude.not x+ }+ Constant {} -> Constant { value = Prelude.not $ value b }++assert :: [ Boolean ] -> SAT ()+assert bs = do+ let ( con, uncon ) = partition isConstant bs+ let cval = Prelude.or $ map value con+ when ( Prelude.not cval ) $ emit $ clause $ map encode uncon++monadic :: Monad m+ => ( [ a ] -> m b )+ -> ( [ m a ] -> m b )+monadic f ms = do+ xs <- sequence ms+ f xs+
+ Satchmo/Boolean/Op.hs view
@@ -0,0 +1,41 @@+module Satchmo.Boolean.Op ++( constant+, and, or, xor+, monadic+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Internal+import Satchmo.Code+import Satchmo.Boolean.Data++and :: [ Boolean ] -> SAT Boolean+and xs = do+ y <- boolean+ sequence $ do+ x <- xs+ return $ assert [ not y, x ]+ assert $ y : map not xs+ return y++or :: [ Boolean ] -> SAT Boolean+or xs = do+ y <- and $ map not xs+ return $ not y++xor :: [ Boolean ] -> SAT Boolean+xor [x] = return x+xor (x : xs) = do+ rest <- xor xs+ xor2 x rest++xor2 :: Boolean -> Boolean -> SAT Boolean+xor2 x y = do+ a <- and [ x, not y ]+ b <- and [ not x, y ]+ or [ a, b ]+
+ Satchmo/Code.hs view
@@ -0,0 +1,39 @@+{-# language MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}++module Satchmo.Code ++( Decode (..)+, Decoder+)++where++import Satchmo.Data+++import Data.Map ( Map )+import qualified Data.Map as M+import Data.Array++import Control.Monad.Reader+++class Decode c a | c -> a where decode :: c -> Decoder a++type Decoder a = Reader ( Map Literal Bool ) a+++instance ( Decode c a, Decode d b ) => Decode ( c,d) (a,b) where+ decode (c,d) = do a <- decode c; b <- decode d; return ( a,b)++instance ( Decode c a ) => Decode [c] [a] where+ decode = mapM decode ++instance (Ix i, Decode c a) => Decode ( Array i c) ( Array i a ) where+ decode x = do+ pairs <- sequence $ do+ (i,e) <- assocs x+ return $ do+ f <- decode e+ return (i,f)+ return $ array (bounds x) pairs
+ Satchmo/Counting.hs view
@@ -0,0 +1,73 @@+module Satchmo.Counting ++( atleast+, atmost+, exactly+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean++atleast_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+atleast_block k [] = do+ t <- constant True+ f <- constant False+ return $ t : replicate k f+atleast_block k (x:xs) = do+ cs <- atleast_block k xs+ sequence $ do+ i <- [ 0 .. k ]+ return $ if i == 0 then return $ cs !! 0+ else do+ p <- and [ x, cs !! (i-1) ]+ or [ cs !! i, p ]++atleast :: Int -> [ Boolean ] -> SAT Boolean+atleast k xs = do+ cs <- atleast_block k xs+ return $ cs !! k+ ++atmost_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+atmost_block k [] = do+ t <- constant $ True+ return $ replicate (k+1) t+atmost_block k (x:xs) = do+ cs <- atmost_block k xs+ sequence $ do+ i <- [ 0 .. k ]+ return $ do+ f <- constant False+ p <- and [ x, if i > 0 then cs !! (i-1) else f ]+ q <- and [ not x, cs !! i ]+ or [ p, q ]++atmost :: Int -> [ Boolean ] -> SAT Boolean+atmost k xs = do+ cs <- atmost_block k xs+ return $ cs !! k+ ++exactly_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+exactly_block k [] = do+ t <- constant True+ f <- constant False+ return $ t : replicate k f+exactly_block k (x:xs) = do+ cs <- exactly_block k xs+ sequence $ do+ i <- [ 0 .. k ]+ return $ do+ f <- constant False+ p <- and [ x, if i > 0 then cs !! (i-1) else f ]+ q <- and [ not x, cs !! i ]+ or [ p, q ]++exactly :: Int -> [ Boolean ] -> SAT Boolean+exactly k xs = do+ cs <- exactly_block k xs+ return $ cs !! k+
+ Satchmo/Data.hs view
@@ -0,0 +1,42 @@+module Satchmo.Data ++( CNF, cnf, clauses+, Clause, clause, literals+, Literal, literal, nicht+)++where++import Control.Monad.State.Strict++data CNF = CNF { clauses :: [ Clause ] }++instance Show CNF where+ show ( CNF cs ) = unlines $ map show cs++cnf :: [ Clause ] -> CNF+cnf cs = CNF cs+++data Clause = Clause { literals :: [ Literal ] }++instance Show Clause where+ show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )++clause :: [ Literal ] -> Clause+clause ls = Clause { literals = ls }+++data Literal = Literal Int + deriving ( Eq, Ord )++instance Show Literal where + show ( Literal i ) = show i++literal :: Int -> Literal+literal i | i /= 0 = Literal i+++nicht :: Literal -> Literal+nicht ( Literal i ) = Literal $ negate i+
+ Satchmo/Internal.hs view
@@ -0,0 +1,50 @@+module Satchmo.Internal ++( SAT+, fresh, emit+, sat+)++where++import Satchmo.Data++import Control.Monad.State.Strict+import Control.Monad.Writer.Strict++data Accu = Accu + { next :: ! Int+ , size :: ! Int+ }++start :: Accu+start = Accu + { next = 1+ , size = 0+ }++type SAT a = WriterT [ Clause ] (State Accu) a++sat :: SAT a -> ( String, a )+sat m = + let ~( ~(a,w), accu) = runState ( runWriterT m ) start+ in ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]+ : map show w+ , a+ )+ +fresh :: SAT Literal+fresh = do+ a <- get+ put $ a { next = next a + 1 }+ return $ literal $ next a++emit :: Clause -> SAT ()+emit clause = do+ a <- get+ tell [ clause ]+ put $ a + { size = size a + 1 + }++
+ Satchmo/Solve.hs view
@@ -0,0 +1,49 @@+module Satchmo.Solve++( solve+, Decoder+)++where++import Satchmo.Data+import Satchmo.Code+import Satchmo.Internal++import Data.Map ( Map )+import qualified Data.Map as M++import Control.Monad.State+import Control.Monad.Reader+import System.Process+++solve :: SAT ( Decoder a )+ -> IO ( Maybe a )+solve build = do+ let (s, a) = sat build+ mfm <- run s+ case mfm of+ Nothing -> do+ putStrLn "not satisfiable"+ return Nothing+ Just fm -> do+ putStrLn "satisfiable"+ -- print fm+ return $ Just $ runReader a fm+ +run :: String -> IO ( Maybe ( Map Literal Bool ) )+run cs = do+ let debug = False+ if debug + then putStrLn cs+ else putStrLn $ head $ lines cs+ ( code, stdout, stderr ) <- + readProcessWithExitCode "minisat" [ "/dev/stdin", "/dev/stdout" ] cs+ when debug $ putStrLn stdout+ case lines stdout of+ "SAT" : xs : _ -> return $ Just $ M.fromList $ do+ x <- takeWhile ( /= 0 ) $ map read $ words xs+ let l = literal $ abs x+ return ( l, x > 0 )+ _ -> return $ Nothing
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TODO view
@@ -0,0 +1,8 @@+* minisat needs to be in the $PATH (for execution),+ but this is not checked during installation.++* actually, should provide several backends (separate package satchmo-minisat etc.,+ similar as hsql with backends like hsql-mysql etc.)++* need timeout handler for calling the SAT solver.+
+ gpl-2.0.txt view
@@ -0,0 +1,339 @@+ GNU GENERAL PUBLIC LICENSE+ Version 2, June 1991++ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The licenses for most software are designed to take away your+freedom to share and change it. By contrast, the GNU General Public+License is intended to guarantee your freedom to share and change free+software--to make sure the software is free for all its users. This+General Public License applies to most of the Free Software+Foundation's software and to any other program whose authors commit to+using it. (Some other Free Software Foundation software is covered by+the GNU Lesser General Public License instead.) You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+this service if you wish), that you receive source code or can get it+if you want it, that you can change the software or use pieces of it+in new free programs; and that you know you can do these things.++ To protect your rights, we need to make restrictions that forbid+anyone to deny you these rights or to ask you to surrender the rights.+These restrictions translate to certain responsibilities for you if you+distribute copies of the software, or if you modify it.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must give the recipients all the rights that+you have. You must make sure that they, too, receive or can get the+source code. And you must show them these terms so they know their+rights.++ We protect your rights with two steps: (1) copyright the software, and+(2) offer you this license which gives you legal permission to copy,+distribute and/or modify the software.++ Also, for each author's protection and ours, we want to make certain+that everyone understands that there is no warranty for this free+software. If the software is modified by someone else and passed on, we+want its recipients to know that what they have is not the original, so+that any problems introduced by others will not reflect on the original+authors' reputations.++ Finally, any free program is threatened constantly by software+patents. We wish to avoid the danger that redistributors of a free+program will individually obtain patent licenses, in effect making the+program proprietary. To prevent this, we have made it clear that any+patent must be licensed for everyone's free use or not licensed at all.++ The precise terms and conditions for copying, distribution and+modification follow.++ GNU GENERAL PUBLIC LICENSE+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION++ 0. This License applies to any program or other work which contains+a notice placed by the copyright holder saying it may be distributed+under the terms of this General Public License. The "Program", below,+refers to any such program or work, and a "work based on the Program"+means either the Program or any derivative work under copyright law:+that is to say, a work containing the Program or a portion of it,+either verbatim or with modifications and/or translated into another+language. (Hereinafter, translation is included without limitation in+the term "modification".) Each licensee is addressed as "you".++Activities other than copying, distribution and modification are not+covered by this License; they are outside its scope. The act of+running the Program is not restricted, and the output from the Program+is covered only if its contents constitute a work based on the+Program (independent of having been made by running the Program).+Whether that is true depends on what the Program does.++ 1. You may copy and distribute verbatim copies of the Program's+source code as you receive it, in any medium, provided that you+conspicuously and appropriately publish on each copy an appropriate+copyright notice and disclaimer of warranty; keep intact all the+notices that refer to this License and to the absence of any warranty;+and give any other recipients of the Program a copy of this License+along with the Program.++You may charge a fee for the physical act of transferring a copy, and+you may at your option offer warranty protection in exchange for a fee.++ 2. You may modify your copy or copies of the Program or any portion+of it, thus forming a work based on the Program, and copy and+distribute such modifications or work under the terms of Section 1+above, provided that you also meet all of these conditions:++ a) You must cause the modified files to carry prominent notices+ stating that you changed the files and the date of any change.++ b) You must cause any work that you distribute or publish, that in+ whole or in part contains or is derived from the Program or any+ part thereof, to be licensed as a whole at no charge to all third+ parties under the terms of this License.++ c) If the modified program normally reads commands interactively+ when run, you must cause it, when started running for such+ interactive use in the most ordinary way, to print or display an+ announcement including an appropriate copyright notice and a+ notice that there is no warranty (or else, saying that you provide+ a warranty) and that users may redistribute the program under+ these conditions, and telling the user how to view a copy of this+ License. (Exception: if the Program itself is interactive but+ does not normally print such an announcement, your work based on+ the Program is not required to print an announcement.)++These requirements apply to the modified work as a whole. If+identifiable sections of that work are not derived from the Program,+and can be reasonably considered independent and separate works in+themselves, then this License, and its terms, do not apply to those+sections when you distribute them as separate works. But when you+distribute the same sections as part of a whole which is a work based+on the Program, the distribution of the whole must be on the terms of+this License, whose permissions for other licensees extend to the+entire whole, and thus to each and every part regardless of who wrote it.++Thus, it is not the intent of this section to claim rights or contest+your rights to work written entirely by you; rather, the intent is to+exercise the right to control the distribution of derivative or+collective works based on the Program.++In addition, mere aggregation of another work not based on the Program+with the Program (or with a work based on the Program) on a volume of+a storage or distribution medium does not bring the other work under+the scope of this License.++ 3. You may copy and distribute the Program (or a work based on it,+under Section 2) in object code or executable form under the terms of+Sections 1 and 2 above provided that you also do one of the following:++ a) Accompany it with the complete corresponding machine-readable+ source code, which must be distributed under the terms of Sections+ 1 and 2 above on a medium customarily used for software interchange; or,++ b) Accompany it with a written offer, valid for at least three+ years, to give any third party, for a charge no more than your+ cost of physically performing source distribution, a complete+ machine-readable copy of the corresponding source code, to be+ distributed under the terms of Sections 1 and 2 above on a medium+ customarily used for software interchange; or,++ c) Accompany it with the information you received as to the offer+ to distribute corresponding source code. (This alternative is+ allowed only for noncommercial distribution and only if you+ received the program in object code or executable form with such+ an offer, in accord with Subsection b above.)++The source code for a work means the preferred form of the work for+making modifications to it. For an executable work, complete source+code means all the source code for all modules it contains, plus any+associated interface definition files, plus the scripts used to+control compilation and installation of the executable. However, as a+special exception, the source code distributed need not include+anything that is normally distributed (in either source or binary+form) with the major components (compiler, kernel, and so on) of the+operating system on which the executable runs, unless that component+itself accompanies the executable.++If distribution of executable or object code is made by offering+access to copy from a designated place, then offering equivalent+access to copy the source code from the same place counts as+distribution of the source code, even though third parties are not+compelled to copy the source along with the object code.++ 4. You may not copy, modify, sublicense, or distribute the Program+except as expressly provided under this License. Any attempt+otherwise to copy, modify, sublicense or distribute the Program is+void, and will automatically terminate your rights under this License.+However, parties who have received copies, or rights, from you under+this License will not have their licenses terminated so long as such+parties remain in full compliance.++ 5. You are not required to accept this License, since you have not+signed it. However, nothing else grants you permission to modify or+distribute the Program or its derivative works. These actions are+prohibited by law if you do not accept this License. Therefore, by+modifying or distributing the Program (or any work based on the+Program), you indicate your acceptance of this License to do so, and+all its terms and conditions for copying, distributing or modifying+the Program or works based on it.++ 6. Each time you redistribute the Program (or any work based on the+Program), the recipient automatically receives a license from the+original licensor to copy, distribute or modify the Program subject to+these terms and conditions. You may not impose any further+restrictions on the recipients' exercise of the rights granted herein.+You are not responsible for enforcing compliance by third parties to+this License.++ 7. If, as a consequence of a court judgment or allegation of patent+infringement or for any other reason (not limited to patent issues),+conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot+distribute so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you+may not distribute the Program at all. For example, if a patent+license would not permit royalty-free redistribution of the Program by+all those who receive copies directly or indirectly through you, then+the only way you could satisfy both it and this License would be to+refrain entirely from distribution of the Program.++If any portion of this section is held invalid or unenforceable under+any particular circumstance, the balance of the section is intended to+apply and the section as a whole is intended to apply in other+circumstances.++It is not the purpose of this section to induce you to infringe any+patents or other property right claims or to contest validity of any+such claims; this section has the sole purpose of protecting the+integrity of the free software distribution system, which is+implemented by public license practices. Many people have made+generous contributions to the wide range of software distributed+through that system in reliance on consistent application of that+system; it is up to the author/donor to decide if he or she is willing+to distribute software through any other system and a licensee cannot+impose that choice.++This section is intended to make thoroughly clear what is believed to+be a consequence of the rest of this License.++ 8. If the distribution and/or use of the Program is restricted in+certain countries either by patents or by copyrighted interfaces, the+original copyright holder who places the Program under this License+may add an explicit geographical distribution limitation excluding+those countries, so that distribution is permitted only in or among+countries not thus excluded. In such case, this License incorporates+the limitation as if written in the body of this License.++ 9. The Free Software Foundation may publish revised and/or new versions+of the General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++Each version is given a distinguishing version number. If the Program+specifies a version number of this License which applies to it and "any+later version", you have the option of following the terms and conditions+either of that version or of any later version published by the Free+Software Foundation. If the Program does not specify a version number of+this License, you may choose any version ever published by the Free Software+Foundation.++ 10. If you wish to incorporate parts of the Program into other free+programs whose distribution conditions are different, write to the author+to ask for permission. For software which is copyrighted by the Free+Software Foundation, write to the Free Software Foundation; we sometimes+make exceptions for this. Our decision will be guided by the two goals+of preserving the free status of all derivatives of our free software and+of promoting the sharing and reuse of software generally.++ NO WARRANTY++ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,+REPAIR OR CORRECTION.++ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE+POSSIBILITY OF SUCH DAMAGES.++ END OF TERMS AND CONDITIONS++ How to Apply These Terms to Your New Programs++ If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++ To do so, attach the following notices to the program. It is safest+to attach them to the start of each source file to most effectively+convey the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++ <one line to give the program's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ This program is free software; you can redistribute it and/or modify+ it under the terms of the GNU General Public License as published by+ the Free Software Foundation; either version 2 of the License, or+ (at your option) any later version.++ This program is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU General Public License for more details.++ You should have received a copy of the GNU General Public License along+ with this program; if not, write to the Free Software Foundation, Inc.,+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.++Also add information on how to contact you by electronic and paper mail.++If the program is interactive, make it output a short notice like this+when it starts in an interactive mode:++ Gnomovision version 69, Copyright (C) year name of author+ Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+ This is free software, and you are welcome to redistribute it+ under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License. Of course, the commands you use may+be called something other than `show w' and `show c'; they could even be+mouse-clicks or menu items--whatever suits your program.++You should also get your employer (if you work as a programmer) or your+school, if any, to sign a "copyright disclaimer" for the program, if+necessary. Here is a sample; alter the names:++ Yoyodyne, Inc., hereby disclaims all copyright interest in the program+ `Gnomovision' (which makes passes at compilers) written by James Hacker.++ <signature of Ty Coon>, 1 April 1989+ Ty Coon, President of Vice++This General Public License does not permit incorporating your program into+proprietary programs. If your program is a subroutine library, you may+consider it more useful to permit linking proprietary applications with the+library. If this is what you want to do, use the GNU Lesser General+Public License instead of this License.
+ satchmo.cabal view
@@ -0,0 +1,30 @@+Name: satchmo+Version: 1.0+License: GPL+License-file: gpl-2.0.txt+Author: Johannes Waldmann+Maintainer: Johannes Waldmann+Homepage: http://dfa.imn.htwk-leipzig.de/satchmo/+Category: Testing+Synopsis: SAT encoding monad+description: Encoding for boolean and integral constraints into CNF-SAT.+ The encoder is provided as a State monad (hence the "mo" in "satchmo").+ Requires SAT solver minisat installed.+Build-depends: mtl, process, containers, base, array+Exposed-modules:+ Satchmo.Boolean+ Satchmo.Solve+ Satchmo.Counting+ Satchmo.Binary+ Satchmo.Code+Other-modules:+ Satchmo.Boolean.Data+ Satchmo.Boolean.Op+ Satchmo.Internal+ Satchmo.Data+hs-source-dirs: .+extra-source-files: test/Binary.hs test/HC.hs test/Schur.hs+ test/Cage.hs test/Ramsey.hs test/VC.hs+ TODO+extensions: +build-type: Simple
+ test/Binary.hs view
@@ -0,0 +1,76 @@+-- | run tests like this: "solve test2"++import Prelude hiding ( not )++import Satchmo.Boolean+import Satchmo.Code+import Satchmo.Binary+import Satchmo.Solve+++assert_positive x = do + n <- fixed 0 0 + e <- equals n x + assert [ not e ]++assert_equals x y = do + e <- equals x y + assert [ e ]++assert_lt x y = do + d <- number $ width y+ assert_positive d+ xd <- add x d+ assert_equals xd y++test1 = do + x <- number 4 + y <- fixed 4 12 + assert_equals x y+ return $ decode (x,y)++test2 = do + x <- fixed 5 3+ y <- fixed 5 9+ z <- add x y+ return $ decode [x,y,z]++test3 = do + x <- number 5 + xx <- add x x+ xxx <- add xx x+ y <- fixed 5 15 + assert_equals xxx y + return $ decode [ x, y ]++test4 = do + x <- number 8+ y <- number 8+ xy <- times x y+ z <- fixed 8 63+ assert_equals xy z+ return $ decode [x, y, z]++test5 = do + x <- number 8+ y <- number 8+ xy <- times x y+ z <- fixed 10 1001+ assert_equals xy z+ return $ decode [x, y, z]++ramanujan = do+ let bits = 5+ a <- number bits+ b <- number bits+ c <- number bits+ d <- number bits++ assert_lt a c ; assert_lt c d ; assert_lt d b++ let cube x = do x2 <- times x x ; times x2 x+ a3 <- cube a; b3 <- cube b; ab <- add a3 b3+ c3 <- cube c; d3 <- cube d; cd <- add c3 d3+ assert_equals ab cd++ return $ decode [a,b,c,d]
+ test/Cage.hs view
@@ -0,0 +1,58 @@+import Prelude hiding ( not )++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Solve++import Data.List ( inits, tails )+import System.Environment++-- | command line arguments: r g n+-- program looks for a (r,g) cage:+-- r-regular graph with girth g on n nodes++main :: IO ()+main = do+ argv <- getArgs+ let [ r, g, n ] = map read argv+ Just a <- solve $ cage r g n+ putStrLn $ table a++type Graph = Relation Int Int++cage r g n = do+ a <- relation ((1,1),(n,n))+ monadic assert [ symmetric a ]+ monadic assert [ irreflexive a ]+ monadic assert [ regular r a ]+ girth_at_least g a+ return $ decode a++girth_at_least :: Int -> Graph -> SAT ()+girth_at_least k g = sequence_ $ do+ let ((lo,_),(hi,_)) = bounds g+ c <- [ 3 .. k-1 ]+ xs <- sublists c [lo .. hi]+ return $ assert_no_circle xs g+ +assert_no_circle xs g = + assert $ do + (x,y) <- zip xs $ rotate 1 xs+ return $ not $ g ! (x,y)+ +sublists :: Int -> [a] -> [[a]]+sublists 0 xs = return []+sublists k xs = do+ ( pre, this : post ) <- splits xs+ that <- sublists (k-1) $ pre ++ post+ return $ this : that++splits :: [a] -> [ ([a],[a]) ]+splits xs = zip ( inits xs ) ( tails xs )++rotate :: Int -> [a] -> [a]+rotate k xs = + let ( pre, post ) = splitAt k xs+ in post ++ pre
+ test/HC.hs view
@@ -0,0 +1,76 @@+{-# language ScopedTypeVariables #-}++import Prelude hiding ( not )+import qualified Prelude++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Solve++import Data.List (sort)+import qualified Data.Array as A+import Control.Monad ( guard, when )+import System.Environment++-- | command line arguments: m n+-- compute knight's tour on m x n chess board++main :: IO ()+main = do+ argv <- getArgs+ let [ m, n ] = map read argv+ Just a <- solve $ tour m n+ putStrLn $ unlines $ do+ let ((u,l),(o,r)) = A.bounds a+ x <- [u .. o]+ return $ unwords $ do + y <- [ l ..r ]+ return $ fill 4 $ show $ a A.! (x,y)++fill k cs = replicate (k - length cs) ' ' ++ cs++tour m n = do+ let s = m * n+ p :: Relation Int (Int,Int) <- bijection ((1,(1,1)), (s,(m,n)))+ sequence_ $ do+ (i,j) <- zip [1..s] $ rotate 1 [1..s]+ a <- A.range ((1,1),(m,n))+ return $ do+ assert $ not ( p!(i,a)) : do+ b <- A.range ((1,1),(m,n))+ guard $ reaches a b+ return $ p ! (j,b) + assert $ not ( p!(j,a)) : do+ b <- A.range ((1,1),(m,n))+ guard $ reaches a b+ return $ p ! (i,b) + return $ do+ a <- decode p+ return $ A.array ((1,1),(m,n)) $ do+ ((i,p),True) <- A.assocs a+ return (p,i)++bijection :: (A.Ix a, A.Ix b) + => ((a,b),(a,b)) + -> SAT ( Relation a b )+bijection bnd = do+ let ((u,l),(o,r)) = bnd+ a <- relation bnd+ sequence_ $ do+ x <- A.range (u,o)+ return $ monadic assert $ return $ exactly 1 $ do y <- A.range (l,r) ; return $ a!(x,y)+ sequence_ $ do+ y <- A.range (l,r)+ return $ monadic assert $ return $ exactly 1 $ do x <- A.range (u,o) ; return $ a!(x,y)+ return a ++reaches (px,py) (qx,qy) = + 5 == (px - qx)^2 + (py - qy)^2++rotate :: Int -> [a] -> [a]+rotate k xs = + let ( pre, post ) = splitAt k xs+ in post ++ pre+
+ test/Ramsey.hs view
@@ -0,0 +1,83 @@+import Prelude hiding ( not )+import qualified Prelude++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Solve++import Data.List ( inits, tails )+import Data.Ix+import qualified Data.Array as A+import Control.Monad ( forM, guard )+import System.Environment++-- | command line arguments: c_1 .. c_k n+-- program prints graph g that proves+-- R(c_1, .., c_k) > n++main :: IO ()+main = do+ argv <- fmap ( map read ) getArgs+ let cs = init argv+ n = last argv+ Just a <- solve $ ramsey cs n+ print a++type Graph = Relation Int Int++ramsey cs n = do+ cols <- sequence $ replicate (length cs) $ do+ r <- relation ((1,1),(n,n))+ monadic assert [ symmetric r ]+ monadic assert [ irreflexive r ]+ return r+ circular_colouring ( n `div` length cs ) cols+ each_edge_is_coloured n cols+ forM ( zip cs cols ) no_monochromatic_clique+ return $ do+ ds <- mapM decode cols+ return $ do+ i <- range ((1,1),(n,n))+ let c = length $ takeWhile Prelude.not $ do d <- ds ; return $ d A.! i+ return ( i, c )++circular_colouring period cols = sequence_ $ do+ (col, col') <- zip cols $ rotate 1 cols+ x @ (p,q) <- indices col+ let y = (p+period,q+period)+ guard $ inRange ( bounds col ) y+ return $ do+ assert [ not $ col ! x, col' ! y ]++rotate :: Int -> [a] -> [a]+rotate k xs = + let ( pre, post ) = splitAt k xs+ in post ++ pre++each_edge_is_coloured n cols = sequence_ $ do+ (p,q) <- range ((1,1),(n,n))+ guard $ p < q+ return $ assert $ do + col <- cols+ return $ col ! (p,q)++no_monochromatic_clique (c, col) = sequence_ $ do+ let ((lo,_),(hi,_)) = bounds col+ xs <- ordered_sublists c [lo .. hi]+ return $ assert $ do+ x : ys <- tails xs+ y <- ys+ return $ not $ col!(x,y)++ordered_sublists :: Int -> [a] -> [[a]]+ordered_sublists 0 xs = return []+ordered_sublists k xs = do+ ( pre, this : post ) <- splits xs+ that <- ordered_sublists (k-1) $ post+ return $ this : that++splits :: [a] -> [ ([a],[a]) ]+splits xs = zip ( inits xs ) ( tails xs )+
+ test/Schur.hs view
@@ -0,0 +1,65 @@+import Prelude hiding ( not, or, and )++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Solve++import Data.List ( inits, tails )+import qualified Data.Array as A+import System.Environment+import Control.Monad ( guard, forM_ )++-- | command line arguments: c n+-- program looks for sum-free c-colouring of [1 .. n]++main :: IO ()+main = do+ argv <- getArgs+ let [ c, n ] = map read argv+ Just a <- solve $ schur c n+ putStrLn $ table a+ print $ do+ o <- [ 1 .. c ]+ return ( o, length $ do i <- [ 1 .. n ]; guard $ a A.! (i,o) )++schur c n = do+ col <- relation ((1,1),(n,c))+ each_number_coloured col+ sum_free_colouring col+ return $ decode col++periodic p col = sequence_ $ do+ let ((1,1),(n,c)) = bounds col+ x <- [ 1 .. n ]+ let y = x + p+ guard $ y <= n+ o <- [ 1 .. c ]+ let p = 1 + o `mod` c+ return $ assert [ not $ col!(x,o), col!(y,p) ]++each_number_coloured col = sequence_ $ do+ let ((1,1),(n,c)) = bounds col+ x <- [ 1 .. n ]+ return $ assert $ do o <- [1 .. c]; return $ col!(x,o)++sum_free_colouring col = sequence_ $ do+ let ((1,1),(n,c)) = bounds col+ x <- [ 1 .. n ]+ y <- [ x .. n ]+ let z = (x + y) `mod` (n+1)+ guard $ z <= n+ guard $ 1 <= z+ o <- [1 .. c]+ return $ assert $ do + p <- [ x, y, z ]+ return $ not $ col!(p,o)++evenly_distributed col = do+ let ((1,1),(n,c)) = bounds col+ d = n `div` c+ forM_ [ 1 .. c ] $ \ o -> do+ a <- atleast d $ do i <- [ 1 .. n ] ; return $ col!(i,o)+ assert [a]+
+ test/VC.hs view
@@ -0,0 +1,37 @@+import Prelude hiding ( not )++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Solve++import Control.Monad ( guard )+import System.Environment++-- | command line arguments: n s+-- compute vertex cover of size <= s for knight's graph on n x n chess board++main :: IO ()+main = do+ argv <- getArgs+ let [ n, s ] = map read argv+ Just a <- solve $ knight n s+ putStrLn $ table a++knight n s = do+ a <- relation ((1,1),(n,n))+ m <- atmost s $ do i <- indices a ; return $ a ! i+ assert [m]+ sequence_ $ do+ p <- indices a+ return $ assert $ do+ q <- indices a+ guard $ p == q || reaches p q+ return $ a!q+ return $ decode a+ +reaches (px,py) (qx,qy) = + 5 == (px - qx)^2 + (py - qy)^2++