minisat-solver (empty) → 0.1
raw patch · 23 files changed
+4409/−0 lines, 23 filesdep +basedep +containersdep +easyrendersetup-changedbinary-added
Dependencies added: base, containers, easyrender, minisat-solver, transformers
Files
- ChangeLog +2/−0
- LICENSE +22/−0
- SAT/MiniSat.hs +50/−0
- SAT/MiniSat/Formula.hs +505/−0
- SAT/MiniSat/Functional.hs +28/−0
- SAT/MiniSat/Literals.hs +25/−0
- SAT/MiniSat/LowLevel.hs +77/−0
- SAT/MiniSat/Monadic.hs +199/−0
- SAT/MiniSat/Variable.hs +78/−0
- Setup.hs +2/−0
- c-sources/ChangeLog +70/−0
- c-sources/LICENSE.MiniSat +20/−0
- c-sources/LICENSE.bc_minisat_all +4/−0
- c-sources/Makefile +116/−0
- c-sources/README.html +202/−0
- c-sources/README.pdf binary
- c-sources/main.c +345/−0
- c-sources/solver.c +1587/−0
- c-sources/solver.h +215/−0
- c-sources/vec.h +111/−0
- examples/Sudoku.hs +203/−0
- examples/Woodblocks.hs +401/−0
- minisat-solver.cabal +147/−0
+ ChangeLog view
@@ -0,0 +1,2 @@+v0.1 2016/10/24+ Initial public release.
+ LICENSE view
@@ -0,0 +1,22 @@+MiniSat -- Copyright (c) 2005 Niklas Sorensson+bc_minisat_all -- Copyright (c) 2015 Takahisa Toda+Haskell bindings -- Copyright (c) 2016 Peter Selinger++Permission is hereby granted, free of charge, to any person obtaining a+copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ SAT/MiniSat.hs view
@@ -0,0 +1,50 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | This module provides high-level Haskell bindings for the well-known+-- MiniSat satisfiability solver. It solves the boolean satisfiability+-- problem, i.e., the input is a boolean formula, and the output is a+-- list of all satisfying assignments. MiniSat is a fully automated,+-- well-optimized general-purpose SAT solver written by Niklas Een and+-- Niklas Sorensson, and further modified by Takahisa Toda.+--+-- Unlike other similar Haskell packages, the purpose of this library+-- is not to provide access to low-level C functions, to give the user+-- fine-grained interactive control over the SAT solver, or to provide+-- building blocks for developing new SAT solvers. Rather, we package+-- the SAT solver as a general-purpose tool that can easily be+-- integrated into other programs as a turn-key solution to many+-- search problems.+-- +-- It is well-known that the boolean satisfiability problem is+-- NP-complete, and therefore, no SAT solver can be efficient for all+-- inputs. However, there are many search problems that can be+-- naturally expressed as satisfiability problems and are nevertheless+-- tractable. Writing custom code to traverse the search space is+-- tedious and rarely efficient, especially in cases where the size of+-- the search space is sensitive to the order of traversal. This is+-- where using a general-purpose SAT solver can often be a time saver.+--+-- We provide a convenient high-level interface to the SAT solver,+-- hiding the complexity of the underlying C implementation. The main+-- API function is 'solve_all', which inputs a boolean formula, and+-- outputs a list of all satisfying assignments (which are modelled as+-- maps from variables to truth values). The list is generated lazily,+-- so that the underlying low-level C code only does as much work as+-- necessary.+--+-- Two example programs illustrating the use of this library can be+-- found in the \"examples\" directory of the Cabal package.++module SAT.MiniSat (+ -- * Boolean formulas+ Formula(..),+ -- * SAT solver interface+ satisfiable,+ solve,+ solve_all+ ) where++import SAT.MiniSat.Formula
+ SAT/MiniSat/Formula.hs view
@@ -0,0 +1,505 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | This module extends the SAT solver to arbitrary boolean formulas+-- (not necessarily in conjunctive normal form). This is done by the+-- standard trick of translating each boolean formula to a CNF,+-- preserving satisfiability and the number of solutions. The+-- translation is carefully done in such a way that the size of the+-- CNF is linear in the size of the formula.++module SAT.MiniSat.Formula where++import SAT.MiniSat.Variable+import SAT.MiniSat.Literals++import Control.Monad.Trans.State+import Control.Monad+import qualified Data.Map as Map+import Data.Map (Map)+import Data.Maybe+import Prelude hiding (all)++-- ----------------------------------------------------------------------+-- * Boolean formulas++-- | The type of boolean formulas. It is parametric over a set of+-- variables /v/. We provide the usual boolean operators, including+-- implications and exclusive or. For convenience, we also provide the+-- list quantifiers 'All', 'Some', 'None', 'ExactlyOne', and+-- 'AtMostOne', as well as a general 'Let' operator that can be+-- used to reduce the size of repetitive formulas.++data Formula v =+ Var v -- ^ A variable.+ | Yes -- ^ The formula /true/.+ | No -- ^ The formula /false/.+ | Not (Formula v) -- ^ Negation.+ | Formula v :&&: Formula v -- ^ Conjunction.+ | Formula v :||: Formula v -- ^ Disjunction.+ | Formula v :++: Formula v -- ^ Exclusive or.+ | Formula v :->: Formula v -- ^ Implication.+ | Formula v :<->: Formula v -- ^ If and only if.+ | All [Formula v] -- ^ All are true.+ | Some [Formula v] -- ^ At least one is true.+ | None [Formula v] -- ^ None are true.+ | ExactlyOne [Formula v] -- ^ Exactly one is true.+ | AtMostOne [Formula v] -- ^ At most one is true.+ | Let (Formula v) (Formula v -> Formula v)+ -- ^ 'Let' /a/ /f/ is the formula \"let /x/=/a/ in /fx/\",+ -- which permits the subexpression /a/ to be re-used. It+ -- is logically equivalent to /fa/, but typically smaller.+ | Bound Integer -- ^ For internal use only.++infixr 6 :&&:+infixr 5 :||:+infixr 4 :++:+infixr 2 :->:+infix 1 :<->:++instance (Eq v) => Eq (Formula v) where+ a == b = exformula 0 a == exformula 0 b++instance (Ord v) => Ord (Formula v) where+ compare a b = compare (exformula 0 a) (exformula 0 b)++instance (Show v) => Show (Formula v) where+ showsPrec d a = showsPrec d (exformula 0 a)++-- ----------------------------------------------------------------------+-- * Explicit formulas++-- | Same as 'Formula', except it uses explicit bound variables. This is+-- only used to define 'Eq', 'Ord', and 'Show' instances for+-- 'Formula'.+data ExFormula v =+ ExVar v -- ^ A variable.+ | ExTrue -- ^ The formula /true/.+ | ExFalse -- ^ The formula /false/.+ | ExNot (ExFormula v) -- ^ Negation.+ | ExAnd (ExFormula v) (ExFormula v) -- ^ Conjunction.+ | ExOr (ExFormula v) (ExFormula v) -- ^ Disjunction.+ | ExXOr (ExFormula v) (ExFormula v) -- ^ Exclusive or.+ | ExImp (ExFormula v) (ExFormula v) -- ^ Implication.+ | ExIff (ExFormula v) (ExFormula v) -- ^ If and only if.+ | ExAll [ExFormula v] -- ^ All are true.+ | ExSome [ExFormula v] -- ^ At least one is true.+ | ExNone [ExFormula v] -- ^ None are true.+ | ExExactlyOne [ExFormula v] -- ^ Exactly one is true.+ | ExAtMostOne [ExFormula v] -- ^ At most one is true.+ | ExLet Integer (ExFormula v) (ExFormula v) -- ^ Let.+ | ExBound Integer -- ^ Bound variable.+ deriving (Eq, Ord)++-- | Convert a 'Formula' to an 'ExFormula'. The first argument is the+-- current nesting depth of let binders.+exformula :: Integer -> Formula v -> ExFormula v+exformula i (Var v) = ExVar v+exformula i Yes = ExTrue+exformula i No = ExFalse+exformula i (Not a) = ExNot (exformula i a)+exformula i (a :&&: b) = ExAnd (exformula i a) (exformula i b)+exformula i (a :||: b) = ExOr (exformula i a) (exformula i b)+exformula i (a :++: b) = ExXOr (exformula i a) (exformula i b)+exformula i (a :->: b) = ExImp (exformula i a) (exformula i b)+exformula i (a :<->: b) = ExIff (exformula i a) (exformula i b)+exformula i (All vs) = ExAll [exformula i v | v <- vs]+exformula i (Some vs) = ExSome [exformula i v | v <- vs]+exformula i (None vs) = ExNone [exformula i v | v <- vs]+exformula i (ExactlyOne vs) = ExExactlyOne [exformula i v | v <- vs]+exformula i (AtMostOne vs) = ExAtMostOne [exformula i v | v <- vs]+exformula i (Let a f) = ExLet i (exformula i a) (exformula (i+1) (f (Bound i)))+exformula i (Bound x)+ | 0 <= x && x < i = ExBound x+ | otherwise = error "MiniSat.Formula: 'Bound' is for internal use only"++-- | Names for bound variables.+variables :: [String]+variables = vs ++ [ v ++ show n | n <- [1..], v <- vs ]+ where+ vs = ["x", "y", "z", "u", "v", "w", "r", "s", "t"]++-- | Convert an integer to a bound variable name.+showBound :: Integer -> ShowS+showBound i = showString (variables !! (fromInteger i))++-- | The 'Show' instance of 'ExFormula' actually shows the corresponding+-- 'Formula'. We omit parentheses between associative identical+-- operators, but show some additional parentheses between different+-- operators for clarity.+instance (Show v) => Show (ExFormula v) where+ showsPrec d (ExVar v) = showParen (d > 10) $+ showString "Var " . showsPrec d v+ showsPrec d ExTrue = showString "Yes"+ showsPrec d ExFalse = showString "No"+ showsPrec d (ExNot a) = showParen (d > 10) $+ showString "Not " . showsPrec 11 a+ showsPrec d (ExAnd a b) = showParen (d > 6 || d == 4 || d == 5) $+ showsPrec 6 a . showString " :&&: " . showsPrec 6 b+ showsPrec d (ExOr a b) = showParen (d > 5 || d == 4) $+ showsPrec 5 a . showString " :||: " . showsPrec 5 b+ showsPrec d (ExXOr a b) = showParen (d > 4) $+ showsPrec 4 a . showString " :++: " . showsPrec 4 b+ showsPrec d (ExImp a b) = showParen (d > 2) $+ showsPrec 3 a . showString " :->: " . showsPrec 2 b+ showsPrec d (ExIff a b) = showParen (d > 1) $+ showsPrec 3 a . showString " :<->: " . showsPrec 3 b+ showsPrec d (ExAll as) = showParen (d > 10) $+ showString "All " . showsPrec 11 as+ showsPrec d (ExSome as) = showParen (d > 10) $+ showString "Some " . showsPrec 11 as+ showsPrec d (ExNone as) = showParen (d > 10) $+ showString "None " . showsPrec 11 as+ showsPrec d (ExExactlyOne as) = showParen (d > 10) $+ showString "ExactlyOne " . showsPrec 11 as+ showsPrec d (ExAtMostOne as) = showParen (d > 10) $+ showString "AtMostOne " . showsPrec 11 as+ showsPrec d (ExLet i a b) = showParen (d > 10) $+ showString "Let " . showsPrec 11 a . showString " (\\"+ . showBound i . showString " -> " . showsPrec 0 b . showString ")"+ showsPrec d (ExBound i) = showBound i++-- ----------------------------------------------------------------------+-- * Desugaring++-- | A version of 'Let' that binds a list of variables.+let_list :: [Formula v] -> ([Formula v] -> Formula v) -> Formula v+let_list [] f = f []+let_list (a:as) f = Let a (\x -> let_list as (\xs -> f (x:xs)))++-- | Implementation of 'All'.+all :: [Formula v] -> Formula v+all vs = foldl (:&&:) Yes vs++-- | Implementation of 'Some'.+some :: [Formula v] -> Formula v+some vs = foldl (:||:) No vs++-- | Implementation of 'None'.+none :: [Formula v] -> Formula v+none vs = Not (some vs)++-- | Implementation of 'AtMostOne'. Note that this translation is linear.+-- Without 'Let', the size of the translated formula would be /O/(/n/^2).+atMostOne :: [Formula v] -> Formula v+atMostOne [] = Yes+atMostOne [a] = Yes+atMostOne (a1:a2:as) =+ Let a1 (\x1 ->+ Let a2 (\x2 ->+ Not (x1 :&&: x2) :&&: atMostOne ((x1 :||: x2) : as)))++-- | Implementation of 'ExactlyOne'.+exactlyOne :: [Formula v] -> Formula v+exactlyOne as = let_list as (\xs -> some xs :&&: atMostOne xs)++-- ----------------------------------------------------------------------+-- * Reduced boolean formulas++-- | A reduced boolean formula doesn't contain the constants \"true\" or+-- \"false\", nor the connectives \"and\", \"implies\", or \"iff\",+-- nor list quantifiers. We use reduced formulas as an intermediate+-- representation between boolean formulas and De Morgan normal forms.+-- The primary purpose of this is to get rid of the constants \"true\"+-- and \"false\" in absorbing positions (i.e., \"/a/ or true\", \"/b/+-- and false\").+data RFormula v =+ RFVar v -- ^ A variable.+ | RFBound Integer -- ^ A bound variable.+ | RFNot (RFormula v) -- ^ Negation.+ | RFOr (RFormula v) (RFormula v) -- ^ Disjunction.+ | RFXOr (RFormula v) (RFormula v) -- ^ Exclusive or.+ | RFLet Integer (RFormula v) (RFormula v) -- ^ Let /x/ = /a/ in /b/.+ deriving (Show)++-- | Translate a boolean formula to reduced form, or one of the+-- constants 'True' or 'False'. The integer argument is the current+-- nesting depth of let binders, and is used to number local bound+-- variables.+rformula :: Integer -> Formula v -> Either Bool (RFormula v)+rformula i (Var v) = Right (RFVar v)+rformula i Yes = Left True+rformula i No = Left False+rformula i (Not a) =+ case rformula i a of+ Left x -> Left (not x)+ Right a'' -> Right (RFNot a'')+rformula i (a :||: b) =+ case (rformula i a, rformula i b) of+ (Left True, b'') -> Left True+ (Left False, b'') -> b''+ (a'', Left True) -> Left True+ (a'', Left False) -> a''+ (Right a'', Right b'') -> Right (RFOr a'' b'')+rformula i (a :++: b) =+ case (rformula i a, rformula i b) of+ (Left x, Left y) -> Left (x /= y)+ (Left True, Right b'') -> Right (RFNot b'')+ (Left False, Right b'') -> Right b''+ (Right a'', Left True) -> Right (RFNot a'')+ (Right a'', Left False) -> Right a''+ (Right a'', Right b'') -> Right (RFXOr a'' b'')+rformula i (a :&&: b) = rformula i (Not (Not a :||: Not b))+rformula i (a :->: b) = rformula i (Not a :||: b)+rformula i (a :<->: b) = rformula i (Not a :++: b)+rformula i (All vs) = rformula i (all vs)+rformula i (Some vs) = rformula i (some vs)+rformula i (None vs) = rformula i (none vs)+rformula i (AtMostOne vs) = rformula i (atMostOne vs)+rformula i (ExactlyOne vs) = rformula i (exactlyOne vs)+rformula i (Let a f) =+ case rformula i a of+ Left True -> rformula i (f Yes)+ Left False -> rformula i (f No)+ Right a'' ->+ case rformula (i+1) (f (Bound i)) of+ Left x -> Left x+ Right b'' -> Right (RFLet i a'' b'')+rformula i (Bound x) = Right (RFBound x)++-- ----------------------------------------------------------------------+-- * De Morgan formulas++-- | Formulas in De Morgan standard form. We omit the constant formulas+-- 'True' and 'False', as they should only occur at the top level.+data DMFormula v =+ DMPos v -- ^ A positive literal.+ | DMNeg v -- ^ A negative literal.+ | DMPosBound Integer -- ^ A positive bound variable.+ | DMNegBound Integer -- ^ A negative bound variable.+ | DMAnd (DMFormula v) (DMFormula v) -- ^ Conjunction.+ | DMOr (DMFormula v) (DMFormula v) -- ^ Disjunction.+ | DMXOr (DMFormula v) (DMFormula v) -- ^ Exclusive or.+ | DMLet Integer (DMFormula v) (DMFormula v) -- ^ let /x/ = /a/ in /b/.+ +-- | Translate a reduced formula to De Morgan standard form.+demorgan :: RFormula v -> DMFormula v+demorgan (RFVar v) = DMPos v+demorgan (RFBound x) = DMPosBound x+demorgan (RFNot a) = demorgan_neg a+demorgan (RFOr a b) = DMOr (demorgan a) (demorgan b)+demorgan (RFXOr a b) = DMXOr (demorgan a) (demorgan b)+demorgan (RFLet x a b) = DMLet x (demorgan a) (demorgan b)++-- | Translate the negation of a reduced formula to De Morgan standard+-- form.+demorgan_neg :: RFormula v -> DMFormula v+demorgan_neg (RFVar v) = DMNeg v+demorgan_neg (RFBound x) = DMNegBound x+demorgan_neg (RFNot a) = demorgan a+demorgan_neg (RFOr a b) = DMAnd (demorgan_neg a) (demorgan_neg b)+demorgan_neg (RFXOr a b) = DMXOr (demorgan_neg a) (demorgan b)+demorgan_neg (RFLet x a b) = DMLet x (demorgan a) (demorgan_neg b)++-- ----------------------------------------------------------------------+-- * A monad for translation to CNF++-- | Literals over a set /v/, extended with countably many additional elements.+type ELit v = Lit (Either Integer v)++-- | A monad for translation to CNF. This monad keeps track of two kinds+-- of state: an integer counter to provide a supply of fresh+-- variables, and a list of definitional clauses.+data Trans v a = Trans (Integer -> (a, Integer, [[ELit v]]))++instance Monad (Trans v) where+ return a = Trans (\n -> (a, n, []))+ (Trans f) >>= g = Trans (\n ->+ let (a1, n1, l1) = f n in+ let Trans h = g a1 in+ let (a2, n2, l2) = h n1 in+ (a2, n2, l1 ++ l2))+ +instance Applicative (Trans v) where+ pure = return+ (<*>) = ap+ +instance Functor (Trans v) where+ fmap = liftM++-- | Run the 'Trans' monad.+runTrans :: Trans v a -> (a, [[ELit v]])+runTrans (Trans f) = (a, l)+ where+ (a, _, l) = f 0++-- | Return a fresh literal.+fresh_lit :: Trans v (ELit v)+fresh_lit = Trans (\n -> (Pos (Left n), n+1, []))++-- | Add some definitional clauses.+add_cnf :: [[ELit v]] -> Trans v ()+add_cnf cs = Trans (\n -> ((), n, cs))++-- ----------------------------------------------------------------------+-- * Translation from De Morgan to CNF++-- $ The simplest way to translate a formula, say+--+-- > (A ∧ B) ∨ (C ∧ (D ∨ E ∨ F)),+-- +-- is to introduce a new variable for each intermediate result, i.e.,+-- to give clauses+--+-- > X, X ↔ Y ∨ Z, Y ↔ A ∧ B, Z ↔ C ∧ W, W ↔ D ∨ V, V ↔ E ∨ F.+--+-- (Each equivalence \"↔\" can be translated into CNF+-- straightforwardly). Our translation is basically an optimized+-- version of this. The optimizations are: introduce additional+-- variables only when necessary; if the input formula is a CNF, leave+-- it unchanged. We give specialized translations of some formulas+-- depending on the context; for example, an exclusive or can be+-- translated in several different ways. For the above example, our+-- translation yields:+--+-- > Y ∨ Z, X ↔ A ∧ B, Z ↔ C ∧ W, W ↔ D ∨ E ∨ F.++-- | An environment is a mapping from local bound variables to+-- literals.+type Env v = Map Integer (ELit v)++-- | Translate a De Morgan formula to a SAT-equivalent CNF. Since this+-- requires the introduction of fresh variables, the CNF is over a+-- larger variable set, and we work in the 'Trans' monad. Moreover,+-- the translation depends on an environment.+trans_cnf :: Env v -> DMFormula v -> Trans v [[ELit v]]+trans_cnf env (DMPos v) = return [[Pos (Right v)]]+trans_cnf env (DMNeg v) = return [[Neg (Right v)]]+trans_cnf env (DMPosBound n) = return [[x]]+ where+ x = env Map.! n+trans_cnf env (DMNegBound n) = return [[neg x]]+ where+ x = env Map.! n+trans_cnf env (DMAnd a b) = do+ a' <- trans_cnf env a+ b' <- trans_cnf env b+ return (a' ++ b')+trans_cnf env (DMOr a b) = do+ a' <- trans_or env a+ b' <- trans_or env b+ return [a' ++ b']+trans_cnf env (DMXOr a b) = do+ x <- trans_lit env a+ y <- trans_lit env b+ return [[x, y], [neg x, neg y]]+trans_cnf env (DMLet n a b) = do+ do_let env n a b trans_cnf++-- | Translate a De Morgan formula to a disjunction of literals.+trans_or :: Env v -> DMFormula v -> Trans v [ELit v]+trans_or env (DMXOr a b) = do+ x <- trans_lit env (DMXOr a b)+ return [x]+trans_or env (DMLet n a b) = do+ do_let env n a b trans_or+trans_or env a = do+ c <- trans_cnf env a+ or_of_cnf c++-- | Translate a De Morgan formula to a single literal.+trans_lit :: Env v -> DMFormula v -> Trans v (ELit v)+trans_lit env (DMXOr a b) = do+ x <- trans_lit env a+ y <- trans_lit env b+ z <- lit_of_xor x y+ return z+trans_lit env (DMLet n a b) = do+ do_let env n a b trans_lit+trans_lit env a = do+ c <- trans_cnf env a+ lit_of_cnf c++-- | Polymorphically translate a 'DMLet' expression. The fifth+-- argument is usually one of 'trans_cnf', 'trans_or', or 'trans_lit',+-- and is used to translate the body of the \"let\".+do_let :: Env v -> Integer -> DMFormula v -> DMFormula v -> (Env v -> DMFormula v -> Trans v a) -> Trans v a+do_let env n a b cont = do+ x <- trans_lit env a+ let env' = Map.insert n x env+ cont env' b+ +-- | Convert a CNF to a disjunction of literals.+or_of_cnf :: [[ELit v]] -> Trans v [ELit v]+or_of_cnf [d] = return d+or_of_cnf ds = do+ x <- lit_of_cnf ds+ return [x]++-- | Convert a CNF to a single literal.+lit_of_cnf :: [[ELit v]] -> Trans v (ELit v)+lit_of_cnf ds = do+ xs <- sequence (map lit_of_or ds)+ y <- lit_of_and xs+ return y++-- | Convert a conjunction of literals to a single literal.+lit_of_and :: [ELit v] -> Trans v (ELit v)+lit_of_and [l] = return l+lit_of_and cs = do+ x <- fresh_lit+ -- Define x <-> c1 ∧ ... ∧ cn+ add_cnf [[neg x, c] | c <- cs ]+ add_cnf [[x] ++ [neg c | c <- cs]] + return x++-- | Convert a disjunction of literals to a single literal.+lit_of_or :: [ELit v] -> Trans v (ELit v)+lit_of_or [l] = return l+lit_of_or ds = do+ x <- fresh_lit+ -- Define x <-> d1 ∨ ... ∨ dn+ add_cnf [ [x, neg d] | d <- ds ]+ add_cnf [[neg x] ++ [d | d <- ds]]+ return x++-- | Convert an exclusive or of two literals to a single literal.+lit_of_xor :: ELit v -> ELit v -> Trans v (ELit v)+lit_of_xor x y = do+ z <- fresh_lit+ -- Define z <-> x ⊕ y+ add_cnf [[z, x, neg y]]+ add_cnf [[z, neg x, y]]+ add_cnf [[neg z, x, y]]+ add_cnf [[neg z, neg x, neg y]]+ return z++-- ----------------------------------------------------------------------+-- * Top-level functions++-- | Translate a De Morgan formula to a SAT-equivalent CNF.+cnf_of_dm :: DMFormula v -> [[ELit v]]+cnf_of_dm f = l ++ a+ where+ env = Map.empty+ (a, l) = runTrans (trans_cnf env f)++-- | Translate a boolean formula to a SAT-equivalent CNF.+cnf_of_formula :: Formula v -> [[ELit v]]+cnf_of_formula f =+ case rformula 0 f of+ Left True -> []+ Left False -> [[]]+ Right rf -> cnf_of_dm (demorgan rf) ++-- ----------------------------------------------------------------------+-- * SAT solver API for boolean formulas++-- | Check whether a boolean formula is satisfiable.+satisfiable :: (Ord v) => Formula v -> Bool+satisfiable a = isJust (solve a)++-- | Return a satisfying assignment for the boolean formula, if any.+solve :: (Ord v) => Formula v -> Maybe (Map v Bool)+solve a = listToMaybe (solve_all a)++-- | Lazily enumerate all satisfying assignments for the boolean formula.+solve_all :: (Ord v) => Formula v -> [Map v Bool]+solve_all a = res+ where+ a' = cnf_of_formula a+ res' = cnf_solve_all a'+ res = map restrict res'+ restrict ans = Map.fromList [ (v, b) | (Right v, b) <- Map.toList ans ]
+ SAT/MiniSat/Functional.hs view
@@ -0,0 +1,28 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | A functional (non-monadic) interface to the functions of+-- "SAT.MiniSat.Monadic". This layer:+--+-- * hides the existence of a solver object by providing a function+-- mapping SAT instances to a lazy list of solutions.++module SAT.MiniSat.Functional where++import SAT.MiniSat.Monadic+import SAT.MiniSat.Literals++-- | Input a CNF and output the a (lazily generated) list of+-- solutions. Variables are represented as integers, which should be+-- consecutive and start from 0.+m_solve :: [[Lit Int]] -> [[Maybe Bool]]+m_solve clauses = m_run $ do+ r <- m_solver_addclauses clauses+ if r == False then do+ return []+ else do+ m_solver_solve_start+ sols <- m_solver_next_solutions+ return sols
+ SAT/MiniSat/Literals.hs view
@@ -0,0 +1,25 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | This module provides a type of literals. ++module SAT.MiniSat.Literals where++-- | A literal is a positive or negative atom.+data Lit a = Pos a | Neg a+ deriving (Eq, Show)++-- | We order literals first by variable, then by sign, so that dual+-- literals are neighbors in the ordering.+instance (Ord a) => Ord (Lit a) where+ compare (Pos x) (Pos y) = compare x y+ compare (Neg x) (Neg y) = compare x y+ compare (Pos x) (Neg y) = compare (x,False) (y,True)+ compare (Neg x) (Pos y) = compare (x,True) (y,False)++-- | Negate a literal.+neg :: Lit a -> Lit a+neg (Pos a) = Neg a+neg (Neg a) = Pos a
+ SAT/MiniSat/LowLevel.hs view
@@ -0,0 +1,77 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++{-# LANGUAGE ForeignFunctionInterface #-}++-- | A low-level Haskell wrapper around the MiniSat-All library.++module SAT.MiniSat.LowLevel where++import Foreign+import Foreign.C.Types++-- ----------------------------------------------------------------------+-- * Some types++-- | An abstract type for the solver.+data C_Solver = C_Solver++-- | The marshalled \"int\" type from C.+type C_Int = Int32++-- | The marshalled \"lit\" type from the MiniSat library.+type C_Lit = C_Int++-- | The marshalled \"bool\" type from the MiniSat library.+type C_Bool = C_Int++-- | The marshalled \"lbool\" type from the MiniSat library.+type C_LBool = CChar++-- ----------------------------------------------------------------------+-- * Conversions++-- | Low-level wrapper around the C function /lit_new/.+foreign import ccall unsafe "solver.h lit_new"+ c_lit_new :: C_Int -> C_Bool -> C_Lit++-- ----------------------------------------------------------------------+-- * C API functions++-- | Low-level wrapper around the C function /solver_new/.+foreign import ccall unsafe "solver.h solver_new"+ c_solver_new :: IO (Ptr C_Solver)++-- | Low-level wrapper around the C function /solver_delete/.+foreign import ccall unsafe "solver.h solver_delete"+ c_solver_delete :: Ptr C_Solver -> IO ()++-- | Free a solver, callable by the garbage collector.+foreign import ccall unsafe "solver.h &solver_delete"+ c_solver_delete_ptr :: FinalizerPtr C_Solver++-- | Low-level wrapper around the C function /solver_addclause/.+foreign import ccall unsafe "solver.h solver_addclause"+ c_solver_addclause :: Ptr C_Solver -> Ptr C_Lit -> C_Int -> IO C_Bool++-- | Low-level wrapper around the C function /solver_solve_start/.+foreign import ccall unsafe "solver.h solver_solve_start"+ c_solver_solve_start :: Ptr C_Solver -> IO ()++-- | Low-level wrapper around the C function /solver_solve_next/.+foreign import ccall unsafe "solver.h solver_solve_next"+ c_solver_solve_next :: Ptr C_Solver -> IO C_Bool++-- | Low-level wrapper around the C function /solver_solve_finish/.+foreign import ccall unsafe "solver.h solver_solve_finish"+ c_solver_solve_finish :: Ptr C_Solver -> IO ()++-- | Low-level wrapper around the C function /solver_nvars/.+foreign import ccall unsafe "solver.h solver_nvars"+ c_solver_nvars :: Ptr C_Solver -> IO C_Int++-- | Low-level wrapper around the C function /solver_solution/.+foreign import ccall unsafe "solver.h solver_solution"+ c_solver_solution :: Ptr C_Solver -> IO (Ptr C_LBool)
+ SAT/MiniSat/Monadic.hs view
@@ -0,0 +1,199 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | A monadic interface to the functions of+-- "SAT.MiniSat.LowLevel". This layer:+--+-- * hooks into garbage collection;+--+-- * converts low-level types to Haskell types;+--+-- * replaces the 'IO' monad by a state monad;+-- +-- * converts low-level errors to I/O exceptions.+--+-- All of the exported functions may potentially raise an exception.++module SAT.MiniSat.Monadic where++import SAT.MiniSat.LowLevel+import SAT.MiniSat.Literals++import Foreign+import Foreign.C.Error+import Control.Monad.Trans.State+import System.IO.Unsafe++-- ----------------------------------------------------------------------+-- * Error handling++-- | Check an assertion, and raise an 'IO' exception (using the current+-- errno and the supplied location string) if the assertion fails.+ensure :: String -> Bool -> IO ()+ensure s True = return ()+ensure s False = throwErrno s++-- ----------------------------------------------------------------------+-- * Conversions++-- | Marshall a C boolean to a Haskell boolean.+bool_of_cbool :: C_Bool -> Bool+bool_of_cbool 0 = False+bool_of_cbool n = True++-- | Marshall a Haskell boolean to a C boolean.+cbool_of_bool :: Bool -> C_Bool+cbool_of_bool True = 1+cbool_of_bool False = 0++-- | Marshall a Haskell literal to a MiniSat literal.+clit_of_lit :: Lit Int -> C_Lit+clit_of_lit (Pos n) = c_lit_new (fromIntegral n) (cbool_of_bool False)+clit_of_lit (Neg n) = c_lit_new (fromIntegral n) (cbool_of_bool True)++-- | Marshall an \"lbool\" to a 'Maybe' 'Bool'.+maybebool_of_lbool :: C_LBool -> Maybe Bool+maybebool_of_lbool 0 = Nothing+maybebool_of_lbool 1 = Just True+maybebool_of_lbool (-1) = Just False+maybebool_of_lbool _ = error "maybebool_of_lbool"++-- ----------------------------------------------------------------------+-- * High-level Solver type++-- | The type of solvers.+newtype Solver = Solver (ForeignPtr C_Solver)++-- | Convert a low-level pointer to a garbage-collected 'Solver'.+make_Solver :: Ptr C_Solver -> IO Solver+make_Solver p = do+ fptr <- newForeignPtr c_solver_delete_ptr p+ return (Solver fptr)++-- | Marshall a 'Solver' to a 'Ptr' 'C_Solver'.+with_Solver :: Solver -> (Ptr C_Solver -> IO a) -> IO a+with_Solver (Solver fptr) = withForeignPtr fptr++-- | Create a new solver.+solver_new :: IO Solver+solver_new = do+ p <- c_solver_new+ ensure "solver_new" (p /= nullPtr)+ make_Solver p++-- ----------------------------------------------------------------------+-- * State monad++-- $ The low-level C functions live in the 'IO' monad. However, the only+-- actual side effect of these functions is to update the 'Solver'+-- object. Therefore, it is safe to lift these functions to a state+-- monad. Moreover, in doing so, we are able to exploit laziness in a+-- way that is not possible in the 'IO' monad.++-- | The 'SolverState' monad is for functions whose only side effect+-- is to update the 'Solver' object.+type SolverState a = State Solver a++-- | Marshall a function from the 'IO' monad to the state monad. The+-- call to 'unsafePerformIO' is safe, provided that the 'IO'+-- computation's only side effect is to update the 'Solver' object.+stateful :: (Solver -> IO a) -> SolverState a+stateful body = state $ \s -> unsafePerformIO $ do+ r <- body s+ return (r, s)++-- | Run a 'SolverState' computation in the context of a newly created+-- solver. The use of 'unsafePerformIO' is safe because the only side+-- effect of 'solver_new' is to create a new solver state.+m_run :: SolverState a -> a+m_run body = unsafePerformIO $ do+ s <- solver_new+ let (a, s') = runState body s+ return a++-- ----------------------------------------------------------------------+-- * Marshalled API functions++-- | Add a clause to the solver. May return 'False' if the clause is+-- unsatisfiable, in which case the Solver should not be searched.+-- The clause is represented as a list of literals.+m_solver_addclause :: [Lit Int] -> SolverState Bool+m_solver_addclause lits = stateful $ \s -> do+ with_Solver s $ \s_ptr -> do+ withArrayLen clits $ \n clits_ptr -> do+ r <- c_solver_addclause s_ptr clits_ptr (fromIntegral n)+ return (bool_of_cbool r)+ where+ clits = map clit_of_lit lits++-- | Initialize the solver for searching.+m_solver_solve_start :: SolverState ()+m_solver_solve_start = stateful $ \s -> do+ with_Solver s $ \s_ptr -> do+ c_solver_solve_start s_ptr++-- | Search the next solution.+m_solver_solve_next :: SolverState Bool+m_solver_solve_next = stateful $ \s -> do+ with_Solver s $ \s_ptr -> do+ r <- c_solver_solve_next s_ptr+ return (bool_of_cbool r)++-- | Finalizer to run after search.+m_solver_solve_finish :: SolverState ()+m_solver_solve_finish = stateful $ \s -> do+ with_Solver s $ \s_ptr -> do+ c_solver_solve_finish s_ptr++-- | Retrieve the most recent solution (only valid if+-- 'm_solver_solve_next' returned 'True', and no other API functions+-- have been called since then). The solution is represented as a+-- list, where the /n/th element of the list represents the assignment+-- ('True', 'False', or 'Nothing') of variable /n/.+m_solver_solution :: SolverState [Maybe Bool]+m_solver_solution = stateful $ \s -> do+ with_Solver s $ \s_ptr -> do+ lbools_ptr <- c_solver_solution s_ptr+ n <- c_solver_nvars s_ptr+ lbools <- peekArray (fromIntegral n) lbools_ptr+ let mbools = map maybebool_of_lbool lbools+ return mbools++-- ----------------------------------------------------------------------+-- * Derived API functions++-- | Add a list of clauses to the solver. May return 'False' if the+-- clauses are unsatisfiable, in which case the Solver should not be+-- searched.+m_solver_addclauses :: [[Lit Int]] -> SolverState Bool+m_solver_addclauses [] = return True+m_solver_addclauses (h:t) = do+ r <- m_solver_addclause h+ if r == False then do+ return False+ else do+ m_solver_addclauses t++-- | Search and return the next solution.+m_solver_next_solution :: SolverState (Maybe [Maybe Bool])+m_solver_next_solution = do+ r <- m_solver_solve_next+ if r == False then do+ return Nothing+ else do+ sol <- m_solver_solution+ return (Just sol)++-- | Return all remaining solutions.+m_solver_next_solutions :: SolverState [[Maybe Bool]]+m_solver_next_solutions = do+ r <- m_solver_next_solution+ case r of+ Nothing -> do+ return []+ Just h -> do+ t <- m_solver_next_solutions+ return (h:t)+
+ SAT/MiniSat/Variable.hs view
@@ -0,0 +1,78 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | A more convenient interface to the functionality of +-- "SAT.MiniSat.Functional". This layer:+--+-- * permits any ordered type to be used as the type of boolean+-- variables;+--+-- * represents solutions as a 'Map' from variables to booleans.++module SAT.MiniSat.Variable where++import SAT.MiniSat.Functional+import SAT.MiniSat.Literals++import qualified Data.Map as Map+import Data.Map (Map)+import qualified Data.Set as Set+import Data.Set (Set)+import Data.Maybe++-- ----------------------------------------------------------------------+-- * Auxiliary functions++-- | Extract the underlying variable of a literal.+var_of_lit :: Lit a -> a+var_of_lit (Pos v) = v+var_of_lit (Neg v) = v++-- | Map a variable function over literals.+lit_map :: (a -> b) -> Lit a -> Lit b+lit_map f (Pos x) = Pos (f x)+lit_map f (Neg x) = Neg (f x)++-- | Turn a list into a set and then back into a list. This sorts the+-- list and removes duplicates.+setify :: (Ord a) => [a] -> [a]+setify a = Set.toList (Set.fromList a)++-- ----------------------------------------------------------------------+-- * Primitive API function++-- | Compute the list of all solutions of a SAT instance.+--+-- A conjunctive normal form is represented as a list of clauses, each+-- of which is a list of literals.+--+-- A solution is represented as a (total or partial) truth assignment,+-- i.e., a map from variables to booleans.+cnf_solve_all :: (Ord v) => [[Lit v]] -> [Map v Bool]+cnf_solve_all cnf = results where+ vars = setify [ v | c <- cnf, l <- c, let v = var_of_lit l ]+ bij = zip vars [0..]+ int_of_var = (Map.!) (Map.fromList bij)+ var_of_int = (Map.!) (Map.fromList [ (n,v) | (v,n) <- bij ])+ m_cnf = map convert_clause cnf+ convert_clause c = setify [ lit_map int_of_var l | l <- c ]+ m_results = m_solve m_cnf+ results = map convert_result m_results+ convert_result l = r+ where+ r = Map.fromList [ (var_of_int n, b) | (n, Just b) <- zip [0..] l ]++-- ----------------------------------------------------------------------+-- * Derived API functions++-- | Check whether the SAT instance is satisfiable, and return a+-- satisfying assignment if there is one.+cnf_solve :: (Ord v) => [[Lit v]] -> Maybe (Map v Bool)+cnf_solve cnf = listToMaybe (cnf_solve_all cnf)++-- | Check whether the SAT instance is satisfiable.+cnf_satisfiable :: (Ord v) => [[Lit v]] -> Bool+cnf_satisfiable cnf = isJust (cnf_solve cnf)+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ c-sources/ChangeLog view
@@ -0,0 +1,70 @@+Cabal package minisat-solver 0.1 Released Oct. 24nd 2016+========================================+* Modified by Peter Selinger to export the solutions via API, rather than+ printing them to stdout.+* Modified by Peter Selinger for coding style and removed some dead code.++bc_minisat_all v1.1.0 Released Sep. 30th 2015+========================================+* Supported solution counting with GMP library.+* Supported interruption signal handling and deleted timelimit-related functionality instead.+* Changed names of some macros.+* Added functionality for continuing search by simulating the previous decisions after backtracking to the root level.++bc_minisat_all v1.0.0 Released Jul. 27th 2015+========================================+* Generalization is now renamed to simplification, and several bugs are fixed in the simplification part.+* Furthermore, the following change was made:+** The former part of simplification is implemented by traversing implication graph, which is more efficient than scanning the whole CNF.+** The latter part is organized and some bugs are corrected.+* Added functionality for setting timelimit and periodically reporting progress.+* Added functionality for including GNU MP bignum library so that a huge number of solutions can be precisely counted.+* Fixed the bug of not handling the case that blocking clases happen to be empty in solver_search().+* Deleted solver_generalize_naive() because it is useless.++minisat_all v2.0.1 Released Jun. 23rd 2015+========================================+* Added a license description (LICENSE.minisat_all).++minisat_all v2.0.0 Released April 30th 2015+========================================+* Fixed the bug of inserting a problem line by wrongly calling fseek in solver_solve().+** Problem line is no longer inserted.+* Improved a blocking clause computation according to the following paper:+** Y. Yu, P. Subramanyan, N. Tsiskaridze, S. Malik: "All-SAT using Minimal Blocking Clauses", in Proc. of the 27th International Conference on VLSI Design and the 13th International Conference on Embedded Systems, pp.86-91, 2014.++minisat_all v1.0.0 Released April 16th 2015+========================================+* This software computes the following problem , which is called ALLSAT.+ INPUT: a CNF (given in DIMACS CNF format) of a Boolean function f+ OUTPUT: all satisying assignments to the CNF.+* Installation+ Executing make in the top directory.+* Usage+ $ minisat_all in.dat (out.dat)+* If you just want to obtain a list of all satisfying assignments, specify output file as above.+ Then all assignments are written in DIMACS CNF format.+* This software is a common implementation of ALLSAT solver using SAT solver+* Two generalization methods of found solutions are implemented: see the two functions solver_generalize_faster and solver_generalize_naive in solver.c.+* They can be switched by defining macro in Makefile+* Also, another method without generalization is implemented, which is just to avoid rediscovery of found solutions.+* Contact+ Takahisa Toda <toda.takahisa(at)gmail.com>+ Graduate School of Information Systems, the University of Electro-Communications+ 1-5-1 Chofugaoka, Chofu, Tokyo 182-8585, Japan++MiniSat-C v1.14.1+========================================++* Fixed some serious bugs. +* Tweaked to be Visual Studio friendly (by Alan Mishchenko).+ This disabled reading of gzipped DIMACS files and signal handling, but none+ of these features are essential (and easy to re-enable, if wanted).++MiniSat-C v1.14+========================================++Ok, we get it. You hate C++. You hate templates. We agree; C++ is a+seriously messed up language. Although we are more pragmatic about the+quirks and maldesigns in C++, we sympathize with you. So here is a+pure C version of MiniSat, put together by Niklas Sörensson.
+ c-sources/LICENSE.MiniSat view
@@ -0,0 +1,20 @@+MiniSat -- Copyright (c) 2005, Niklas Sorensson++Permission is hereby granted, free of charge, to any person obtaining a+copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ c-sources/LICENSE.bc_minisat_all view
@@ -0,0 +1,4 @@+bc_minisat_all -- Copyright (c) 2015, Takahisa Toda++This software is developed by modifying MiniSat-C v1.14.1 and inherits the license of MiniSat-C v1.14.1.+Please confirm the copyright notice given in LICENSE.MiniSat.
+ c-sources/Makefile view
@@ -0,0 +1,116 @@+##+## Makefile for Standard, Profile, Debug, and Release version of MiniSat+##++CSRCS = $(wildcard *.c)+CHDRS = $(wildcard *.h)+COBJS = $(addsuffix .o, $(basename $(CSRCS)))++PCOBJS = $(addsuffix p, $(COBJS))+DCOBJS = $(addsuffix d, $(COBJS))+RCOBJS = $(addsuffix r, $(COBJS))++EXEC = bc_minisat_all++CC = gcc+CFLAGS = -std=c99 -fPIC+COPTIMIZE = -O3 -fomit-frame-pointer+++.PHONY : s p d r build clean depend lib libd++all: r++s: WAY=standard+p: WAY=profile+d: WAY=debug+r: WAY=release+rs: WAY=release static++# The solver can not count a huge number of solutions beyond a cerntain threshold.+# To count precisely, install the GNU MP bignum library and uncomment the following GMPFLAGS and define GMP in MYFLAGS.+GMPFLAGS =+#GMPFLAGS += -lgmp++MYFLAGS = +#MYFLAGS += -D SIMPLIFY # Simplification of satisyfying assignments+#MYFLAGS += -D NONDISJOINT # Nondisjoint partial satisfying assignments+#MYFLAGS += -D FIXEDORDER # Variable selection ordering is fixed+MYFLAGS += -D CONTINUE # Continue search at the point where a solution is found.+#MYFLAGS += -D GMP # GNU MP bignum library is used++s: CFLAGS+=$(COPTIMIZE) -ggdb -D NDEBUG $(MYFLAGS) -D VERBOSEDEBUG+p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG $(MYFLAGS)+d: CFLAGS+=-O0 -ggdb -D DEBUG $(MYFLAGS)+r: CFLAGS+=$(COPTIMIZE) -D NDEBUG $(MYFLAGS)+rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG $(MYFLAGS)++s: build $(EXEC)+p: build $(EXEC)_profile+d: build $(EXEC)_debug+r: build $(EXEC)_release+rs: build $(EXEC)_static++build:+ @echo Building $(EXEC) "("$(WAY)")"++clean:+ @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \+ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) depend.mak++## Build rule+%.o %.op %.od %.or: %.c+ @echo Compiling: $<+ @$(CC) $(CFLAGS) -c -o $@ $<++## Linking rules (standard/profile/debug/release)+$(EXEC): $(COBJS)+ @echo Linking $(EXEC)+ @$(CC) $(COBJS) $(GMPFLAGS) -lz -lm -ggdb -Wall -o $@ ++$(EXEC)_profile: $(PCOBJS)+ @echo Linking $@+ @$(CC) $(PCOBJS) $(GMPFLAGS) -lz -lm -ggdb -Wall -pg -o $@++$(EXEC)_debug: $(DCOBJS)+ @echo Linking $@+ @$(CC) $(DCOBJS) $(GMPFLAGS) -lz -lm -ggdb -Wall -o $@++$(EXEC)_release: $(RCOBJS)+ @echo Linking $@+ @$(CC) $(RCOBJS) $(GMPFLAGS) -lz -lm -Wall -o $@++$(EXEC)_static: $(RCOBJS)+ @echo Linking $@+ @$(CC) --static $(RCOBJS) $(GMPFLAGS) -lz -lm -Wall -o $@++lib: libbc_minisat_all.a+libd: libbc_minisatd_all.a++libbc_minisat_all.a: solver.or csolver.or+ @echo Library: "$@ ( $^ )"+ @rm -f $@+ @ar cq $@ $^++libbc_minisatd_all.a: solver.od csolver.od+ @echo Library: "$@ ( $^ )"+ @rm -f $@+ @ar cq $@ $^+++## Make dependencies+depend: depend.mak+depend.mak: $(CSRCS) $(CHDRS)+ @echo Making dependencies ...+ @$(CC) -MM $(CSRCS) > depend.mak+ @cp depend.mak /tmp/depend.mak.tmp+ @sed "s/o:/op:/" /tmp/depend.mak.tmp >> depend.mak+ @sed "s/o:/od:/" /tmp/depend.mak.tmp >> depend.mak+ @sed "s/o:/or:/" /tmp/depend.mak.tmp >> depend.mak+ @rm /tmp/depend.mak.tmp++include depend.mak++## Coding style+indent:+ indent -kr -i2 -ncs -brf -l1000 -T FILE -T solver -T lit -T bool -T lbool -T uint64 -T stats -T clause -T veci -T vecp *.c *.h
+ c-sources/README.html view
@@ -0,0 +1,202 @@+<?xml version="1.0" encoding="UTF-8"?>+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">+<html xmlns="http://www.w3.org/1999/xhtml">+ <head>+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />+ <title>BC_MINISAT_ALL: A Blocking AllSAT Solver</title>+ <link rel="stylesheet" href="http://www.sd.is.uec.ac.jp/toda/css/default.css" type="text/css" />+ <meta name="generator" content="DocBook XSL-NS Stylesheets V1.75.2" />+ </head>+ <body>+ <div xml:lang="en" class="article" title="BC_MINISAT_ALL: A Blocking AllSAT Solver" lang="en">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title"><a id="idp192"></a>BC_MINISAT_ALL: A Blocking AllSAT Solver</h2>+ </div>+ <div>+ <div class="author">+ <h3 class="author">+ <span class="firstname">Takahisa</span>+ <span class="surname">Toda</span>+ </h3>+ <div class="affiliation">+ <div class="address">+ <p><br />+ <code class="email"><<a class="email" href="mailto:toda.takahisa(at)gmail.com">toda.takahisa(at)gmail.com</a>></code><br />+ </p>+ </div>+ </div>+ </div>+ </div>+ <div>+<p><a href="http://www.sd.is.uec.ac.jp/toda/index.html" style="float:right;">Back to Top Page.</a></p> <p class="pubdate">+ Last update: 2015-9-30+ </p>+ </div>+ </div>+ <hr />+ </div>+ <div class="sect1" title="1. Description">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="definition"></a>1. Description</h2>+ </div>+ </div>+ </div>+ <p>+ A blocking clause-based AllSAT solver (a blocking solver for short), implemented on top of MiniSat-C v1.14.1, is presented.+ </p>+ </div>+ <div class="sect1" title="2. DOWNLOAD">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="download"></a>2. DOWNLOAD</h2>+ </div>+ </div>+ </div>+ <div class="itemizedlist">+ <ul class="itemizedlist" type="disc">+ <li class="listitem">+ Latest version: <a class="ulink" href="bc_minisat_all-1.1.0.tar.gz" target="_top">bc_minisat_all version 1.1.0</a>, released on 30th Sep., 2015.+ </li>+ <li class="listitem">+ Old versions: <a class="ulink" href="bc_minisat_all-1.0.0.tar.gz" target="_top">bc_minisat_all version 1.0.0</a>, <a class="ulink" href="minisat_all-2.0.1.tar.gz" target="_top">v.2.0.1</a>, <a class="ulink" href="minisat_all-2.0.0.tar.gz" target="_top">v.2.0.0</a>, <a class="ulink" href="minisat_all-1.0.0.tar.gz" target="_top">v.1.0.0</a>.+ </li>+ </ul>+ </div>+ </div>+ <div class="sect1" title="3. FILE FORMAT">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="format"></a>3. FILE FORMAT</h2>+ </div>+ </div>+ </div>+ <p>+ Input boolean formula should be in DIMACS CNF format.+ For details of DIMACS CNF format and benchmark problems, see <a class="ulink" href="http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html" target="_top">SATLIB</a>.+ </p>+ </div>+ <div class="sect1" title="4. HOW TO COMPILE">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="compile"></a>4. HOW TO COMPILE</h2>+ </div>+ </div>+ </div>+ <p>If no option is given, standard mode is selected.</p>+ <pre class="screen">++$ tar zxvf bc_minisat_all-1.0.0.tar.gz+$ cd bc_minisat_all-1.0.0+$ make [options] +list of options+s standard: debug information used by debugger is generated at compilation time, and detailed solver status is reported at runtime.+p profile: in addition to standard setting, profile information used by gprof is generated at compilation time and several tests are performed at runtime.+d debug: in addition to standard setting, several tests are performed at runtime and no optimization is applied.+r release: release version, compiled with dynamic link+rs static: release version, compiled with static link+clean executable files, object files, etc are removed.++ </pre>+ </div>+ <div class="sect1" title="5. MACRO"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="macro"></a>5. MACRO</h2></div></div></div>+ + Program behavior can be controlled by defining or not defining the following macros in <code class="filename">Makefile</code>.+ <div class="itemizedlist"><ul class="itemizedlist" type="disc"><li class="listitem">+ SIMPLIFY: Simplification of assignments is enabled. If this is not defined, simplification is not performed, and blocking clauses consisting of decision literals are used instead.+ </li><li class="listitem">+ NONDISJOINT: Nondisjoint partial assignments are computed (see Yu et al. 2014). If this is not defined, computed partial assignments are pairwise disjoint: in other words, different partial assignments do not share common total assignments. This macro makes sense only when SIMPLIFICATION is defined too.+ </li><li class="listitem">+ CONTINUE: Search is continued at the point where a solutions is found. If this is not defined, solver starts from scratch.+ </li><li class="listitem">+ FIXEDORDER: Variable selection heuristic is disabled and variables are selected in increasing order of variable indices. If this is not defined, variable selection heuristic is used. This functionality is added to evaluate efficiency of variable selection heuristics.+ </li><li class="listitem">+ GMP: GNU MP bignum library is used to count solutions.+ </li></ul></div>+ </div>+ <div class="sect1" title="6. USAGE">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="usage"></a>6. USAGE</h2>+ </div>+ </div>+ </div>+ <p>+ If an output file is specified, all satisfying assignments to a CNF are generated in DIMACS CNF format without problem line. + <span class="emphasis"><em>Notice: there may be as many number of assignments as can not be stored in a disk space.</em></span>+ If simplification is performed, computed assingments are partial, which means some variables may not appear.+ </p>+ <pre class="screen">++Usage: ./bc_minisat_all [options] input-file [output-file]++ </pre>+ <p>+ </p>+ </div>+ <div class="sect1" title="7. LICENSE">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="license"></a>7. LICENSE</h2>+ </div>+ </div>+ </div>+ <p>bc_minisat_all is implemented by modifying MiniSat-C_v1.14.1. Please confirm the license file included in this software.</p>+ </div>+ <div class="sect1" title="8. NOTICE">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="notice"></a>8. NOTICE</h2>+ </div>+ </div>+ </div>+ <p>+ A huge number of assignments may be generated and <span class="emphasis"><em>disk space may be exhausted</em></span>. To avoid disk overflow, take measure such as using <span class="command"><strong>ulimit</strong></span> command.+ </p>+ </div>+ <div class="sect1" title="9. REFERENCES">+ <div class="titlepage">+ <div>+ <div>+ <h2 class="title" style="clear: both"><a id="references"></a>9. REFERENCES</h2>+ </div>+ </div>+ </div>+ <div class="itemizedlist">+ <ul class="itemizedlist" type="disc">+ <li class="listitem">+ N. Eén, N. Sörensson : <a class="ulink" href="http://minisat.se/" target="_top">MiniSat Page</a>: MiniSat-C_v1.14.1, accessed on 15 Dec. 2014.+ </li>+ <li class="listitem">+ N. Eén, N. Sörensson : <a class="ulink" href="http://dx.doi.org/10.1007/978-3-540-24605-3_37" target="_top">An Extensible SAT-solver</a>, In Proceedings of the 6th international conference of Theory and Applications of Satisfiability Testing, pages 502--518, 2004.+ </li>+ <li class="listitem">+Morgado, A. and Marques-Silva, J.: <a class="ulink" href="http://dx.doi.org/10.1109/ICTAI.2005.69" target="_top">Good learning and implicit model enumeration</a>, In Proceedings of 17th IEEE International Conference on Tools with Artificial Intelligence, 2005. ICTAI 05.+ </li>+ <li class="listitem">+Yinlei Yu and Subramanyan, P. and Tsiskaridze, N. and Malik, S.: <a class="ulink" href="http://dx.doi.org/10.1109/VLSID.2014.22" target="_top">All-SAT Using Minimal Blocking Clauses</a>, In Proceedings of 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems, 2014, pp.86-91.+ </li>+ <li class="listitem">+McMillan, KenL.: <a class="ulink" href="http://dx.doi.org/10.1007/3-540-45657-0_19" target="_top">Applying SAT Methods in Unbounded Symbolic Model Checking</a>, Computer Aided Verification, LNCS Vol.2404, pp.250-264. 2002.+ </li>+ <li class="listitem">+Jin, HoonSang and Han, HyoJung and Somenzi, Fabio: <a class="ulink" href="http://dx.doi.org/10.1007/978-3-540-31980-1_19" target="_top">Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit</a>, Tools and Algorithms for the Construction and Analysis of Systems, LNCS Vol.3440, pp.287-300, 2005.+ </li>+ <li class="listitem">+Weinan Zhao and Weimin Wu: <a class="ulink" href="http://dx.doi.org/10.1109/CADCG.2009.5246850" target="_top">ASIG: An all-solution SAT solver for CNF formulas</a>, In Proceedings of 11th IEEE International Conference on Computer-Aided Design and Computer Graphics, 2009. CAD/Graphics '09, pp. 508-513, 2009.+ </li>+ </ul>+ </div>+ </div>+ </div>+ </body>+</html>
+ c-sources/README.pdf view
binary file changed (absent → 14916 bytes)
+ c-sources/main.c view
@@ -0,0 +1,345 @@+/* **********************************************************************+MiniSat -- Copyright (c) 2005, Niklas Sorensson+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+********************************************************************** */+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko++#include "solver.h"++#include <stdio.h>+#include <stdlib.h>+#include <time.h>+#include <limits.h>+#include <signal.h>++#ifdef GMP+#include <gmp.h>+#endif++// ======================================================================+// Helpers:++// Reads an input stream to end-of-file and returns the result as a+// 'char*' terminated by '\0' (dynamic allocation in case 'in' is+// standard input).+char *readFile(FILE *in) {+ char *data = malloc(65536);+ int cap = 65536;+ int size = 0;++ while (!feof(in)) {+ if (size == cap) {+ cap *= 2;+ data = realloc(data, cap);+ }+ size += fread(&data[size], 1, 65536, in);+ }+ data = realloc(data, size + 1);+ data[size] = '\0';++ return data;+}++// static inline double cpuTime(void) {+// struct rusage ru;+// getrusage(RUSAGE_SELF, &ru);+// return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;+// }++// ======================================================================+// DIMACS Parser:++static inline void skipWhitespace(char **in) {+ while ((**in >= 9 && **in <= 13) || **in == 32) {+ (*in)++;+ }+}++static inline void skipLine(char **in) {+ for (;;) {+ if (**in == 0) {+ return;+ }+ if (**in == '\n') {+ (*in)++;+ return;+ }+ (*in)++;+ }+}++static inline int parseInt(char **in) {+ int val = 0;+ int _neg = 0;++ skipWhitespace(in);+ if (**in == '-') {+ _neg = 1;+ (*in)++;+ } else if (**in == '+') {+ (*in)++;+ }+ if (**in < '0' || **in > '9') {+ fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **in);+ exit(1);+ }+ while (**in >= '0' && **in <= '9') {+ val = val * 10 + (**in - '0');+ (*in)++;+ }+ return _neg ? -val : val;+}++static void readClause(char **in, solver *s, veci *lits) {+ int parsed_lit, var;++ veci_resize(lits, 0);+ for (;;) {+ parsed_lit = parseInt(in);+ if (parsed_lit == 0) {+ break;+ }+ var = abs(parsed_lit) - 1;+ veci_push(lits, (parsed_lit > 0 ? toLit(var) : lit_neg(toLit(var))));+ }+}++static lbool parse_DIMACS_main(char *in, solver *s) {+ veci lits;+ veci_new(&lits);++ for (;;) {+ skipWhitespace(&in);+ if (*in == 0) {+ break;+ } else if (*in == 'c' || *in == 'p') {+ skipLine(&in);+ } else {+ lit *begin;++ readClause(&in, s, &lits);+ begin = veci_begin(&lits);+ if (!solver_addclause(s, begin, veci_size(&lits))) {+ veci_delete(&lits);+ return l_False;+ }+ }+ }+ veci_delete(&lits);+ return solver_simplify(s); // note: this casts a bool to lbool,+ // probably a bug.+}++// Inserts problem into solver. Returns FALSE upon immediate conflict.+static lbool parse_DIMACS(FILE *in, solver *s) {+ char *text = readFile(in);+ lbool ret = parse_DIMACS_main(text, s);++ free(text);+ return ret;+}++// ======================================================================++void printStats(stats *stats, int cpu_time, bool interrupted) {+ double Time = (float)(cpu_time) / (float)(CLOCKS_PER_SEC);++ printf("restarts : %12llu\n", stats->starts);+ printf("conflicts : %12.0f (%9.0f / sec )\n", (double)stats->conflicts, (double)stats->conflicts / Time);+ printf("decisions : %12.0f (%9.0f / sec )\n", (double)stats->decisions, (double)stats->decisions / Time);+ printf("propagations : %12.0f (%9.0f / sec )\n", (double)stats->propagations, (double)stats->propagations / Time);+ printf("inspects : %12.0f (%9.0f / sec )\n", (double)stats->inspects, (double)stats->inspects / Time);+ printf("conflict literals : %12.0f (%9.2f %% deleted )\n", (double)stats->tot_literals, (double)(stats->max_literals - stats->tot_literals)*100.0 / (double)stats->max_literals);+ printf("CPU time : %12.2f sec\t", Time);+ printf("\n");++#ifdef NONDISJOINT+ printf("disjoint : disabled\n");+#else+ printf("disjoint : enabled\n");+#endif++#ifdef FIXEDORDER+ printf("variable ordering : fixed\n");+#else+ printf("variable ordering : heuristic\n");+#endif++#ifdef CONTINUE+ printf("continuation : enabled\n");+#else+ printf("continuation : disabled\n");+#endif++#ifdef GMP+ printf("gmp : enabled\n");+#ifdef SIMPLIFY+ printf("simplification : enabled\n");+ printf("SAT (partial) : ");+ mpz_out_str(stdout, 10, stats->par_solutions);+ if (interrupted) {+ printf("+");+ }+ printf("\n");++#ifndef NONDISJOINT+ printf("SAT (full) : ");+ mpz_out_str(stdout, 10, stats->tot_solutions);+ if (interrupted) {+ printf("+");+ }+ printf("\n");+#endif++#else /* NO SIMPLIFY */+ printf("simplification : disabled\n");+ printf("SAT (full) : ");+ mpz_out_str(stdout, 10, stats->tot_solutions);+ if (interrupted) {+ printf("+");+ }+ printf("\n");+#endif++#else // if GMP not defined+ printf("gmp : disabled\n");+#ifdef SIMPLIFY+ printf("simplification : enabled\n");+ printf("SAT (partial) : %12llu", stats->par_solutions); // partial assignments which cover the whole solution space.+ if (stats->par_solutions == ULONG_MAX || interrupted) {+ printf("+"); // overflow or interrupted+ }+ printf("\n");++#ifndef NONDISJOINT+ printf("SAT (full) : %12llu", stats->tot_solutions);+ if (stats->tot_solutions == ULONG_MAX || interrupted) {+ printf("+"); // overflow or interrupted+ }+ printf("\n");+#endif++#else /*NO SIMPLIFY */+ printf("simplification : disabled\n");+ printf("SAT (full) : %12llu", stats->tot_solutions);+ if (stats->tot_solutions == ULONG_MAX || interrupted) {+ printf("+"); // overflow or interrupted+ }+ printf("\n");+#endif+#endif // GMP+}++solver *slv;++static void SIGINT_handler(int signum) {+ printf("\n");+ printf("*** INTERRUPTED ***\n");+ printStats(&slv->stats, clock() - slv->stats.clk, true);+ printf("\n");+ printf("*** INTERRUPTED ***\n");+ exit(0);+}++// ======================================================================++static inline void PRINT_USAGE(char *p) {+ fprintf(stderr, "Usage:\t%s [options] input-file [output-file]\n", (p));+}+++int main(int argc, char **argv) {+ solver *s = solver_new();+ lbool st;+ FILE *in;+ FILE *out;+ s->stats.clk = clock();++ char *infile = NULL;+ char *outfile = NULL;++ /* Receive inputs */+ for (int i = 1; i < argc; i++) {+ if (argv[i][0] == '-') {+ switch (argv[i][1]) {+ case '?':+ case 'h':+ default:+ PRINT_USAGE(argv[0]);+ return 0;+ }+ } else {+ if (infile == NULL) {+ infile = argv[i];+ } else if (outfile == NULL) {+ outfile = argv[i];+ } else {+ PRINT_USAGE(argv[0]);+ return 0;+ }+ }+ }+ if (infile == NULL) {+ PRINT_USAGE(argv[0]);+ return 0;+ }++ in = fopen(infile, "rb");+ if (in == NULL) {+ fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : infile);+ exit(1);+ }+ if (outfile != NULL) {+ out = fopen(outfile, "wb");+ if (out == NULL) {+ fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : outfile);+ exit(1);+ } else {+ s->out = out;+ }+ } else {+ out = NULL;+ }++ st = parse_DIMACS(in, s);+ fclose(in);++ if (st == l_False) {+ solver_delete(s);+ printf("Trivial problem\nUNSATISFIABLE\n");+ exit(20);+ }+ s->verbosity = 1;+ slv = s;+ if (signal(SIGINT, SIGINT_handler) == SIG_ERR) {+ fprintf(stderr, "ERROR! Cound not set signal");+ exit(1);+ }++ solver_solve(s);++ printf("input : %s\n", infile);+ printStats(&s->stats, clock() - s->stats.clk, false);++ solver_delete(s);+ return 0;+}
+ c-sources/solver.c view
@@ -0,0 +1,1587 @@+/* **********************************************************************+MiniSat -- Copyright (c) 2005, Niklas Sorensson+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+********************************************************************** */+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko++#include <stdio.h>+#include <assert.h>+#include <math.h>+#include <stdint.h>+#include <limits.h>+#include <string.h>++#include "solver.h"++static inline void solver_inc_totsol(solver *s) {+#ifdef GMP+ mpz_add_ui(s->stats.tot_solutions, s->stats.tot_solutions, 1);+#else+ if (s->stats.tot_solutions < ULONG_MAX) {+ s->stats.tot_solutions++;+ }+#endif+}+++static inline void solver_inc_parsol(solver *s) {+#ifdef GMP+ mpz_add_ui(s->stats.par_solutions, s->stats.par_solutions, 1);+#else+ if (s->stats.par_solutions < ULONG_MAX) {+ s->stats.par_solutions++;+ }+#endif+}++// ======================================================================+// Debug:++//#define VERBOSEDEBUG++// For derivation output (verbosity level 2)+#define L_IND "%-*d"+#define L_ind solver_dlevel(s) * 3 + 3, solver_dlevel(s)+#define L_LIT "%sx%d"+#define L_lit(p) lit_sign(p) ? "~" : "", (lit_var(p))++// Just like 'assert()' but expression will be evaluated in the+// release version as well.+static inline void check(int expr) {+ assert(expr);+}++static void printlits(lit *begin, lit *end) {+ int i;+ for (i = 0; i < end - begin; i++) {+ printf(L_LIT " ", L_lit(begin[i]));+ }+}++// ======================================================================+// Random numbers:+++// Returns a random float 0 <= x < 1. Seed must never be 0.+static inline double drand(double *seed) {+ int q;+ *seed *= 1389796;+ q = (int)(*seed / 2147483647);+ *seed -= (double)q *2147483647;+ return *seed / 2147483647;+}+++// Returns a random integer 0 <= x < size. Seed must never be 0.+static inline int irand(double *seed, int size) {+ return (int)(drand(seed) * size);+}+++// ======================================================================+// Predeclarations:++void sort(void **array, int size, int (*comp) (const void *, const void *));++// ======================================================================+// Literals++lit lit_new(int v, bool sign) {+ if (sign) {+ return lit_neg(toLit(v));+ } else {+ return toLit(v);+ }+}++// ======================================================================+// Clause datatype + minor functions:++struct clause_t {+ int size_learnt;+ lit lits[0];+};++static inline int clause_size(clause *c) {+ return c->size_learnt >> 1;+}++static inline lit *clause_begin(clause *c) {+ return c->lits;+}++static inline int clause_learnt(clause *c) {+ return c->size_learnt & 1;+}++static inline float clause_activity(clause *c) {+ return *((float *)&c->lits[c->size_learnt >> 1]);+}++static inline void clause_setactivity(clause *c, float a) {+ *((float *)&c->lits[c->size_learnt >> 1]) = a;+}++// ======================================================================+// Encode literals in clause pointers:++clause *clause_from_lit(lit l) {+ return (clause *)((unsigned long)l + (unsigned long)l + 1);+}++bool clause_is_lit(clause *c) {+ return ((unsigned long)c & 1);+}++lit clause_read_lit(clause *c) {+ return (lit)((unsigned long)c >> 1);+}++// ======================================================================+// Simple helpers:++static inline int solver_dlevel(solver *s) {+ return veci_size(&s->trail_lim);+}++static inline vecp *solver_read_wlist(solver *s, lit l) {+ return &s->wlists[l];+}++static inline void vecp_remove(vecp *v, void *e) {+ void **ws = vecp_begin(v);+ int j = 0;++ for (; ws[j] != e; j++) {+ /* empty */+ }+ assert(j < vecp_size(v));+ for (; j < vecp_size(v) - 1; j++) {+ ws[j] = ws[j + 1];+ }+ vecp_resize(v, vecp_size(v) - 1);+}++static inline lit solver_assumedlit(solver *s, int level) {+ return s->trail[veci_begin(&s->trail_lim)[level - 1]];+}++static inline int solver_isimplied(solver *s, int x) {+ return s->levels[x] <= s->root_level || x != lit_var(solver_assumedlit(s, s->levels[x]));+}++// ======================================================================+// Variable order functions:++static inline void order_update(solver *s, int v) // updateorder+{+ int *orderpos = s->orderpos;+ double *activity = s->activity;+ int *heap = veci_begin(&s->order);+ int i = orderpos[v];+ int x = heap[i];+ int parent = (i - 1) / 2;++ assert(s->orderpos[v] != -1);++ while (i != 0 && activity[x] > activity[heap[parent]]) {+ heap[i] = heap[parent];+ orderpos[heap[i]] = i;+ i = parent;+ parent = (i - 1) / 2;+ }+ heap[i] = x;+ orderpos[x] = i;+}++static inline void order_assigned(solver *s, int v) {+ /* empty */+}++static inline void order_unassigned(solver *s, int v) { // undoorder+ int *orderpos = s->orderpos;++ if (orderpos[v] == -1) {+ orderpos[v] = veci_size(&s->order);+ veci_push(&s->order, v);+ order_update(s, v);+ }+}++static int order_select(solver *s, float random_var_freq) { // selectvar+ int *heap;+ double *activity;+ int *orderpos;++ lbool *values = s->assigns;++ // Random decision:+ if (drand(&s->random_seed) < random_var_freq) {+ int next = irand(&s->random_seed, s->size);+ assert(next >= 0 && next < s->size);+ if (values[next] == l_Undef) {+ return next;+ }+ }+ // Activity based decision:++ heap = veci_begin(&s->order);+ activity = s->activity;+ orderpos = s->orderpos;++ while (veci_size(&s->order) > 0) {+ int next = heap[0];+ int size = veci_size(&s->order) - 1;+ int x = heap[size];++ veci_resize(&s->order, size);++ orderpos[next] = -1;++ if (size > 0) {+ double act = activity[x];++ int i = 0;+ int child = 1;++ while (child < size) {+ if (child + 1 < size && activity[heap[child]] < activity[heap[child + 1]]) {+ child++;+ }+ assert(child < size);++ if (act >= activity[heap[child]]) {+ break;+ }+ heap[i] = heap[child];+ orderpos[heap[i]] = i;+ i = child;+ child = 2 * child + 1;+ }+ heap[i] = x;+ orderpos[heap[i]] = i;+ }++ if (values[next] == l_Undef) {+ return next;+ }+ }++ return var_Undef;+}++// ======================================================================+// Activity functions:++static inline void act_var_rescale(solver *s) {+ double *activity = s->activity;+ int i;++ for (i = 0; i < s->size; i++) {+ activity[i] *= 1e-100;+ }+ s->var_inc *= 1e-100;+}++static inline void act_var_bump(solver *s, int v) {+ double *activity = s->activity;++ if ((activity[v] += s->var_inc) > 1e100) {+ act_var_rescale(s);+ }+ //printf("bump %d %f\n", v-1, activity[v]);++ if (s->orderpos[v] != -1) {+ order_update(s, v);+ }+}++static inline void act_var_decay(solver *s) {+ s->var_inc *= s->var_decay;+}++static inline void act_clause_rescale(solver *s) {+ clause **cs = (clause **)vecp_begin(&s->learnts);+ int i;++ for (i = 0; i < vecp_size(&s->learnts); i++) {+ float a = clause_activity(cs[i]);+ clause_setactivity(cs[i], a * (float)1e-20);+ }+ s->cla_inc *= (float)1e-20;+}+++static inline void act_clause_bump(solver *s, clause *c) {+ float a = clause_activity(c) + s->cla_inc;++ clause_setactivity(c, a);+ if (a > 1e20) {+ act_clause_rescale(s);+ }+}++static inline void act_clause_decay(solver *s) {+ s->cla_inc *= s->cla_decay;+}+++// ======================================================================+// Clause functions:++/* pre: size > 1 && no variable occurs twice */+static clause *clause_new(solver *s, lit *begin, lit *end, int learnt) {+ int size;+ clause *c;+ int i;++ assert(end - begin > 1);+ assert(learnt >= 0 && learnt < 2);+ size = end - begin;+ c = (clause *)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));+ c->size_learnt = (size << 1) | learnt;++ for (i = 0; i < size; i++) {+ c->lits[i] = begin[i];+ }++ if (learnt) {+ *((float *)&c->lits[size]) = 0.0;+ }++ assert(begin[0] >= 0);+ assert(begin[0] < s->size * 2);+ assert(begin[1] >= 0);+ assert(begin[1] < s->size * 2);++ assert(lit_neg(begin[0]) < s->size * 2);+ assert(lit_neg(begin[1]) < s->size * 2);++ //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c);+ //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c);++ vecp_push(solver_read_wlist(s, lit_neg(begin[0])), (void *)(size > 2 ? c : clause_from_lit(begin[1])));+ vecp_push(solver_read_wlist(s, lit_neg(begin[1])), (void *)(size > 2 ? c : clause_from_lit(begin[0])));++ return c;+}+++static void clause_remove(solver *s, clause *c) {+ lit *lits = clause_begin(c);++ assert(lit_neg(lits[0]) < s->size * 2);+ assert(lit_neg(lits[1]) < s->size * 2);++ //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c);+ //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c);++ assert(lits[0] < s->size * 2);+ vecp_remove(solver_read_wlist(s, lit_neg(lits[0])), (void *)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));+ vecp_remove(solver_read_wlist(s, lit_neg(lits[1])), (void *)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));++ if (clause_learnt(c)) {+ s->stats.learnts--;+ s->stats.learnts_literals -= clause_size(c);+ } else {+ s->stats.clauses--;+ s->stats.clauses_literals -= clause_size(c);+ }++ free(c);+}+++static lbool clause_simplify(solver *s, clause *c) {+ lit *lits = clause_begin(c);+ lbool *values = s->assigns;+ int i;++ assert(solver_dlevel(s) == 0);++ for (i = 0; i < clause_size(c); i++) {+ lbool sig = !lit_sign(lits[i]);+ sig += sig - 1;+ if (values[lit_var(lits[i])] == sig) {+ return l_True;+ }+ }+ return l_False;+}++// ======================================================================+// Minor (solver) functions:++void solver_setnvars(solver *s, int n) {+ int var;++ if (s->cap < n) {++ while (s->cap < n) {+ s->cap = s->cap * 2 + 1;+ }+ s->wlists = (vecp *)realloc(s->wlists, sizeof(vecp) * s->cap * 2);+ s->activity = (double *)realloc(s->activity, sizeof(double) * s->cap);+ s->assigns = (lbool *)realloc(s->assigns, sizeof(lbool) * s->cap);+ s->chosen = (lbool *)realloc(s->chosen, sizeof(lbool) * s->cap);+ s->orderpos = (int *)realloc(s->orderpos, sizeof(int) * s->cap);+ s->reasons = (clause **)realloc(s->reasons, sizeof(clause *) * s->cap);+ s->levels = (int *)realloc(s->levels, sizeof(int) * s->cap);+ s->tags = (lbool *)realloc(s->tags, sizeof(lbool) * s->cap);+ s->trail = (lit *)realloc(s->trail, sizeof(lit) * s->cap);+ s->solution = (lbool *)realloc(s->solution, sizeof(lbool) * s->cap);+ }++ for (var = s->size; var < n; var++) {+ vecp_new(&s->wlists[2 * var]);+ vecp_new(&s->wlists[2 * var + 1]);+ s->activity[var] = 0;+ s->assigns[var] = l_Undef;+ s->chosen[var] = l_False;+ s->orderpos[var] = veci_size(&s->order);+ s->reasons[var] = (clause *)0;+ s->levels[var] = 0;+ s->tags[var] = l_Undef;++ /* does not hold because variables enqueued at top level will not+ be reinserted in the heap+ assert(veci_size(&s->order) == var); + */+ veci_push(&s->order, var);+ order_update(s, var);+ }++ s->size = n > s->size ? n : s->size;+}+++static inline bool enqueue(solver *s, lit l, clause *from) {+ lbool *values = s->assigns;+ int v = lit_var(l);+ lbool val = values[v];++#ifdef VERBOSEDEBUG+ printf(L_IND "enqueue(" L_LIT ")\n", L_ind, L_lit(l));+#endif++ lbool sig = !lit_sign(l);++ sig += sig - 1;+ if (val != l_Undef) {+ return val == sig;+ } else {+ // New fact -- store it.+#ifdef VERBOSEDEBUG+ printf(L_IND "bind(" L_LIT ")\n", L_ind, L_lit(l));+#endif+ int *levels = s->levels;+ clause **reasons = s->reasons;++ values[v] = sig;+ levels[v] = solver_dlevel(s);+ reasons[v] = from;+ s->trail[s->qtail++] = l;++ order_assigned(s, v);+ return true;+ }+}+++static inline void assume(solver *s, lit l) {+ assert(s->qtail == s->qhead);+ assert(s->assigns[lit_var(l)] == l_Undef);+#ifdef VERBOSEDEBUG+ printf(L_IND "assume(" L_LIT ")\n", L_ind, L_lit(l));+#endif+ veci_push(&s->trail_lim, s->qtail);+ enqueue(s, l, (clause *)0);+}+++static inline void solver_canceluntil(solver *s, int level) {+ lit *trail;+ lbool *values;+ clause **reasons;+ int bound;+ int c;++ if (solver_dlevel(s) <= level) {+ return;+ }++ trail = s->trail;+ values = s->assigns;+ reasons = s->reasons;+ bound = (veci_begin(&s->trail_lim))[level];++#ifdef FIXEDORDER+ s->nextvar = lit_var(trail[bound]);+#endif++ for (c = s->qtail - 1; c >= bound; c--) {+ int x = lit_var(trail[c]);+ values[x] = l_Undef;+ reasons[x] = (clause *)0;+ }++ for (c = s->qhead - 1; c >= bound; c--) {+ order_unassigned(s, lit_var(trail[c]));+ }++ s->qhead = s->qtail = bound;+ veci_resize(&s->trail_lim, level);+}++static void solver_record(solver *s, veci *cls) {+ lit *begin = veci_begin(cls);+ lit *end = begin + veci_size(cls);+ clause *c = (veci_size(cls) > 1) ? clause_new(s, begin, end, 1) : (clause *)0;+ enqueue(s, *begin, c);++ assert(veci_size(cls) > 0);++ if (c != 0) {+ vecp_push(&s->learnts, c);+ act_clause_bump(s, c);+ s->stats.learnts++;+ s->stats.learnts_literals += veci_size(cls);+ }+}+++static double solver_progress(solver *s) {+ lbool *values = s->assigns;+ int *levels = s->levels;+ int i;++ double progress = 0;+ double F = 1.0 / s->size;+ for (i = 0; i < s->size; i++) {+ if (values[i] != l_Undef) {+ progress += pow(F, levels[i]);+ }+ }+ return progress / s->size;+}++// ======================================================================+// Major methods:++static bool solver_lit_removable(solver *s, lit l, int minl) {+ lbool *tags = s->tags;+ clause **reasons = s->reasons;+ int *levels = s->levels;+ int top = veci_size(&s->tagged);++ assert(lit_var(l) >= 0 && lit_var(l) < s->size);+ assert(reasons[lit_var(l)] != 0);+ veci_resize(&s->stack, 0);+ veci_push(&s->stack, lit_var(l));++ while (veci_size(&s->stack) > 0) {+ clause *c;+ int v = veci_begin(&s->stack)[veci_size(&s->stack) - 1];+ assert(v >= 0 && v < s->size);+ veci_resize(&s->stack, veci_size(&s->stack) - 1);+ assert(reasons[v] != 0);+ c = reasons[v];++ if (clause_is_lit(c)) {+ int v = lit_var(clause_read_lit(c));+ if (tags[v] == l_Undef && levels[v] != 0) {+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)) {+ veci_push(&s->stack, v);+ tags[v] = l_True;+ veci_push(&s->tagged, v);+ } else {+ int *tagged = veci_begin(&s->tagged);+ int j;+ for (j = top; j < veci_size(&s->tagged); j++)+ tags[tagged[j]] = l_Undef;+ veci_resize(&s->tagged, top);+ return false;+ }+ }+ } else {+ lit *lits = clause_begin(c);+ int i, j;++ for (i = 1; i < clause_size(c); i++) {+ int v = lit_var(lits[i]);+ if (tags[v] == l_Undef && levels[v] != 0) {+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)) {++ veci_push(&s->stack, lit_var(lits[i]));+ tags[v] = l_True;+ veci_push(&s->tagged, v);+ } else {+ int *tagged = veci_begin(&s->tagged);+ for (j = top; j < veci_size(&s->tagged); j++) {+ tags[tagged[j]] = l_Undef;+ }+ veci_resize(&s->tagged, top);+ return false;+ }+ }+ }+ }+ }++ return true;+}++static void solver_analyze(solver *s, clause *c, veci *learnt) {+ lit *trail = s->trail;+ lbool *tags = s->tags;+ clause **reasons = s->reasons;+ int *levels = s->levels;+ int cnt = 0;+ lit p = lit_Undef;+ int ind = s->qtail - 1;+ lit *lits;+ int i, j, minl;+ int *tagged;++ veci_push(learnt, lit_Undef);++ do {+ assert(c != 0);++ if (clause_is_lit(c)) {+ lit q = clause_read_lit(c);+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0) {+ tags[lit_var(q)] = l_True;+ veci_push(&s->tagged, lit_var(q));+ act_var_bump(s, lit_var(q));+ if (levels[lit_var(q)] == solver_dlevel(s)) {+ cnt++;+ } else {+ veci_push(learnt, q);+ }+ }+ } else {++ if (clause_learnt(c)) {+ act_clause_bump(s, c);+ }++ lits = clause_begin(c);+ //printlits(lits,lits+clause_size(c)); printf("\n");+ for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++) {+ lit q = lits[j];+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0) {+ tags[lit_var(q)] = l_True;+ veci_push(&s->tagged, lit_var(q));+ act_var_bump(s, lit_var(q));+ if (levels[lit_var(q)] == solver_dlevel(s)) {+ cnt++;+ } else {+ veci_push(learnt, q);+ }+ }+ }+ }++ while (tags[lit_var(trail[ind--])] == l_Undef) {+ /* empty */+ }++ p = trail[ind + 1];+ c = reasons[lit_var(p)];+ cnt--;++ } while (cnt > 0);++ *veci_begin(learnt) = lit_neg(p);++ lits = veci_begin(learnt);+ minl = 0;+ for (i = 1; i < veci_size(learnt); i++) {+ int lev = levels[lit_var(lits[i])];+ minl |= 1 << (lev & 31);+ }++ // simplify (full)+ for (i = j = 1; i < veci_size(learnt); i++) {+ if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s, lits[i], minl)) {+ lits[j++] = lits[i];+ }+ }++ // update size of learnt + statistics+ s->stats.max_literals += veci_size(learnt);+ veci_resize(learnt, j);+ s->stats.tot_literals += j;++ // clear tags+ tagged = veci_begin(&s->tagged);+ for (i = 0; i < veci_size(&s->tagged); i++) {+ tags[tagged[i]] = l_Undef;+ }+ veci_resize(&s->tagged, 0);++#ifdef DEBUG+ for (i = 0; i < s->size; i++) {+ assert(tags[i] == l_Undef);+ }+#endif++#ifdef VERBOSEDEBUG+ printf(L_IND "Learnt {", L_ind);+ for (i = 0; i < veci_size(learnt); i++) {+ printf(" " L_LIT, L_lit(lits[i]));+ }+#endif+ if (veci_size(learnt) > 1) {+ int max_i = 1;+ int max = levels[lit_var(lits[1])];+ lit tmp;++ for (i = 2; i < veci_size(learnt); i++)+ if (levels[lit_var(lits[i])] > max) {+ max = levels[lit_var(lits[i])];+ max_i = i;+ }++ tmp = lits[1];+ lits[1] = lits[max_i];+ lits[max_i] = tmp;+ }+#ifdef VERBOSEDEBUG+ {+ int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;+ printf(" } at level %d\n", lev);+ }+#endif+}++clause *solver_propagate(solver *s) {+ lbool *values = s->assigns;+ clause *confl = (clause *)0;+ lit *lits;++ //printf("solver_propagate\n");+ while (confl == 0 && s->qtail - s->qhead > 0) {+ lit p = s->trail[s->qhead++];+ vecp *ws = solver_read_wlist(s, p);+ clause **begin = (clause **)vecp_begin(ws);+ clause **end = begin + vecp_size(ws);+ clause **i, **j;++ s->stats.propagations++;+ s->simpdb_props--;++ //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));+ for (i = j = begin; i < end;) {+ if (clause_is_lit(*i)) {+ *j++ = *i;+ if (!enqueue(s, clause_read_lit(*i), clause_from_lit(p))) {+ confl = s->binary;+ (clause_begin(confl))[1] = lit_neg(p);+ (clause_begin(confl))[0] = clause_read_lit(*i++);++ // Copy the remaining watches:+ while (i < end) {+ *j++ = *i++;+ }+ }+ } else {+ lit false_lit;+ lbool sig;++ lits = clause_begin(*i);++ // Make sure the false literal is data[1]:+ false_lit = lit_neg(p);+ if (lits[0] == false_lit) {+ lits[0] = lits[1];+ lits[1] = false_lit;+ }+ assert(lits[1] == false_lit);+ //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");++ // If 0th watch is true, then clause is already satisfied.+ sig = !lit_sign(lits[0]);+ sig += sig - 1;+ if (values[lit_var(lits[0])] == sig) {+ *j++ = *i;+ } else {+ // Look for new watch:+ lit *stop = lits + clause_size(*i);+ lit *k;+ for (k = lits + 2; k < stop; k++) {+ lbool sig = lit_sign(*k);+ sig += sig - 1;+ if (values[lit_var(*k)] != sig) {+ lits[1] = *k;+ *k = false_lit;+ vecp_push(solver_read_wlist(s, lit_neg(lits[1])), *i);+ goto next;+ }+ }++ *j++ = *i;+ // Clause is unit under assignment:+ if (!enqueue(s, lits[0], *i)) {+ confl = *i++;+ // Copy the remaining watches:+ while (i < end) {+ *j++ = *i++;+ }+ }+ }+ }+ next:+ i++;+ }++ s->stats.inspects += j - (clause **)vecp_begin(ws);+ vecp_resize(ws, j - (clause **)vecp_begin(ws));+ }++ return confl;+}++static inline int clause_cmp(const void *x, const void *y) {+ return clause_size((clause *)x) > 2 && (clause_size((clause *)y) == 2 || clause_activity((clause *)x) < clause_activity((clause *)y)) ? -1 : 1;+}++void solver_reducedb(solver *s) {+ int i, j;+ double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity+ clause **learnts = (clause **)vecp_begin(&s->learnts);+ clause **reasons = s->reasons;++ sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);++ for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++) {+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) {+ clause_remove(s, learnts[i]);+ } else {+ learnts[j++] = learnts[i];+ }+ }+ for (; i < vecp_size(&s->learnts); i++) {+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) {+ clause_remove(s, learnts[i]);+ } else {+ learnts[j++] = learnts[i];+ }+ }++ //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);++ vecp_resize(&s->learnts, j);+}++static void solver_simplification(solver *s) {+ lbool *chosen = s->chosen; // specifies whether a decision variable at each level is chosen.+ for (int i = solver_dlevel(s); i >= 0; i--) {+ chosen[i] = l_False;+ }++ // find all decision variables related to implied variables by+ // traversing implication graph.+ for (int c = s->qtail - 1; c >= 0; c--) {+ const int x = lit_var(s->trail[c]);+ clause *cl = s->reasons[x];++ if (s->levels[x] <= s->root_level) {+ continue;+ }++ if (solver_isimplied(s, x)) {+ lit *lits;+ int size;+ lit tmp;++ if (clause_is_lit(cl)) {+ tmp = clause_read_lit(cl);+ lits = &tmp;+ size = 1;+ } else {+ lits = clause_begin(cl);+ size = clause_size(cl);+ }++ for (int j = 0; j < size; j++) {+ const int y = lit_var(lits[j]);+ if (!solver_isimplied(s, y)) {+ assert(s->levels[y] > s->root_level);+ chosen[s->levels[y]] = l_True;+ }+ }+ }+ }++ // choose, in a greedy manner, decision variables that are necessary+ // for CNF to be satisfied. Thus, the set of chosen variables is+ // not necessarily minimal.+#ifdef NONDISJOINT+ const int m = solver_norigclauses(s);+#else+ const int m = solver_nclauses(s);+#endif++ for (int i = 0; i < m; i++) {+ clause *c = vecp_begin(&s->clauses)[i];+ lit *lits = clause_begin(c);+ lbool ischosen = l_False;+ int tmp = -1;++ for (int j = clause_size(c) - 1; j >= 0; j--) {+ const int x = lit_var(lits[j]);+ if (!solver_isimplied(s, x)) {+ lbool sig = !lit_sign(lits[j]);+ sig += sig - 1;+ if (s->assigns[x] == sig) {+ if (chosen[s->levels[x]] == l_True) {+ ischosen = l_True;+ break;+ } else {+ tmp = x;+ }+ }+ }+ }++ if (ischosen != l_True && tmp >= 0) {+ chosen[s->levels[tmp]] = l_True;+ }+ }+++ // Construct a blocking clause of chosen literals.+ veci_resize(&s->blkcls, 0);+ for (int i = solver_dlevel(s); i > s->root_level; i--) {+ if (chosen[i] == l_True) {+ veci_push(&s->blkcls, lit_neg(solver_assumedlit(s, i)));+ }+ }++#ifndef NONDISJOINT+#ifdef GMP+ mpz_set_ui(s->stats.cnt, 1);+ mpz_mul_2exp(s->stats.cnt, s->stats.cnt, solver_dlevel(s) - veci_size(&s->blkcls));+ mpz_add(s->stats.tot_solutions, s->stats.tot_solutions, s->stats.cnt);+#else+ uint64 cnt = 1;+ for (int i = solver_dlevel(s) - veci_size(&s->blkcls); i > 0; i--) {+ if (cnt > ULONG_MAX / 2) {+ cnt = 0;+ break; // overflow+ } else {+ cnt *= 2;+ }+ }+ if (cnt > 0 && s->stats.tot_solutions <= ULONG_MAX - cnt) {+ s->stats.tot_solutions += cnt;+ } else {+ s->stats.tot_solutions = ULONG_MAX; // overflow+ }+#endif+#endif+}+++// note: after using this fuction, propagation stack is canceled!+static lbool solver_testblkcls(solver *s, veci *cls) // for debug+{+ solver_canceluntil(s, s->root_level);++ for (int i = veci_size(cls) - 1; i >= 0; i--) {+ lit l = veci_begin(cls)[i];+ lbool val = s->assigns[lit_var(l)];+ lbool sig = !lit_sign(l);+ sig += sig - 1;+ if (val == l_Undef) {+ assume(s, lit_neg(l));+ clause *confl = solver_propagate(s);+ if (confl != 0) {+ solver_canceluntil(s, s->root_level);+ return l_False;+ }+ } else if (val != sig) {+ solver_canceluntil(s, s->root_level);+ return l_False;+ }+ }++ const int m = solver_nclauses(s);++ for (int i = 0; i < m; i++) {+ int res = l_False;+ clause *c = vecp_begin(&s->clauses)[i];+ lit *lits = clause_begin(c);++ for (int j = clause_size(c) - 1; j >= 0; j--) {+ int x = lit_var(lits[j]);+ lbool sig = !lit_sign(lits[j]);+ sig += sig - 1;+ if (s->assigns[x] == sig)+ res = l_True;+ }++ if (res == l_False) {+ solver_canceluntil(s, s->root_level);+ return l_False;+ }+ }++ solver_canceluntil(s, s->root_level);+ return l_True;+}++const double var_decay = 0.95;+const double clause_decay = 0.999;+const double random_var_freq = 0.02;++// Search a solution. Return l_False if no solution, l_True if final+// solution, or l_Undef if a solution was found (maybe not+// final). Do not call again after l_False or l_True.+// The solution is returned in s->solution.+static lbool solver_search(solver *s, int nof_learnts) {+ int *levels = s->levels;++ veci learnt_clause;++ assert(s->root_level == solver_dlevel(s));++ s->stats.starts++;+ s->var_decay = (float)(1 / var_decay);+ s->cla_decay = (float)(1 / clause_decay);+ veci_new(&learnt_clause);++ for (;;) {+ clause *confl = solver_propagate(s);+ if (confl != 0) {+ // CONFLICT+ int blevel;++#ifdef VERBOSEDEBUG+ printf(L_IND "**CONFLICT**\n", L_ind);+#endif+ s->stats.conflicts++;+ if (solver_dlevel(s) <= s->root_level) {+ veci_delete(&learnt_clause);+ return l_False;+ }++ veci_resize(&learnt_clause, 0);+ solver_analyze(s, confl, &learnt_clause);+ blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;+ blevel = s->root_level > blevel ? s->root_level : blevel;+ solver_canceluntil(s, blevel);+ solver_record(s, &learnt_clause);+ act_var_decay(s);+ act_clause_decay(s);++ } else {+ // NO CONFLICT+ int next;++ if (solver_dlevel(s) == 0) {+ // Simplify the set of problem clauses:+ solver_simplify(s);+ }++ if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) {+ // Reduce the set of learnt clauses:+ solver_reducedb(s);+ }+ // New variable decision:+ s->stats.decisions++;++#ifdef FIXEDORDER // choose next variable in increasing order+ for (next = s->nextvar; next < s->size && s->assigns[next] != l_Undef; next++) {+ /* empty */+ }+ if (!(next < s->size)) {+ next = var_Undef;+ }+#else // use variable selection heuristic+ next = order_select(s, (float)random_var_freq);+#endif+++ if (next == var_Undef) {+#ifdef VERBOSEDEBUG+ printf(L_IND "**MODEL**\n", L_ind);+#endif+ solver_inc_parsol(s);++ if (solver_dlevel(s) <= s->root_level) { // if variables are all implied.+ memcpy(s->solution, s->assigns, solver_nvars(s) * sizeof(lbool));+#ifndef NONDISJOINT+ solver_inc_totsol(s);+#endif+ veci_delete(&learnt_clause);+ return l_True;+ }+#ifdef SIMPLIFY+ solver_simplification(s);+ memcpy(s->solution, s->assigns, solver_nvars(s) * sizeof(lbool));++ if (veci_size(&s->blkcls) == 0) {+ veci_delete(&learnt_clause);+ return l_True;+ }+#else /*NO SIMPLIFY */+ veci_resize(&s->blkcls, 0);+ for (int i = solver_dlevel(s); i > s->root_level; i--) {+ veci_push(&s->blkcls, lit_neg(solver_assumedlit(s, i)));+ }+ memcpy(s->solution, s->assigns, solver_nvars(s) * sizeof(lbool));+ solver_inc_totsol(s);+#endif++#ifndef CONTINUE+#ifdef DEBUG+ lbool res = solver_testblkcls(s, &s->blkcls);+ assert(res == l_True);+#endif+#endif++#ifdef VERBOSEDEBUG+ printf(L_IND "Blocked {", L_ind);+ for (int i = 0; i < veci_size(&s->blkcls); i++) {+ printf(" " L_LIT, L_lit(veci_begin(&s->blkcls)[i]));+ }+ printf(" }\n");+#endif++#ifdef CONTINUE+ veci_resize(&learnt_clause, 0);+ for (int i = solver_dlevel(s); i > s->root_level; i--) {+ veci_push(&learnt_clause, solver_assumedlit(s, i));+ }+ assert(veci_size(&learnt_clause) > 0);+ lit highest_lit = *veci_begin(&learnt_clause); // literal of the highest decision level+ veci_begin(&learnt_clause)[0] = lit_neg(highest_lit);++ solver_canceluntil(s, s->root_level);+ solver_addclause(s, veci_begin(&s->blkcls), veci_size(&s->blkcls));++#ifdef VERBOSEDEBUG+ printf(L_IND "**CONTINUE SEARCH BY SIMULATION**\n", L_ind);+#endif+ // simulate the previous decisions until conflict or+ // contradiction to the previous decisions happen.+ for (int i = veci_size(&learnt_clause) - 1; i >= 0; i--) {+ lit l = veci_begin(&learnt_clause)[i]; // previous decision+ lbool val = s->assigns[lit_var(l)];+ lbool sig = !lit_sign(l);+ sig += sig - 1;++ if (val == l_Undef) {+ assume(s, l);+ if ((confl = solver_propagate(s)) != 0) {+ break;+ }+ } else if (val != sig) {+ break; // contradict to the previous decision+ } else {+ // the previous decision is now implied.+ }+ }+ assert(solver_dlevel(s) < veci_size(&learnt_clause));+ return l_Undef;+ +#else /* not CONTINUE: restart from scratch */+#ifdef VERBOSEDEBUG+ printf(L_IND "**CONTINUE SEARCH FROM SCRATCH**\n", L_ind);+#endif+ solver_canceluntil(s, s->root_level);+ solver_addclause(s, veci_begin(&s->blkcls), veci_size(&s->blkcls));+ veci_delete(&learnt_clause);+ return l_Undef; // restart from scratch+#endif+ } else {+ assume(s, lit_neg(toLit(next)));+ }+ }+ }+}++// ======================================================================+// External solver functions:++solver *solver_new(void) {+ solver *s = (solver *)malloc(sizeof(solver));++ // initialize vectors+ vecp_new(&s->clauses);+ vecp_new(&s->learnts);+ veci_new(&s->order);+ veci_new(&s->trail_lim);+ veci_new(&s->tagged);+ veci_new(&s->stack);+ veci_new(&s->blkcls);++#ifdef FIXEDORDER+ s->nextvar = 0;+#endif++ // initialize arrays+ s->wlists = 0;+ s->activity = 0;+ s->assigns = 0;+ s->chosen = 0;+ s->out = NULL;+ s->orderpos = 0;+ s->reasons = 0;+ s->levels = 0;+ s->tags = 0;+ s->trail = 0;+ s->solution = 0;+ + s->stats.clk = (clock_t) 0;++ // initialize other vars+ s->size = 0;+ s->cap = 0;+ s->qhead = 0;+ s->qtail = 0;+ s->cla_inc = 1;+ s->cla_decay = 1;+ s->var_inc = 1;+ s->var_decay = 1;+ s->root_level = 0;+ s->simpdb_assigns = 0;+ s->simpdb_props = 0;+ s->random_seed = 91648253;+ s->progress_estimate = 0;+ s->binary = (clause *)malloc(sizeof(clause) + sizeof(lit) * 2);+ s->binary->size_learnt = (2 << 1);+ s->verbosity = 0;++ s->stats.starts = 0;+ s->stats.decisions = 0;+ s->stats.propagations = 0;+ s->stats.inspects = 0;+ s->stats.conflicts = 0;+ s->stats.clauses = 0;+ s->stats.clauses_literals = 0;+ s->stats.learnts = 0;+ s->stats.learnts_literals = 0;+ s->stats.max_literals = 0;+ s->stats.tot_literals = 0;++#ifdef GMP+ mpz_init(s->stats.tot_solutions);+ mpz_init(s->stats.par_solutions);+ mpz_init(s->stats.cnt);+ mpz_set_ui(s->stats.tot_solutions, 0);+ mpz_set_ui(s->stats.par_solutions, 0);+#else+ s->stats.tot_solutions = 0;+ s->stats.par_solutions = 0;+#endif++ return s;+}+++void solver_delete(solver *s) {+ int i;++ for (i = 0; i < vecp_size(&s->clauses); i++) {+ free(vecp_begin(&s->clauses)[i]);+ }++ for (i = 0; i < vecp_size(&s->learnts); i++) {+ free(vecp_begin(&s->learnts)[i]);+ }++ // delete vectors+ vecp_delete(&s->clauses);+ vecp_delete(&s->learnts);+ veci_delete(&s->order);+ veci_delete(&s->trail_lim);+ veci_delete(&s->tagged);+ veci_delete(&s->stack);+ veci_delete(&s->blkcls);+ free(s->binary);++#ifdef GMP+ mpz_clear(s->stats.tot_solutions);+ mpz_clear(s->stats.par_solutions);+ mpz_clear(s->stats.cnt);+#endif++ // delete arrays+ if (s->wlists != 0) {+ int i;+ for (i = 0; i < s->size * 2; i++) {+ vecp_delete(&s->wlists[i]);+ }+ // if one is different from null, all are+ free(s->wlists);+ free(s->activity);+ free(s->assigns);+ free(s->chosen);+ free(s->orderpos);+ free(s->reasons);+ free(s->levels);+ free(s->trail);+ free(s->tags);+ free(s->solution);+ }++ free(s);+}+++bool solver_addclause(solver *s, lit *begin, int size) {+ lit *i, *j;+ int maxvar;+ lbool *values;+ lit last;+ lit *end = begin + size;+ + if (size == 0) {+ return false;+ }+ //printlits(begin,end); printf("\n");+ // insertion sort+ maxvar = lit_var(*begin);+ for (i = begin + 1; i < end; i++) {+ lit l = *i;+ maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;+ for (j = i; j > begin && *(j - 1) > l; j--) {+ *j = *(j - 1);+ }+ *j = l;+ }+ solver_setnvars(s, maxvar + 1);++ //printlits(begin,end); printf("\n");+ values = s->assigns;++ // delete duplicates+ last = lit_Undef;+ for (i = j = begin; i < end; i++) {+ //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));+ lbool sig = !lit_sign(*i);+ sig += sig - 1;+ if (*i == lit_neg(last) || sig == values[lit_var(*i)]) {+ return true; // tautology+ } else if (*i != last && values[lit_var(*i)] == l_Undef) {+ last = *j++ = *i;+ }+ }++ //printf("final: "); printlits(begin,j); printf("\n");++ if (j == begin) { // empty clause+ return false;+ } else if (j - begin == 1) { // unit clause+ return enqueue(s, *begin, (clause *)0);+ }+ // create new clause+ vecp_push(&s->clauses, clause_new(s, begin, j, 0));++ s->stats.clauses++;+ s->stats.clauses_literals += j - begin;++ return true;+}+++bool solver_simplify(solver *s) {+ clause **reasons;+ int type;++ assert(solver_dlevel(s) == 0);++ if (solver_propagate(s) != 0) {+ return false;+ }++ if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) {+ return true;+ }++ reasons = s->reasons;+ for (type = 0; type < 2; type++) {+ vecp *cs = type ? &s->learnts : &s->clauses;+ clause **cls = (clause **)vecp_begin(cs);++ int i, j;+ int k = s->norigclauses;+ for (j = i = 0; i < vecp_size(cs); i++) {+ if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && clause_simplify(s, cls[i]) == l_True) {+ clause_remove(s, cls[i]);+ if (!type && i < k) {+ s->norigclauses--;+ }+ } else {+ cls[j++] = cls[i];+ }+ }+ vecp_resize(cs, j);+ }++ s->simpdb_assigns = s->qhead;+ // (shouldn't depend on 'stats' really, but it will do for now)+ s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);++ return true;+}++// Prepare the solver for solving.+void solver_solve_start(solver *s) {+ const double nof_learnts = solver_nclauses(s) / 3;++ s->root_level = solver_dlevel(s);+ s->norigclauses = solver_nclauses(s);+ s->nof_learnts = (int) nof_learnts;+ s->done = false;+}++// Search for the next solution. Return true if a solution was found,+// else false. The solution, if any, is returned in s->solution.+bool solver_solve_next(solver *s) {+ lbool status;++ if (s->done) {+ return false;+ }+ + status = solver_search(s, s->nof_learnts);+ if (status == l_True) {+ s->done = true;+ return true;+ } else if (status == l_False) {+ s->done = true;+ return false;+ } else {+ return true;+ }+}++// Reset solver after searching is finished.+void solver_solve_finish(solver *s) {+ solver_canceluntil(s, 0);+}++// Find all solutions and print them out. Return true if one or more+// solutions were found, else false.+bool solver_solve(solver *s) {+ bool more = true;+ bool found = false;+ + solver_solve_start(s);+ while (more) {+ more = solver_solve_next(s);+ if (more) {+ found = true;+ if (s->out != NULL) {+ for (int x = 0; x < solver_nvars(s); x++) {+ fprintf(s->out, "%d ", (s->solution[x] == l_True) ? x + 1 : -(x + 1));+ }+ fprintf(s->out, "0\n");+ }+ }+ };+ solver_solve_finish(s);+ return found;+}++int solver_nvars(solver *s) {+ return s->size;+}++lbool *solver_solution(solver *s) {+ return s->solution;+}++int solver_nclauses(solver *s) {+ return vecp_size(&s->clauses);+}++int solver_norigclauses(solver *s) {+ return s->norigclauses;+}++int solver_nconflicts(solver *s) {+ return (int)s->stats.conflicts;+}++// ======================================================================+// Sorting functions (sigh):++static inline void selectionsort(void **array, int size, int (*comp) (const void *, const void *)) {+ int i, j, best_i;+ void *tmp;++ for (i = 0; i < size - 1; i++) {+ best_i = i;+ for (j = i + 1; j < size; j++) {+ if (comp(array[j], array[best_i]) < 0) {+ best_i = j;+ }+ }+ tmp = array[i];+ array[i] = array[best_i];+ array[best_i] = tmp;+ }+}++static void sortrnd(void **array, int size, int (*comp) (const void *, const void *), double *seed) {+ if (size <= 15) {+ selectionsort(array, size, comp);+ } else {+ void *pivot = array[irand(seed, size)];+ void *tmp;+ int i = -1;+ int j = size;++ for (;;) {+ do {+ i++;+ } while (comp(array[i], pivot) < 0);+ do {+ j--;+ } while (comp(pivot, array[j]) < 0);++ if (i >= j) {+ break;+ }++ tmp = array[i];+ array[i] = array[j];+ array[j] = tmp;+ }++ sortrnd(array, i, comp, seed);+ sortrnd(&array[i], size - i, comp, seed);+ }+}++void sort(void **array, int size, int (*comp) (const void *, const void *)) {+ double seed = 91648253;+ sortrnd(array, size, comp, &seed);+}
+ c-sources/solver.h view
@@ -0,0 +1,215 @@+/**********************************************************************+MiniSat -- Copyright (c) 2005, Niklas Sorensson+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+**********************************************************************/+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko++#ifndef solver_h+#define solver_h++#ifdef _WIN32+#define inline __inline // compatible with MS VS 6.0+#endif++#include <stdio.h>+#include <time.h>+#include "vec.h"++#ifdef GMP+#include <gmp.h>+#endif++// ======================================================================+// Simple types:++// does not work for c+++typedef int bool;+static const bool true = 1;+static const bool false = 0;++typedef int lit;+typedef char lbool;++#ifdef _WIN32+typedef signed __int64 uint64; // compatible with MS VS 6.0+#else+typedef unsigned long long uint64;+#endif++static const int var_Undef = -1;+static const lit lit_Undef = -2;++static const lbool l_Undef = 0;+static const lbool l_True = 1;+static const lbool l_False = -1;++static inline lit toLit(int v) {+ return v + v;+}++static inline lit lit_neg(lit l) {+ return l ^ 1;+}++static inline int lit_var(lit l) {+ return l >> 1;+}++static inline int lit_sign(lit l) {+ return (l & 1);+}+++// ======================================================================+// Public interface:++// An API function for converting a variable and sign (false='+',+// true='-') to a literal.+extern lit lit_new(int v, bool sign);++struct solver_t;+typedef struct solver_t solver;++// Allocate a new empty solver.+extern solver *solver_new(void);+// Free a solver.+extern void solver_delete(solver *s);++// Add a clause to the solver. The clause consists of an array of n+// literals starting at begin. Literals are created from non-negative+// integers (0,1,2,...) with toLit and lit_neg.+//+// Returns false if the clause is empty, or if it is unsatisfiable in+// the current assignment.+//+// There might be implicit assumptions made about the variables being+// given in increasing order? Not sure, since original code is not+// documented.+extern bool solver_addclause(solver *s, lit *begin, int n);++// Simplify the solver state. Return false if unsatisfiable?+extern bool solver_simplify(solver *s);++// Prepare for solving. Must call this before solver_solve_next().+extern void solver_solve_start(solver *s);++// Search for the next solution. Return true if a solution was found,+// else false. This can be called repeatedly until false. Must call+// solver_solve_start() first, and solver_solve_finish() at the end.+// The solution, if any, can be retrieved with solver_solution.+extern bool solver_solve_next(solver *s);++// Reset solver after searching is finished.+extern void solver_solve_finish(solver *s);++// Solve the constraints and print out all solutions.+extern bool solver_solve(solver *s);++// Get the number of variables.+extern int solver_nvars(solver *s);++// Get the current solution (valid if the most recent call to+// solver_solve_next returned true). The solution is of length+// solver_nvars(s). Note that the returned pointer may be invalidated+// upon further API calls.+extern lbool *solver_solution(solver *s);++extern int solver_nclauses(solver *s);+extern int solver_norigclauses(solver *s);+extern int solver_nconflicts(solver *s);++extern void solver_setnvars(solver *s, int n);++struct stats_t {+ uint64 starts, decisions, propagations, inspects, conflicts;+ uint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;+#ifdef GMP+ mpz_t tot_solutions, par_solutions, cnt;+#else+ uint64 tot_solutions, par_solutions;+#endif+ clock_t clk;+};+typedef struct stats_t stats;++// ======================================================================+// Solver representation:++struct clause_t;+typedef struct clause_t clause;++struct solver_t {+ int size; // nof variables+ int cap; // size of varmaps+ int qhead; // Head index of queue.+ int qtail; // Tail index of queue.++#ifdef FIXEDORDER+ int nextvar; // variable to be considered next+#endif+ // clauses+ vecp clauses; // List of problem constraints. (contains: clause*)+ vecp learnts; // List of learnt clauses. (contains: clause*)++ // activities+ double var_inc; // Amount to bump next variable with.+ double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with.+ float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.++ vecp *wlists; // + double *activity; // A heuristic measurement of the activity of a variable.+ lbool *assigns; // Current values of variables.+ int *orderpos; // Index in variable order.+ clause **reasons; //+ int *levels; //+ lit *trail;++ int norigclauses; // number of original clauses, meaning those not added as blocking clauses. this number dynamically changes due to simplification.+ lbool *chosen; // + FILE *out; //+ veci blkcls; // holds a blocking clause++ clause *binary; // A temporary binary clause+ lbool *tags; //+ veci tagged; // (contains: var)+ veci stack; // (contains: var)++ veci order; // Variable order. (heap) (contains: var)+ veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)+++ int root_level; // Level of first proper decision.+ int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'.+ int simpdb_props; // Number of propagations before next 'simplifyDB()'.+ double random_seed;+ double progress_estimate;+ int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything++ int nof_learnts; // Upper limit on number of learnt clauses during searching+ bool done; // Used by solver_solve_next to remember end of solutions+ lbool *solution; // Used by solver_solve_next to return solution+ + stats stats;+};++#endif /* solver_h */
+ c-sources/vec.h view
@@ -0,0 +1,111 @@+/* **********************************************************************+MiniSat -- Copyright (c) 2005, Niklas Sorensson+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+********************************************************************** */+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko++#ifndef vec_h+#define vec_h++#include <stdlib.h>+++// vector of 32-bit intergers (added for 64-bit portability)+struct veci_t {+ int size;+ int cap;+ int *ptr;+};+typedef struct veci_t veci;++static inline void veci_new(veci *v) {+ v->size = 0;+ v->cap = 4;+ v->ptr = (int *)malloc(sizeof(int) * v->cap);+}++static inline void veci_delete(veci *v) {+ free(v->ptr);+}++static inline int *veci_begin(veci *v) {+ return v->ptr;+}++static inline int veci_size(veci *v) {+ return v->size;+}++static inline void veci_resize(veci *v, int k) {+ v->size = k;+ // only safe to shrink !!+}++static inline void veci_push(veci *v, int e) {+ if (v->size == v->cap) {+ int newsize = v->cap * 2 + 1;+ v->ptr = (int *)realloc(v->ptr, sizeof(int) * newsize);+ v->cap = newsize;+ }+ v->ptr[v->size++] = e;+}++// vector of 32- or 64-bit pointers+struct vecp_t {+ int size;+ int cap;+ void **ptr;+};+typedef struct vecp_t vecp;++static inline void vecp_new(vecp *v) {+ v->size = 0;+ v->cap = 4;+ v->ptr = (void **)malloc(sizeof(void *) * v->cap);+}++static inline void vecp_delete(vecp *v) {+ free(v->ptr);+}++static inline void **vecp_begin(vecp *v) {+ return v->ptr;+}++static inline int vecp_size(vecp *v) {+ return v->size;+}++static inline void vecp_resize(vecp *v, int k) {+ v->size = k;+} // only safe to shrink !!++static inline void vecp_push(vecp *v, void *e) {+ if (v->size == v->cap) {+ int newsize = v->cap * 2 + 1;+ v->ptr = (void **)realloc(v->ptr, sizeof(void *) * newsize);+ v->cap = newsize;+ }+ v->ptr[v->size++] = e;+}++#endif /* vec_h */
+ examples/Sudoku.hs view
@@ -0,0 +1,203 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | A program to solve Sudoku puzzles. It illustrates how to use the+-- MiniSat solver.++module Main where++import SAT.MiniSat++import qualified Data.Map as Map+import Data.Map (Map)+import Data.List+import Data.Char+import System.IO+import System.Environment++-- ----------------------------------------------------------------------+-- * The rules of Sudoku as a SAT problem++-- | 'Cell' /i/ /j/ /n/ is a boolean variable expressing that the cell+-- at row /i/ and column /j/ contains the number /n/.+data Cell = Cell Int Int Int+ deriving (Eq, Ord, Show)++-- | Like the 'Cell' constructor, but return a formula instead of a+-- variable. For convenience.+cell :: Int -> Int -> Int -> Formula Cell+cell i j n = Var (Cell i j n)++-- | The general-purpose Sudoku rules. They state that each cell +-- contain exactly one number, and each number occurs exactly once in+-- each row, column, and 3x3 square.+rules :: Formula Cell+rules = cells :&&: rows :&&: columns :&&: squares+ where+ cells = All [ ExactlyOne [ cell i j n | n <- [1..9] ] | i <- [1..9], j <- [1..9] ]+ rows = All [ ExactlyOne [ cell i j n | j <- [1..9] ] | i <- [1..9], n <- [1..9] ]+ columns = All [ ExactlyOne [ cell i j n | i <- [1..9] ] | j <- [1..9], n <- [1..9] ]+ squares = All [ ExactlyOne [ cell i j n | i <- [i'..i'+2], j <- [j'..j'+2] ] | i' <- [1,4,7], j' <- [1,4,7], n <- [1..9] ]++-- ----------------------------------------------------------------------+-- * Sudoku solver++-- | A datatype for a partially filled Sudoku.+type Sudoku = Map (Int, Int) Int++-- | Turn a 'Sudoku' into a formula.+formula_of_sudoku :: Sudoku -> Formula Cell+formula_of_sudoku s = All [ cell i j n | ((i,j),n) <- Map.toList s ]++-- | Turn a solution into a 'Sudoku'.+sudoku_of_solution :: Map Cell Bool -> Sudoku+sudoku_of_solution m = Map.fromList [ ((i,j),n) | (Cell i j n, True) <- Map.toList m ] ++-- | Solve the Sudoku. Return all solutions.+solve_sudoku :: Sudoku -> [Sudoku]+solve_sudoku s = map sudoku_of_solution (solve_all (rules :&&: formula_of_sudoku s))++-- ----------------------------------------------------------------------+-- * Pretty-printing++-- | Print a 'Sudoku'.+show_sudoku :: Sudoku -> String+show_sudoku s =+ divider+ ++ concat [ row i | i <- [1,2,3] ] + ++ divider+ ++ concat [ row i | i <- [4,5,6] ]+ ++ divider+ ++ concat [ row i | i <- [7,8,9] ]+ ++ divider+ where+ divider = "+-------+-------+-------+\n"+ row i =+ "| "+ ++ intercalate " " [ entry i j | j <- [1, 2, 3]]+ ++ " | "+ ++ intercalate " " [ entry i j | j <- [4, 5, 6]]+ ++ " | "+ ++ intercalate " " [ entry i j | j <- [7, 8, 9]]+ ++ " |\n"+ entry i j = case Map.lookup (i,j) s of+ Nothing -> " "+ Just n -> show n++-- ----------------------------------------------------------------------+-- * Parsing++-- | Create a Sudoku from a list of 81 numbers (using 0 as blank).+sudoku_of_list :: [Int] -> Sudoku+sudoku_of_list xs =+ Map.fromList [ ((i,j),n) | ((i,j),n) <- zip coords xs, 1 <= n && n <= 9 ]+ where+ coords = [ (i,j) | i <- [1..9], j <- [1..9] ]++-- | Read a Sudoku from a string. This accepts the format produced by+-- 'show_sudoku', or a simple list of 81 numbers with 0 representing a+-- blank.+read_sudoku :: String -> Sudoku+read_sudoku s = sudoku_of_list (aux s)+ where+ aux [] = []+ aux (' ':' ':cs) = 0 : aux cs+ aux (c:cs)+ | '0' <= c && c <= '9' = (ord c - ord '0') : aux cs+ | otherwise = aux cs++-- ----------------------------------------------------------------------+-- * Main++-- | Print usage information.+usage :: IO ()+usage = do+ putStrLn "Usage: Sudoku [option]"+ putStrLn "Options:"+ putStrLn " -h, --help - print usage info and exit"+ putStrLn " -p - solve a predefined Sudoku (default)"+ putStrLn " -r - read a Sudoku from stdin and solve"+ putStrLn ""+ putStrLn "The input can be specified in one of two formats:"+ putStrLn "Format 1:"+ putStrLn "+-------+-------+-------+"+ putStrLn "| | 1 4 | 9 |"+ putStrLn "| 4 7 | 2 | 8 |"+ putStrLn "| 6 | 9 | 2 |"+ putStrLn "+-------+-------+-------+"+ putStrLn "| | | 7 6 9 |"+ putStrLn "| 7 | | 3 |"+ putStrLn "| 5 8 6 | | |"+ putStrLn "+-------+-------+-------+"+ putStrLn "| 8 | 2 | 3 |"+ putStrLn "| 6 | 5 | 9 7 |"+ putStrLn "| 7 | 1 4 | |"+ putStrLn "+-------+-------+-------+"+ putStrLn ""+ putStrLn "Format 2:"+ putStrLn "0 0 0 0 1 4 0 9 0"+ putStrLn "0 4 7 0 0 2 0 0 8"+ putStrLn "0 6 0 0 0 9 2 0 0"+ putStrLn "0 0 0 0 0 0 7 6 9"+ putStrLn "7 0 0 0 0 0 0 0 3"+ putStrLn "5 8 6 0 0 0 0 0 0"+ putStrLn "0 0 8 2 0 0 0 3 0"+ putStrLn "6 0 0 5 0 0 9 7 0"+ putStrLn "0 7 0 1 4 0 0 0 0"+++-- | Make the sure the entire string is strictly read before+-- continuing the IO action.+strictly_read :: String -> IO ()+strictly_read [] = return ()+strictly_read (h:t) = strictly_read t++-- | A predefined Sudoku, so the user doesn't have to enter one.+predefined = sudoku_of_list+ [0,0,0,0,1,4,0,9,0,+ 0,4,7,0,0,2,0,0,8,+ 0,6,0,0,0,9,2,0,0,+ 0,0,0,0,0,0,7,6,9,+ 7,0,0,0,0,0,0,0,3,+ 5,8,6,0,0,0,0,0,0,+ 0,0,8,2,0,0,0,3,0,+ 6,0,0,5,0,0,9,7,0,+ 0,7,0,1,4,0,0,0,0]++-- | The main function.+main :: IO ()+main = do+ args <- getArgs+ case args of+ "--help" : _ -> usage+ "-h" : _ -> usage+ "-r" : _ -> do+ str <- getContents+ strictly_read str+ let s = read_sudoku str+ main_with s+ "-p" : _ -> main_with predefined+ [] -> main_with predefined+ o@('-':_) : _ -> do+ hPutStrLn stderr ("Unrecognized option -- " ++ o)+ hPutStrLn stderr "Try --help for more info."+ _ -> do+ hPutStrLn stderr "Invalid command line. Try --help for more info."++-- | Main-like function for solving the given Sudoku.+main_with :: Sudoku -> IO ()+main_with s = do+ putStrLn "Sudoku:"+ putStr (show_sudoku s)+ case solve_sudoku s of+ [] -> do+ putStrLn "No solution."+ [h] -> do+ putStrLn "Unique solution:"+ putStr (show_sudoku h)+ h:t -> do+ putStrLn "Non-unique solution:"+ putStr (show_sudoku h)+ return ()
+ examples/Woodblocks.hs view
@@ -0,0 +1,401 @@+-- Copyright (C) 2016 Peter Selinger.+--+-- This file is free software and may be distributed under the terms+-- of the MIT license. Please see the file LICENSE for details.++-- | A program to solve the Woodblocks puzzle. It illustrates how to use+-- the MiniSat solver.+--+-- The objective of the Woodblocks puzzle is to fit 27 blocks of+-- dimensions /A/×/B/×/C/ into a cube of side length /A/+/B/+/C/.+-- This puzzle was described by D. G. Hoffman in /David Klarner,/+-- /editor, \"The Mathematical Gardner\", pp. 211-225, Springer, 1981/.+--+-- We assume that 0 < (/A/+/B/+/C/)\/4 < /A/ < /B/ < /C/ <+-- (/A/+/B/+/C/)\/2. For concreteness, we use /A/=4, /B/=5, /C/=6.+--+-- We solve the puzzle by reducing it to a SAT problem, then using the+-- "SAT.MiniSat" library to find all 21 solutions.+--+-- For fun, we provide a 'main' function that can either output the+-- solutions in ASCII form, or graphically as a PDF or PostScript+-- document.++module Main where++import Data.List+import Data.Map (Map)+import qualified Data.Map as Map+import Graphics.EasyRender hiding (X, Y)+import System.Environment+import System.IO++import SAT.MiniSat++-- ----------------------------------------------------------------------+-- * Encoding the puzzle as a SAT problem++-- | An axis is 'X', 'Y', or 'Z'. We use the letter /s/ to denote a+-- generic axis.+data Axis = X | Y | Z+ deriving (Show, Eq, Ord)++-- | A length is 'A', 'B', or 'C'. These symbolic constants represent+-- the values /A/=4, /B/=5, and /C/=6, respectively.+--+-- A length in the 'X'-direction is also called \"width\" or 'X'-length.+-- A length in the 'Y'-direction is also called \"depth\" or 'Y'-length.+-- A length in the 'Z'-direction is also called \"height\" or 'Z'-length.+data Length = A | B | C+ deriving (Show, Eq, Ord)++-- | The members of the 'Size' type are symbolic boolean variables.+-- Specifically, the variable+--+-- > Size i j k s n+--+-- is 'True' if and only if the block at position (/i/, /j/, /k/) has+-- /s/-length /n/. This illustrates the use of a structured type as+-- the type of boolean variables in the SAT solver.+data Size = Size Int Int Int Axis Length+ deriving (Show, Eq, Ord)++-- | Like the 'Size' constructor, but return a formula instead of a+-- variable. For convenience.+size :: Int -> Int -> Int -> Axis -> Length -> Formula Size+size i j k s n = Var (Size i j k s n)++-- | Each of the 27 blocks is identified by a triple (/i/, /j/, /k/) of+-- coordinates, ranging from (0, 0, 0) to (2, 2, 2).+type Block = (Int, Int, Int)++-- | The set of all blocks.+blocks :: [(Int, Int, Int)]+blocks = [ (i, j, k) | i <- [0..2], j <- [0..2], k <- [0..2] ]++-- ----------------------------------------------------------------------+-- ** Basic constraints++-- | Functionality constraints: assert that 'Size' encodes a+-- function, i.e., for all /i/, /j/, /k/, /s/, there exists exactly+-- one /n/ such that 'Size' /i/ /j/ /k/ /s/ /n/.+functionality_constraints :: Formula Size+functionality_constraints = All [ ExactlyOne [ size i j k s n | n <- [A, B, C] ] | (i, j, k) <- blocks, s <- [X, Y, Z] ]++-- | Block constraints: assert that each block has exactly+-- one side each of lengths /A/, /B/, /C/.+block_constraints :: Formula Size+block_constraints = All [ ExactlyOne [ size i j k s n | s <- [X, Y, Z] ] | (i, j, k) <- blocks, n <- [A, B, C] ]++-- | Width constraints: assert that each row of blocks+-- contains exactly one block each of lengths /A/, /B/, /C/. This is+-- an easy-to-prove property of the Woodblocks puzzle.+width_constraints :: Formula Size+width_constraints = All [ ExactlyOne [ size i j k X n | i <- [0..2] ] | j <- [0..2], k <- [0..2], n <- [A, B, C] ]++-- | Depth constraints: like 'width_constraints', but in the+-- 'Y'-direction.+depth_constraints :: Formula Size+depth_constraints = All [ ExactlyOne [ size i j k Y n | j <- [0..2] ] | i <- [0..2], k <- [0..2], n <- [A, B, C] ]++-- | Height constraints: like 'width_constraints', but in the+-- 'Z'-direction.+height_constraints :: Formula Size+height_constraints = All [ ExactlyOne [ size i j k Z n | k <- [0..2] ] | i <- [0..2], j <- [0..2], n <- [A, B, C] ]++-- ----------------------------------------------------------------------+-- ** Overlap constraints++-- $ The basic constraints are sufficient to ensure that adjacent+-- blocks (i.e., those that have a face in common) do not overlap.+-- However, we must also ensure that blocks don't overlap along an+-- edge or a corner. The overlap constraints ensure this. We+-- symbolically compute the minimal and maximal /x/-, /y/-, and+-- /z/-coordinate of each block. We use the fact that two blocks are+-- non-overlapping iff+--+-- x1' ≤ x0 or x1 ≤ x0' or y1' ≤ y0 or y1 ≤ y0' or z1' ≤ z0 or z1 ≤ z0'.++-- | 'Coord' is a symbolic representation of a coordinate, i.e., a+-- number. These are relative to 0, or relative to the quantity /L/ =+-- /A/+/B/+/C/.+data Coord =+ Zero -- ^ The number 0.+ | LengthOf Axis Block -- ^ The /s/-length of block /b/.+ | LMinusLengthOf Axis Block -- ^ /L/ minus the /s/-length of block /b/.+ | L -- ^ The number /L/.+ deriving (Show)++-- | Symbolically calculate the minimum /s/-coordinate of block+-- (/i/, /j/, /k/).+mincoord :: Axis -> Block -> Coord+mincoord X (0, j, k) = Zero+mincoord X (1, j, k) = LengthOf X (0, j, k)+mincoord X (2, j, k) = LMinusLengthOf X (2, j, k)+mincoord X (3, j, k) = L+mincoord Y (i, 0, k) = Zero+mincoord Y (i, 1, k) = LengthOf Y (i, 0, k)+mincoord Y (i, 2, k) = LMinusLengthOf Y (i, 2, k)+mincoord Y (i, 3, k) = L+mincoord Z (i, j, 0) = Zero+mincoord Z (i, j, 1) = LengthOf Z (i, j, 0)+mincoord Z (i, j, 2) = LMinusLengthOf Z (i, j, 2)+mincoord Z (i, j, 3) = L+mincoord _ (_, _, _) = error "mincoord"++-- | Symbolically calculate the maximum /s/-coordinate of block+-- (/i/, /j/, /k/).+maxcoord :: Axis -> Block -> Coord+maxcoord X (i, j, k) = mincoord X (i+1, j, k)+maxcoord Y (i, j, k) = mincoord Y (i, j+1, k)+maxcoord Z (i, j, k) = mincoord Z (i, j, k+1)++-- | 'leq_length' /b1/ /s1/ /b2/ /s2/: a constraint asserting that the+-- /s1/-length of block /b1/ is less than or equal to to /s2/-length+-- of block /b2/.+leq_length :: Block -> Axis -> Block -> Axis -> Formula Size+leq_length (i, j, k) s (i', j', k') s' =+ size i j k s A :||: size i' j' k' s' C :||: (size i j k s B :&&: size i' j' k' s' B)++-- | 'leq' /c1/ /c2/: a constraint asserting that one formal coordinate is+-- less than or equal another.+leq :: Coord -> Coord -> Formula Size+leq Zero _ = Yes+leq _ Zero = No+leq (LengthOf s1 b1) (LengthOf s2 b2) = leq_length b1 s1 b2 s2+leq (LengthOf s1 b1) _ = Yes+leq _ (LengthOf s2 b2) = No+leq (LMinusLengthOf s1 b1) (LMinusLengthOf s2 b2) = leq_length b2 s2 b1 s1+leq (LMinusLengthOf s1 b1) _ = Yes+leq L (LMinusLengthOf s2 b2) = No+leq L L = Yes++-- | 'disjoint' /b1/ /b2/ is a constraint asserting that blocks /b1/+-- and /b2/ do not overlap.+disjoint :: Block -> Block -> Formula Size+disjoint b1 b2 =+ leq (maxcoord X b1) (mincoord X b2)+ :||: leq (maxcoord Y b1) (mincoord Y b2)+ :||: leq (maxcoord Z b1) (mincoord Z b2)+ :||: leq (maxcoord X b2) (mincoord X b1)+ :||: leq (maxcoord Y b2) (mincoord Y b1)+ :||: leq (maxcoord Z b2) (mincoord Z b1)++-- | Overlap constraints: assert that no two distinct blocks overlap.+overlap_constraints :: Formula Size+overlap_constraints = All [ disjoint b1 b2 | b1 <- blocks, b2 <- blocks, b1 /= b2 ]++-- ----------------------------------------------------------------------+-- ** Symmetry constraints++-- | Without loss of generality (up to symmetry), we can fix the+-- orientation of the central block, as well as the /s/-lengths of+-- its /s/-neighbors, for /s/ ∈ {/X/, /Y/, /Z/}.+symmetry_constraints :: Formula Size+symmetry_constraints =+ size 1 1 1 X A+ :&&: size 1 1 1 Y B+ :&&: size 1 1 1 Z C+ :&&: size 0 1 1 X B+ :&&: size 2 1 1 X C+ :&&: size 1 0 1 Y A+ :&&: size 1 2 1 Y C+ :&&: size 1 1 0 Z A+ :&&: size 1 1 2 Z B++-- ----------------------------------------------------------------------+-- ** Summary of constraints++-- | The complete set of puzzle constraints.+puzzle :: Formula Size+puzzle =+ functionality_constraints+ :&&: block_constraints+ :&&: width_constraints+ :&&: depth_constraints+ :&&: height_constraints+ :&&: overlap_constraints+ :&&: symmetry_constraints++-- ----------------------------------------------------------------------+-- * Solving the puzzle++-- | A solution can be represented as a function mapping each triple of+-- block coordinates (/i/, /j/, /k/) to an orientation.+type Solution = Int -> Int -> Int -> (Length, Length, Length)++-- | Map a solution of the SAT formula to a solution of the puzzle.+solution_of_sat :: Map Size Bool -> Solution+solution_of_sat m = f+ where+ m' = Map.fromList [ ((i, j, k, s), n) | (Size i j k s n, True) <- Map.toList m ]+ f i j k = (x, y, z)+ where+ x = m' Map.! (i, j, k, X)+ y = m' Map.! (i, j, k, Y)+ z = m' Map.! (i, j, k, Z)++-- | The set of all solutions to the Woodblocks puzzle. +solutions :: [Solution]+solutions = map solution_of_sat sat_solutions+ where+ sat_solutions = solve_all puzzle++-- ----------------------------------------------------------------------+-- * ASCII output++-- | Show a list, using the given arguments /nil/, /left/, /comma/,+-- /right/, and the given /show/ function for elements.+show_list :: String -> String -> String -> String -> (a -> String) -> [a] -> String+show_list nil left comma right show [] = nil+show_list nil left comma right show xs = left ++ intercalate comma [ show x | x <- xs ] ++ right++-- | Show the block sizes in a grid.+show_solution :: Solution -> String+show_solution f = "Solution:\n" ++ show_list "" "" "\n" "" (show_list "" "" "\n" "\n" (show_list "" "" " " "" show)) xs+ where+ xs = [ [ [ f i j k | i <- [0,1,2] ] | j <- [0,1,2] ] | k <- [0,1,2] ]++-- | Main function for ASCII output.+main_ascii :: IO ()+main_ascii = sequence_ [ print_sol s | s <- solutions ]+ where+ print_sol s = do+ putStrLn (show_solution s)++-- ----------------------------------------------------------------------+-- * Graphical output++-- | A point in 3-space.+type Point = (Int, Int, Int)++-- | A box in 3-space.+type Box = (Point, Point)++-- | Convert a dimension to an integer.+int_of_dim :: Length -> Int+int_of_dim A = 4+int_of_dim B = 5+int_of_dim C = 6++-- | Calculate the minimum /s/-coordinate of block (/i/,/j/,/k/).+smin :: Solution -> Axis -> Int -> Int -> Int -> Int+smin sol X i j k = sum [ int_of_dim x | i' <- [0..i-1], let (x,y,z) = sol i' j k ]+smin sol Y i j k = sum [ int_of_dim y | j' <- [0..j-1], let (x,y,z) = sol i j' k ]+smin sol Z i j k = sum [ int_of_dim z | k' <- [0..k-1], let (x,y,z) = sol i j k' ]++-- | Calculate a block's box.+box_of_block :: Solution -> Int -> Int -> Int -> Box+box_of_block sol i j k = ((x0, y0, z0), (x1, y1, z1))+ where+ x0 = smin sol X i j k+ x1 = smin sol X (i+1) j k+ y0 = smin sol Y i j k+ y1 = smin sol Y i (j+1) k+ z0 = smin sol Z i j k+ z1 = smin sol Z i j (k+1)++-- | Display a box as a rectangle. This is relative to the current+-- coordinate system. The height is printed in the center of the box.+rectangle_of_box :: Box -> Draw ()+rectangle_of_box ((x0, y0, z0), (x1, y1, z1)) = do+ rectangle x0' y0' (x1'-x0') (y1'-y0')+ fillstroke fillcolor+ -- textbox 0.5 font textcolor x0' yc' x1' yc' 0.3 (show (z1 - z0))+ where+ font = Font TimesRoman 2+ textcolor = Color_Gray 0.0+ fillcolor = Color_Gray ((8 + z0' - z1') / 5)+ x0' = fromIntegral x0+ x1' = fromIntegral x1+ y0' = fromIntegral y0+ y1' = fromIntegral y1+ z0' = fromIntegral z0+ z1' = fromIntegral z1+ yc' = (y0' + y1') / 2++-- | Display a layer relative to the current coordinate system.+draw_layer :: Solution -> Int -> Draw ()+draw_layer sol k = do+ -- Todo: add background+ sequence_ [ rectangle_of_box (box_of_block sol i j k) | i <- [0..2], j <- [0..2] ]+ -- Todo: overlay grid++-- | Display a solution, relative to the current coordinate system.+draw_solution :: Solution -> Draw ()+draw_solution sol = do+ block $ do+ draw_layer sol 0+ translate 17.5 0+ draw_layer sol 1+ translate 17.5 0+ draw_layer sol 2++-- | Display a list of solutions, relative to the current coordinate system.+draw_solutions :: [Solution] -> Draw ()+draw_solutions sols = block $ aux sols+ where+ aux [] = return ()+ aux (h:t) = do+ translate 0 (-15)+ draw_solution h+ translate 0 (-5)+ aux t++-- | Divide a list into sublists of length /n/.+paginate :: Int -> [a] -> [[a]]+paginate n [] = []+paginate n xs = x1s : paginate n x2s+ where+ (x1s, x2s) = splitAt n xs++-- | Display a list of solutions as a document.+document_of_solutions :: [Solution] -> Document ()+document_of_solutions sols = do+ sequence_ [ dopage ss | ss <- solss ]+ where+ solss = paginate 6 sols -- solutions per page+ dopage ss = do+ newpage (72*8.5) (72*11) $ do+ -- Set up coordinate system: origin is 1 inch from upper left+ scale 72 72+ translate 4.25 10+ scale (9/115) (9/115)+ translate (-25) 0+ setlinewidth 0.2+ draw_solutions ss++-- | Main function for graphical output.+main_graphical :: RenderFormat -> IO ()+main_graphical fmt = do+ let document = document_of_solutions solutions+ render_stdout fmt document++-- ----------------------------------------------------------------------+-- * Main++-- | Print usage information.+usage :: IO ()+usage = do+ putStrLn "Usage: Woodblocks [option]"+ putStrLn "Options:"+ putStrLn " -h, --help - print usage info and exit"+ putStrLn " -a - ASCII output (default)"+ putStrLn " -f - PDF output"+ putStrLn " -p - PostScript output"++-- | The main function.+main = do+ args <- getArgs+ case args of+ "--help" : _ -> usage+ "-h" : _ -> usage+ "-f" : _ -> main_graphical Format_PDF+ "-p" : _ -> main_graphical Format_PS+ "-a" : _ -> main_ascii+ [] -> main_ascii+ o@('-':_) : _ -> do+ hPutStrLn stderr ("Unrecognized option -- " ++ o)+ hPutStrLn stderr "Try --help for more info."+ _ -> do+ hPutStrLn stderr "Invalid command line. Try --help for more info."
+ minisat-solver.cabal view
@@ -0,0 +1,147 @@+-- The name of the package.+name: minisat-solver++-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented.+-- http://www.haskell.org/haskellwiki/Package_versioning_policy+-- PVP summary: +-+------- breaking API changes+-- | | +----- non-breaking API additions+-- | | | +--- code changes with no API change+version: 0.1++-- A short (one-line) description of the package.+synopsis: High-level Haskell bindings for the MiniSat SAT solver.++-- A longer description of the package.+description: ++ This package provides high-level Haskell bindings for the well-known+ MiniSat satisfiability solver. It solves the boolean satisfiability+ problem, i.e., the input is a boolean formula, and the output is a+ list of all satisfying assignments.++ MiniSat is a fully automated, well-optimized general-purpose SAT+ solver written by Niklas Een and Niklas Sorensson, and further+ modified by Takahisa Toda.++ Unlike other similar Haskell packages, we provide a convenient+ high-level interface to the SAT solver, hiding the complexity of the+ underlying C implementation. It can be easily integrated into other+ programs as an efficient turn-key solution to many search problems.++ To illustrate the use of the library, two example programs are+ included in the "examples" directory; one program solves Sudoku+ puzzles, and the other solves a 3-dimensional block packing+ problem. These programs can be built manually, or by invoking Cabal+ with the '--enable-benchmarks' option.+ +-- URL for the project homepage or repository.+homepage: http://www.mathstat.dal.ca/~selinger/minisat-solver/++-- The license under which the package is released.+license: MIT++-- The file containing the license text.+license-file: LICENSE++-- The package author(s).+author: Peter Selinger++-- An email address to which users can send suggestions, bug reports, and +-- patches.+maintainer: selinger@mathstat.dal.ca++-- A copyright notice.+copyright: Copyright (c) 2016 Peter Selinger,+ Copyright (c) 2015 Takahisa Toda,+ Copyright (c) 2005 Niklas Sorensson++-- A classification category for future use by the package catalogue+-- Hackage. These categories have not yet been specified, but the+-- upper levels of the module hierarchy make a good start.+category: Logic++-- The type of build used by this package.+build-type: Simple++-- Constraint on the version of Cabal needed to build this package.+cabal-version: >=1.8++-- A list of additional files to be included in source distributions+-- built with setup sdist.+extra-source-files:+ ChangeLog+ c-sources/ChangeLog+ c-sources/LICENSE.MiniSat+ c-sources/LICENSE.bc_minisat_all+ c-sources/main.c+ c-sources/Makefile+ c-sources/README.html+ c-sources/README.pdf+ c-sources/solver.h+ c-sources/vec.h++-- ----------------------------------------------------------------------+library+ extensions: ForeignFunctionInterface+ + -- Modules exported by the library.+ exposed-modules: SAT.MiniSat+ + -- Modules included in this library but not exported.+ other-modules: SAT.MiniSat.LowLevel+ SAT.MiniSat.Literals+ SAT.MiniSat.Monadic+ SAT.MiniSat.Functional+ SAT.MiniSat.Variable+ SAT.MiniSat.Formula++ -- A list of directories to search for header files.+ include-dirs: c-sources++ c-sources: c-sources/solver.c++ includes: solver.h+ vec.h+ + -- Other library packages from which modules are imported.+ build-depends: base >= 4.6 && < 5,+ transformers,+ containers++-- ----------------------------------------------------------------------+benchmark Sudoku+ type: exitcode-stdio-1.0++ -- .hs or .lhs file containing the Main module.+ main-is: Sudoku.hs++ -- Root directories for the module hierarchy.+ hs-source-dirs: examples++ -- Modules included in this executable, other than Main.+ -- other-modules:++ -- Other library packages from which modules are imported.+ build-depends: base >= 4.6 && < 5,+ containers,+ minisat-solver++-- ----------------------------------------------------------------------+benchmark Woodblocks+ type: exitcode-stdio-1.0++ -- .hs or .lhs file containing the Main module.+ main-is: Woodblocks.hs++ -- Root directories for the module hierarchy.+ hs-source-dirs: examples++ -- Modules included in this executable, other than Main.+ -- other-modules:++ -- Other library packages from which modules are imported.+ build-depends: base >= 4.6 && < 5,+ easyrender,+ containers,+ minisat-solver