diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,675 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. + diff --git a/SAT/Solver/Mios.hs b/SAT/Solver/Mios.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios.hs @@ -0,0 +1,298 @@ +-- | Minisat-based Implementation and Optimization Study on SAT solver +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios + ( + -- * Interface to the core of solver + versionId + , CNFDescription (..) + , module SAT.Solver.Mios.OptionParser + , runSolver + , solveSAT + , solveSATWithConfiguration + , solve + , getModel + -- * Assignment Validator + , validateAssignment + , validate + -- * For standalone programs + , executeSolverOn + , executeSolver + , executeValidatorOn + , executeValidator + -- * File IO + , dumpAssigmentAsCNF + ) + where + +import Control.Monad ((<=<), unless, void, when) +import Data.Char +import qualified Data.ByteString.Char8 as B +import Data.List +import qualified Data.Vector.Unboxed as U +import Numeric (showFFloat) +import System.CPUTime +import System.Exit +import System.IO + +import SAT.Solver.Mios.Types +import SAT.Solver.Mios.Internal +import SAT.Solver.Mios.Solver +import SAT.Solver.Mios.M114 +import SAT.Solver.Mios.OptionParser +import SAT.Solver.Mios.Validator + +reportElapsedTime :: Bool -> String -> Integer -> IO Integer +reportElapsedTime False _ _ = return 0 +reportElapsedTime _ _ 0 = getCPUTime +reportElapsedTime _ mes t = do + now <- getCPUTime + let toSecond = 1000000000000 :: Double + hPutStr stderr mes + hPutStrLn stderr $ showFFloat (Just 3) ((fromIntegral (now - t)) / toSecond) " sec" + return now + +-- | executes a solver on the given CNF file +-- This is the simplest entry to standalone programs; not for Haskell programs +executeSolverOn :: FilePath -> IO () +executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path }) + +-- | executes a solver on the given 'arg :: MiosConfiguration' +-- | This is another entry point for standalone programs. +executeSolver :: MiosProgramOption -> IO () +executeSolver opts@(_targetFile -> target@(Just cnfFile)) = do + t0 <- reportElapsedTime (_confTimeProbe opts) "" 0 + (desc, cls) <- parseHeader target <$> B.readFile cnfFile + when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile + s <- newSolver (toMiosConf opts) desc + parseClauses s desc cls + t1 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0 + when (_confVerbose opts) $ do + nc <- nClauses s + hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (nVars s, _numberOfVariables desc) ++ " #c = " ++ show (nc, _numberOfClauses desc) + res <- simplifyDB s + -- when (_confVerbose opts) $ hPutStrLn stderr $ "`simplifyDB`: " ++ show res + result <- solve s [] + case result of + True | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE" + False | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE" + True -> print =<< getModel s + False -> do -- contradiction + -- FIXMEin future + when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" + -- print =<< map lit2int <$> asList (conflict s) + putStrLn "[]" + case _outputFile opts of + Just fname -> dumpAssigmentAsCNF fname result =<< getModel s + Nothing -> return () + t2 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Solve: ") t1 + when (result && _confCheckAnswer opts) $ do + asg <- getModel s + s' <- newSolver (toMiosConf opts) desc + parseClauses s' desc cls + good <- validate s' asg + if _confVerbose opts + then hPutStrLn stderr $ if good then "A vaild answer" else "Internal error: mios returns a wrong answer" + else unless good $ hPutStrLn stderr "Internal error: mios returns a wrong answer" + void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2 + void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0 + when (_confStatProbe opts) $ do + hPutStr stderr $ "## [" ++ showPath cnfFile ++ "] " + hPutStrLn stderr . intercalate ", " . map (\(k, v) -> show k ++ ": " ++ show v) =<< getStats s + +executeSolver _ = return () + +-- | new top-level interface that returns +-- +-- * conflicting literal set :: Left [Int] +-- * satisfiable assignment :: Right [Int] +-- +runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) +runSolver m d c = do + s <- newSolver m d + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) c + noConf <- simplifyDB s + if noConf + then do + x <- solve s [] + if x + then Right <$> getModel s + else Left . map lit2int <$> asList (conflict s) + else return $ Left [] + + +-- | the easiest interface for Haskell programs +-- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@ +-- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@. +-- The second part of the first argument is a list of vector, which 0th element is the number of its real elements +solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int] +solveSAT = solveSATWithConfiguration defaultConfiguration + +-- | solves the problem (2rd arg) under the configuration (1st arg) +-- and returns an assignment as list of literals :: Int +solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int] +solveSATWithConfiguration conf desc cls = do + s <- newSolver conf desc + -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1] + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls + noConf <- simplifyDB s + if noConf + then do + result <- solve s [] + if result + then getModel s + else return [] + else return [] + +-- | validates a given assignment from STDIN for the CNF file (2nd arg) +-- this is the entry point for standalone programs +executeValidatorOn :: FilePath -> IO () +executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path }) + +-- | validates a given assignment for the problem (2nd arg) +-- this is another entry point for standalone programs; see app/mios.hs +executeValidator :: MiosProgramOption -> IO () +executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do + (desc, cls) <- parseHeader target <$> B.readFile cnfFile + when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile + s <- newSolver (toMiosConf opts) desc + parseClauses s desc cls + when (_confVerbose opts) $ + hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc) + when (_confVerbose opts) $ do + nc <- nClauses s + nl <- nLearnts s + hPutStrLn stderr $ "(nv, nc, nl) = " ++ show (nVars s, nc, nl) + asg <- read <$> getContents + unless (_confNoAnswer opts) $ print asg + result <- s `validate` (asg :: [Int]) + if result + then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess + else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure + +executeValidator _ = return () + +-- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg) +-- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@, +-- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@ +validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool +validateAssignment desc cls asg = do + s <- newSolver defaultConfiguration desc + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls + s `validate` asg + +-- | dumps an assigment to file. +-- 2nd arg is +-- +-- * @True@ if the assigment is satisfiable assigment +-- +-- * @False@ if not +-- +-- >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s +-- +dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO () +dumpAssigmentAsCNF fname False _ = do + withFile fname WriteMode $ \h -> do + hPutStrLn h "UNSAT" + +dumpAssigmentAsCNF fname True l = do + withFile fname WriteMode $ \h -> do + hPutStrLn h "SAT" + hPutStrLn h . unwords $ map show l + +-------------------------------------------------------------------------------- +-- DIMACS CNF Reader +-------------------------------------------------------------------------------- + +parseHeader :: Maybe FilePath -> B.ByteString -> (CNFDescription, B.ByteString) +parseHeader target bs = if B.head bs == 'p' then (parseP l, B.tail bs') else parseHeader target (B.tail bs') + where + (l, bs') = B.span ('\n' /=) bs + -- format: p cnf n m, length "p cnf" == 5 + parseP line = case B.readInt $ B.dropWhile (`elem` " \t") (B.drop 5 line) of + Just (x, second) -> case B.readInt (B.dropWhile (`elem` " \t") second) of + Just (y, _) -> CNFDescription x y target + _ -> CNFDescription 0 0 target + _ -> CNFDescription 0 0 target + +parseClauses :: Solver -> CNFDescription -> B.ByteString -> IO () +parseClauses s (CNFDescription nv nc _) bs = do + let maxLit = int2lit $ negate nv + buffer <- newVec $ maxLit + 1 + polvec <- newVecBool (maxLit + 1) False + let + loop :: Int -> B.ByteString -> IO () + loop ((< nc) -> False) _ = return () + loop i b = loop (i + 1) =<< readClause s buffer polvec b + loop 0 bs + -- static polarity + let + asg = assigns s + checkPolarity :: Int -> IO () + checkPolarity ((< nv) -> False) = return () + checkPolarity v = do + p <- getNthBool polvec $ var2lit v True + n <- getNthBool polvec $ var2lit v False + when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse + checkPolarity $ v + 1 + checkPolarity 1 + +skipWhitespace :: B.ByteString -> B.ByteString +skipWhitespace s + | elem c " \t\n" = skipWhitespace $ B.tail s + | otherwise = s + where + c = B.head s + +-- | skip comment lines +-- __Pre-condition:__ we are on the benngining of a line +skipComments :: B.ByteString -> B.ByteString +skipComments s + | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s + | otherwise = s + where + c = B.head s + +parseInt :: B.ByteString -> (Int, B.ByteString) +parseInt st = do + let + zero = ord '0' + loop :: B.ByteString -> Int -> (Int, B.ByteString) + loop s val = case B.head s of + c | '0' <= c && c <= '9' -> loop (B.tail s) (val * 10 + ord c - zero) + _ -> (val, B.tail s) + case B.head st of + '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x) + '+' -> loop st (0 :: Int) + c | '0' <= c && c <= '9' -> loop st 0 + _ -> error "PARSE ERROR! Unexpected char" + +readClause :: Solver -> Vec -> VecBool -> B.ByteString -> IO B.ByteString +readClause s buffer pvec stream = do + let + loop :: Int -> B.ByteString -> IO B.ByteString + loop i b = do + let (k, b') = parseInt $ skipWhitespace b + if k == 0 + then do + -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack + setNth buffer 0 $ i - 1 + addClause s buffer + return b' + else do + let l = int2lit k + setNth buffer i l + setNthBool pvec l True + loop (i + 1) b' + loop 1 . skipComments . skipWhitespace $ stream + + +showPath :: FilePath -> String +showPath str + | elem '/' str = take (len - length basename) (repeat ' ') ++ basename + | otherwise = take (len - length basename') (repeat ' ') ++ basename' + where + len = 50 + basename = reverse . takeWhile (/= '/') . reverse $ str + basename' = take len str diff --git a/SAT/Solver/Mios/Clause.hs b/SAT/Solver/Mios/Clause.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Clause.hs @@ -0,0 +1,144 @@ +-- | Clause, a data supporting pointer-based equality +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MagicHash + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Clause + ( + Clause (..) +-- , isLit +-- , getLit + , shrinkClause + , newClauseFromVec + , sizeOfClause + -- * Vector of Clause + , ClauseVector + , newClauseVector + , getNthClause + , setNthClause + , swapClauses + ) + where + +import Control.Monad (forM_) +import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#) +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV +import qualified Data.Vector.Unboxed.Mutable as UV +import Data.List (intercalate) +import SAT.Solver.Mios.Types + +-- | __Fig. 7.(p.11)__ +-- clause, null, binary clause. +-- This matches both of @Clause@ and @GClause@ in MiniSat +-- TODO: GADTs is better? +data Clause = Clause + { + learnt :: !Bool -- ^ whether this is a learnt clause + , activity :: !DoubleSingleton -- ^ activity of this clause + , protected :: !BoolSingleton -- ^ protected from reduce + , lbd :: !IntSingleton -- ^ storing the LBD; values are computed in Solver + , lits :: !Vec -- ^ which this clause consists of + } +-- | BinaryClause Lit -- binary clause consists of only a propagating literal + | NullClause -- as null pointer + +-- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'. +instance Eq Clause where + {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-} + (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y) + +instance Show Clause where + show NullClause = "NullClause" + show _ = "a clause" + +-- | supports a restricted set of 'VectorFamily' methods +instance VectorFamily Clause Lit where + dump mes NullClause = return $ mes ++ "Null" + dump mes Clause{..} = do + a <- show <$> getDouble activity + (len:ls) <- asList lits + return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}" + {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-} + asVec Clause{..} = UV.unsafeTail lits + {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-} + asList NullClause = return [] + asList Clause{..} = do + (n : ls) <- asList lits + return $ take n ls + +-- returns True if it is a 'BinaryClause' +-- FIXME: this might be discarded in minisat 2.2 +-- isLit :: Clause -> Bool +-- isLit (BinaryClause _) = True +-- isLit _ = False + +-- returns the literal in a BinaryClause +-- FIXME: this might be discarded in minisat 2.2 +-- getLit :: Clause -> Lit +-- getLit (BinaryClause x) = x + +-- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes +-- liftToClause :: Clause -> Clause +-- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting" + +-- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals +{-# INLINABLE shrinkClause #-} +shrinkClause :: Int -> Clause -> IO () +shrinkClause !n Clause{..} = setNth lits 0 . subtract n =<< getNth lits 0 + +-- | copies /vec/ and return a new 'Clause' +-- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically. +{-# INLINE newClauseFromVec #-} +newClauseFromVec :: Bool -> Vec -> IO Clause +newClauseFromVec l vec = do + n <- getNth vec 0 + v <- newVec $ n + 1 + forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i + Clause l <$> newDouble 0 <*> newBool False <*> newInt n <*> return v + +-- | returns the number of literals in a clause, even if the given clause is a binary clause +{-# INLINE sizeOfClause #-} +sizeOfClause :: Clause -> IO Int +-- sizeOfClause (BinaryClause _) = return 1 +sizeOfClause !c = getNth (lits c) 0 + +-------------------------------------------------------------------------------- + +-- | Mutable 'Clause' Vector +type ClauseVector = MV.IOVector Clause + +instance VectorFamily ClauseVector Clause where + asList cv = V.toList <$> V.freeze cv + dump mes cv = do + l <- asList cv + sts <- mapM (dump ",") (l :: [Clause]) + return $ mes ++ tail (concat sts) + +-- | returns a new 'ClauseVector' +newClauseVector :: Int -> IO ClauseVector +newClauseVector n = do + v <- MV.new (max 4 n) + MV.set v NullClause + return v + +-- | returns the nth 'Clause' +{-# INLINE getNthClause #-} +getNthClause :: ClauseVector -> Int -> IO Clause +getNthClause = MV.unsafeRead + +-- | sets the nth 'Clause' +{-# INLINE setNthClause #-} +setNthClause :: ClauseVector -> Int -> Clause -> IO () +setNthClause = MV.unsafeWrite + +-- | swaps the two 'Clause's +{-# INLINE swapClauses #-} +swapClauses :: ClauseVector -> Int -> Int -> IO () +swapClauses = MV.unsafeSwap diff --git a/SAT/Solver/Mios/ClauseManager.hs b/SAT/Solver/Mios/ClauseManager.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/ClauseManager.hs @@ -0,0 +1,324 @@ +-- | A shrinkable 'VectorFamily' of 'C.Clause' +{-# LANGUAGE + BangPatterns + , DuplicateRecordFields + , FlexibleInstances + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.ClauseManager + ( + -- * higher level interface for ClauseVector + ClauseManager (..) +-- -- * vector of clauses +-- , SimpleManager + -- * Manager with an extra Int (used as sort key or blocking literal) + , ClauseExtManager + , pushClauseWithKey + , getKeyVector + , markClause +-- , purifyManager + -- * WatcherList + , WatcherList + , newWatcherList + , getNthWatcher + , garbageCollect +-- , numberOfRegisteredClauses + ) + where + +import Control.Monad (forM, unless, when) +import qualified Data.IORef as IORef +import qualified Data.List as L +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV +import SAT.Solver.Mios.Types +import qualified SAT.Solver.Mios.Clause as C + +-- | resizable clause vector +class ClauseManager a where + newManager :: Int -> IO a + numberOfClauses :: a -> IO Int + clearManager :: a -> IO () + shrinkManager :: a -> Int -> IO () + getClauseVector :: a -> IO C.ClauseVector + pushClause :: a -> C.Clause -> IO () +-- removeClause :: a -> C.Clause -> IO () +-- removeNthClause :: a -> Int -> IO () + +{- +-- | The Clause Container +data SimpleManager = SimpleManager + { + _nActives :: IntSingleton -- number of active clause + , _clauseVector :: IORef.IORef C.ClauseVector -- clause list + } + +instance ClauseManager SimpleManager where + {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-} + newManager initialSize = do + i <- newInt 0 + v <- C.newClauseVector initialSize + SimpleManager i <$> IORef.newIORef v + {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-} + numberOfClauses SimpleManager{..} = getInt _nActives + {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-} + clearManager SimpleManager{..} = setInt _nActives 0 + {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-} + shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k) + {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-} + getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector + -- | O(1) inserter + {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-} + pushClause !SimpleManager{..} !c = do + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + if MV.length v - 1 <= n + then do + v' <- MV.unsafeGrow v (max 8 (MV.length v)) + -- forM_ [n .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause + MV.unsafeWrite v' n c + IORef.writeIORef _clauseVector v' + else MV.unsafeWrite v n c + modifyInt _nActives (1 +) + -- | O(1) remove-and-compact function + {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-} + removeNthClause SimpleManager{..} i = do + !n <- subtract 1 <$> getInt _nActives + !v <- IORef.readIORef _clauseVector + MV.unsafeWrite v i =<< MV.unsafeRead v n + setInt _nActives n + -- | O(n) but lightweight remove-and-compact function + -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. + {-# SPECIALIZE INLINE removeClause :: SimpleManager -> C.Clause -> IO () #-} + removeClause SimpleManager{..} c = do + -- putStrLn =<< dump "@removeClause| remove " c + -- putStrLn =<< dump "@removeClause| from " m + !n <- subtract 1 <$> getInt _nActives + -- unless (0 <= n) $ error $ "removeClause catches " ++ show n + !v <- IORef.readIORef _clauseVector + let + seekIndex :: Int -> IO Int + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then return k else seekIndex $ k + 1 + unless (n == -1) $ do + !i <- seekIndex 0 + MV.unsafeWrite v i =<< MV.unsafeRead v n + setInt _nActives n + +instance VectorFamily SimpleManager C.Clause where + dump mes SimpleManager{..} = do + n <- getInt _nActives + if n == 0 + then return $ mes ++ "empty clausemanager" + else do + l <- take n <$> (asList =<< IORef.readIORef _clauseVector) + sts <- mapM (dump ",") (l :: [C.Clause]) + return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) +-} + +-------------------------------------------------------------------------------- + +-- | Clause + Blocking Literal +data ClauseExtManager = ClauseExtManager + { + _nActives :: IntSingleton -- number of active clause + , _purged :: BoolSingleton -- whether it needs gc + , _clauseVector :: IORef.IORef C.ClauseVector -- clause list + , _keyVector :: IORef.IORef Vec -- Int list + } + +instance ClauseManager ClauseExtManager where + {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-} + newManager initialSize = do + i <- newInt 0 + v <- C.newClauseVector initialSize + b <- newVec (MV.length v) + ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b + {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-} + numberOfClauses ClauseExtManager{..} = getInt _nActives + {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-} + clearManager ClauseExtManager{..} = setInt _nActives 0 + {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-} + shrinkManager ClauseExtManager{..} k = modifyInt _nActives (subtract k) + {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-} + getClauseVector ClauseExtManager{..} = IORef.readIORef _clauseVector + -- | O(1) insertion function + {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-} + pushClause !ClauseExtManager{..} !c = do + -- checkConsistency m c + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + if MV.length v - 1 <= n + then do + let len = max 8 $ MV.length v + v' <- MV.unsafeGrow v len + b' <- vecGrow b len + MV.unsafeWrite v' n c + setNth b' n 0 + IORef.writeIORef _clauseVector v' + IORef.writeIORef _keyVector b' + else MV.unsafeWrite v n c >> setNth b n 0 + modifyInt _nActives (1 +) +{- + -- | O(n) but lightweight remove-and-compact function + -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. + {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-} + removeClause ClauseExtManager{..} c = do + !n <- subtract 1 <$> getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + let + seekIndex :: Int -> IO Int + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then return k else seekIndex $ k + 1 + unless (n == -1) $ do + !i <- seekIndex 0 + MV.unsafeWrite v i =<< MV.unsafeRead v n + setNth b i =<< getNth b n + setInt _nActives n + removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" +-} + +-- | sets the expire flag to a clause +{-# INLINE markClause #-} +markClause :: ClauseExtManager -> C.Clause -> IO () +markClause ClauseExtManager{..} c = do + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + let + seekIndex :: Int -> IO () + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1 + unless (n == 0) $ do + seekIndex 0 + setBool _purged True + +{-# INLINE purifyManager #-} +purifyManager :: ClauseExtManager -> IO () +purifyManager ClauseExtManager{..} = do + diry <- getBool _purged + when diry $ do + n <- getInt _nActives + vec <- IORef.readIORef _clauseVector + keys <- IORef.readIORef _keyVector + let + loop :: Int -> Int -> IO Int + loop ((< n) -> False) n' = return n' + loop i j = do + c <- C.getNthClause vec i + if c /= C.NullClause + then do + unless (i == j) $ do + C.setNthClause vec j c + setNth keys j =<< getNth keys i + loop (i + 1) (j + 1) + else loop (i + 1) j + setInt _nActives =<< loop 0 0 + setBool _purged False + +-- | returns the associated Int vector +{-# INLINE getKeyVector #-} +getKeyVector :: ClauseExtManager -> IO Vec +getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector + +-- | O(1) inserter +{-# INLINE pushClauseWithKey #-} +pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () +pushClauseWithKey !ClauseExtManager{..} !c k = do + -- checkConsistency m c + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + if MV.length v - 1 <= n + then do + let len = max 8 $ MV.length v + v' <- MV.unsafeGrow v len + b' <- vecGrow b len + MV.unsafeWrite v' n c + setNth b' n k + IORef.writeIORef _clauseVector v' + IORef.writeIORef _keyVector b' + else MV.unsafeWrite v n c >> setNth b n k + modifyInt _nActives (1 +) + +instance VectorFamily ClauseExtManager C.Clause where + dump mes ClauseExtManager{..} = do + n <- getInt _nActives + if n == 0 + then return $ mes ++ "empty ClauseExtManager" + else do + l <- take n <$> (asList =<< IORef.readIORef _clauseVector) + sts <- mapM (dump ",") (l :: [C.Clause]) + return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) + +-------------------------------------------------------------------------------- WatcherList + +-- | Vector of 'ClauseExtManager' +type WatcherList = V.Vector ClauseExtManager + +-- | /n/ is the number of 'Var', /m/ is default size of each watcher list +-- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector +newWatcherList :: Int -> Int -> IO WatcherList +newWatcherList n m = V.fromList <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m) + +-- | returns the watcher List :: "ClauseManager" for "Literal" /l/ +{-# INLINE getNthWatcher #-} +getNthWatcher :: WatcherList -> Lit-> ClauseExtManager +getNthWatcher = V.unsafeIndex + +instance VectorFamily WatcherList C.Clause where + dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) + +-- | purges all expirable clauses in 'WatcherList' +{-# INLINE garbageCollect #-} +garbageCollect :: WatcherList -> IO () +garbageCollect wm = V.mapM_ purifyManager wm + +numberOfRegisteredClauses :: WatcherList -> IO Int +numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws + +{- +-------------------------------------------------------------------------------- debugging stuff + +checkConsistency :: ClauseManager a => a -> C.Clause -> IO () +checkConsistency manager c = do + nc <- numberOfClauses manager + vec <- getClauseVector manager + let + loop :: Int -> IO () + loop i = do + when (i < nc) $ do + c' <- MV.unsafeRead vec i + when (c' == c) $ error "insert a clause to a ClauseMananger twice" + loop $ i + 1 + loop 0 + +checkClauseOrder :: ClauseManager a => a -> IO () +checkClauseOrder manager = do + putStr "checking..." + nc <- numberOfClauses manager + vec <- getClauseVector manager + let + nthActivity :: Int -> IO Double + nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i + report :: Int -> Int -> IO () + report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j) + loop :: Int -> Double -> IO () + loop i v = do + when (i < nc) $ do + c <- MV.unsafeRead vec i + a <- getDouble (C.activity c) + when (c == C.NullClause) $ error "null is included" + when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i)) + loop (i + 1) a + loop 0 =<< nthActivity 0 + putStrLn "done" +-} diff --git a/SAT/Solver/Mios/Data/Singleton.hs b/SAT/Solver/Mios/Data/Singleton.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Data/Singleton.hs @@ -0,0 +1,196 @@ +-- | A fast(est) mutable data +{-# LANGUAGE + BangPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Data.Singleton + ( + -- * Bool + BoolSingleton + , newBool + , getBool + , setBool + , modifyBool + -- * Int + , IntSingleton + , newInt + , getInt + , setInt + , modifyInt + -- * Double + , DoubleSingleton + , newDouble + , getDouble + , setDouble + , modifyDouble + ) + where +{- +---------------------------------------- +-- Implementation 1. :: IORef +---------------------------------------- + +import Data.IORef + +type BoolSingleton = IORef Bool + +newBool :: Bool -> IO BoolSingleton +newBool = newIORef + +{-# INLINE getBool #-} +getBool :: BoolSingleton -> IO Bool +getBool = readIORef + +{-# INLINE setBool #-} +setBool :: BoolSingleton -> Bool -> IO () +setBool = writeIORef + +{-# INLINE modifyBool #-} +modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () +modifyBool = modifyIORef' + +type IntSingleton = IORef Int + +newInt :: Int -> IO IntSingleton +newInt = newIORef + +{-# INLINE getInt #-} +getInt :: IntSingleton -> IO Int +getInt = readIORef + +{-# INLINE setInt #-} +setInt :: IntSingleton -> Int -> IO () +setInt = writeIORef + +{-# INLINE modifyInt #-} +modifyInt :: IntSingleton -> (Int -> Int) -> IO () +modifyInt = modifyIORef' + +type DoubleSingleton = IORef Double + +newDouble :: Double -> IO DoubleSingleton +newDouble = newIORef + +{-# INLINE getDouble #-} +getDouble :: DoubleSingleton -> IO Double +getDouble = readIORef + +{-# INLINE setDouble #-} +setDouble :: DoubleSingleton -> Double -> IO () +setDouble = writeIORef + +{-# INLINE modifyDouble #-} +modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () +modifyDouble = modifyIORef' +-} +{- +---------------------------------------- +-- Implementation 2. :: Data.Mutable.IOURef +---------------------------------------- + +import qualified Data.Mutable as M + +newtype IntSingleton = IntSingleton + { + mutableInt :: M.IOURef Int + } + +newInt :: IO IntSingleton +newInt = IntSingleton <$> M.newRef 0 + +{-# INLINE getInt #-} +getInt :: IntSingleton -> IO Int +getInt !(IntSingleton val) = M.readRef val + +{-# INLINE setInt #-} +setInt :: IntSingleton -> Int -> IO () +setInt !(IntSingleton val) !x = M.writeRef val x + +{-# INLINE modifyInt #-} +modifyInt :: IntSingleton -> (Int -> Int) -> IO () +modifyInt !(IntSingleton val) !f = M.modifyRef' val f +-} + +-- {- +---------------------------------------- +-- Implementation 3. :: Data.Vector.Unboxed.Mutable +---------------------------------------- + +import qualified Data.Vector.Unboxed.Mutable as UV + +-- | mutable Int +type IntSingleton = UV.IOVector Int + +-- | returns a new 'IntSingleton' +newInt :: Int -> IO IntSingleton +newInt k = do + s <- UV.new 1 + UV.unsafeWrite s 0 k + return s + +-- | returns the value +{-# INLINE getInt #-} +getInt :: IntSingleton -> IO Int +getInt val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setInt #-} +setInt :: IntSingleton -> Int -> IO () +setInt val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyInt #-} +modifyInt :: IntSingleton -> (Int -> Int) -> IO () +modifyInt val !f = UV.unsafeModify val f 0 + +-- | mutable Bool +type BoolSingleton = UV.IOVector Bool + +-- | returns a new 'BoolSingleton' +newBool :: Bool -> IO BoolSingleton +newBool b = do + s <- UV.new 1 + UV.unsafeWrite s 0 b + return s + +-- | returns the value +{-# INLINE getBool #-} +getBool :: BoolSingleton -> IO Bool +getBool val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setBool #-} +setBool :: BoolSingleton -> Bool -> IO () +setBool val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyBool #-} +modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () +modifyBool val !f = UV.unsafeModify val f 0 + +-- | mutable Double +type DoubleSingleton = UV.IOVector Double + +-- | returns a new 'DoubleSingleton' +newDouble :: Double -> IO DoubleSingleton +newDouble d = do + s <- UV.new 1 + UV.unsafeWrite s 0 d + return s + +-- | returns the value +{-# INLINE getDouble #-} +getDouble :: DoubleSingleton -> IO Double +getDouble val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setDouble #-} +setDouble :: DoubleSingleton -> Double -> IO () +setDouble val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyDouble #-} +modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () +modifyDouble val !f = UV.unsafeModify val f 0 +-- -} diff --git a/SAT/Solver/Mios/Data/Stack.hs b/SAT/Solver/Mios/Data/Stack.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Data/Stack.hs @@ -0,0 +1,93 @@ +-- | stack of Int, by adding the length field as the zero-th element to a 'Vec' +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Data.Stack + ( + Stack + , newStack + , clearStack + , sizeOfStack + , pushToStack + , popFromStack + , lastOfStack + , shrinkStack + , asSizedVec + , isoVec + ) + where + +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Solver.Mios.Types + +-- | Unboxed mutable stack for Int. +newtype Stack = Stack + { + ivec :: UV.IOVector Int + } + +instance VectorFamily Stack Int where + dump str v = (str ++) . show <$> asList v + {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-} + asVec (Stack v) = UV.unsafeTail v + asList (Stack v) = do + (n : l) <- asList v + return $ take n l + +-- | returns the number of elements +{-# INLINE sizeOfStack #-} +sizeOfStack :: Stack -> IO Int +sizeOfStack (Stack v) = UV.unsafeRead v 0 + +-- | clear stack +{-# INLINE clearStack #-} +clearStack :: Stack -> IO () +clearStack (Stack v) = UV.unsafeWrite v 0 0 + +-- | returns a new stack which size is @size@ +{-# INLINABLE newStack #-} +newStack :: Int -> IO Stack +newStack n = do + v <- UV.new $ n + 1 + UV.set v 0 + return $ Stack v + +-- | pushs an int to 'Stack' +{-# INLINE pushToStack #-} +pushToStack :: Stack -> Int -> IO () +pushToStack (Stack v) !x = do + !i <- (+ 1) <$> UV.unsafeRead v 0 + UV.unsafeWrite v i x + UV.unsafeWrite v 0 i + +-- | drops the first element from 'Stack' +{-# INLINE popFromStack #-} +popFromStack :: Stack -> IO () +popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0 + +-- | peeks the last element in 'Stack' +{-# INLINE lastOfStack #-} +lastOfStack :: Stack -> IO Int +lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0 + +-- | Shrink the stack. The given arg means the number of discards. +-- therefore, shrink s n == for [1 .. n] $ \_ -> pop s +{-# INLINE shrinkStack #-} +shrinkStack :: Stack -> Int -> IO () +shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0 + +-- | converts Stack to sized Vec; this is the method to get the internal vector +{-# INLINE asSizedVec #-} +asSizedVec :: Stack -> Vec +asSizedVec (Stack v) = v + +-- | isomorphic conversion to 'Vec' +-- +-- Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements +{-# INLINE isoVec #-} +isoVec :: Stack -> IO Vec +isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0 diff --git a/SAT/Solver/Mios/Data/Vec.hs b/SAT/Solver/Mios/Data/Vec.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Data/Vec.hs @@ -0,0 +1,86 @@ +-- | The fundamental data structure: Fixed Mutable Unboxed Int Vector +{-# LANGUAGE + BangPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Data.Vec + ( + Vec + , sizeOfVector + , getNth + , setNth + , swapBetween + , modifyNth + , setAll + , newVec + , newVecWith + , newSizedVecIntFromList + , newSizedVecIntFromUVector + , vecGrow + ) + where + +import qualified Data.Vector.Unboxed as U +import qualified Data.Vector.Unboxed.Mutable as UV + +-- | Costs of all operations are /O/(/1/) +type Vec = UV.IOVector Int + +-- | returns the size of 'Vec' +{-# INLINE sizeOfVector #-} +sizeOfVector :: Vec -> IO Int +sizeOfVector v = return $! UV.length v + +-- | returns a new 'Vec' +{-# INLINE newVec #-} +newVec :: Int -> IO Vec +newVec = UV.new + +-- | returns a new 'Vec' filled with an Int +{-# INLINE newVecWith #-} +newVecWith :: Int -> Int -> IO Vec +newVecWith n x = do + v <- UV.new n + UV.set v x + return v + +-- | gets the nth value +{-# INLINE getNth #-} +getNth :: Vec -> Int -> IO Int +getNth = UV.unsafeRead + +-- | sets the nth value +{-# INLINE setNth #-} +setNth :: Vec -> Int -> Int -> IO () +setNth = UV.unsafeWrite + +-- | modify the nth value +{-# INLINE modifyNth #-} +modifyNth :: Vec -> (Int -> Int) -> Int -> IO () +modifyNth = UV.unsafeModify + +-- | sets all elements +{-# INLINE setAll #-} +setAll :: Vec -> Int -> IO () +setAll = UV.set + +-- | swaps two elements +{-# INLINE swapBetween #-} +swapBetween:: Vec -> Int -> Int -> IO () +swapBetween = UV.unsafeSwap + +-- | returns a new 'Vec' from a @[Int]@ +{-# INLINE newSizedVecIntFromList #-} +newSizedVecIntFromList :: [Int] -> IO Vec +newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l) + +-- | returns a new 'Vec' from a Unboxed Int Vector +{-# INLINE newSizedVecIntFromUVector #-} +newSizedVecIntFromUVector :: U.Vector Int -> IO Vec +newSizedVecIntFromUVector = U.unsafeThaw + +-- | calls @unasfeGrow@ +{-# INLINE vecGrow #-} +vecGrow :: Vec -> Int -> IO Vec +vecGrow = UV.unsafeGrow diff --git a/SAT/Solver/Mios/Data/VecBool.hs b/SAT/Solver/Mios/Data/VecBool.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Data/VecBool.hs @@ -0,0 +1,55 @@ +-- | Mutable Unboxed Boolean Vector +-- +-- * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements +-- +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Data.VecBool + ( + VecBool + , newVecBool + , getNthBool + , setNthBool + , modifyNthBool + ) + where + +import Control.Monad (forM) +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Solver.Mios.Types (VectorFamily(..)) + +-- | Mutable unboxed Bool Vector +type VecBool = UV.IOVector Bool + +-- | provides 'clear' and 'size' +instance VectorFamily VecBool Bool where + clear _ = error "VecBool.clear" + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + +-- | returns a new 'VecBool' +newVecBool :: Int -> Bool -> IO VecBool +newVecBool n x = do + v <- UV.new n + UV.set v x + return v + +-- | returns the nth value in 'VecBool' +{-# INLINE getNthBool #-} +getNthBool :: VecBool -> Int -> IO Bool +getNthBool = UV.unsafeRead + +-- | sets the nth value +{-# INLINE setNthBool #-} +setNthBool :: VecBool -> Int -> Bool -> IO () +setNthBool = UV.unsafeWrite + +-- | sets the nth value +{-# INLINE modifyNthBool #-} +modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO () +modifyNthBool = UV.unsafeModify diff --git a/SAT/Solver/Mios/Data/VecDouble.hs b/SAT/Solver/Mios/Data/VecDouble.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Data/VecDouble.hs @@ -0,0 +1,53 @@ +-- | Mutable Unboxed Double Vector +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Data.VecDouble + ( + VecDouble + , newVecDouble + , getNthDouble + , setNthDouble + , modifyNthDouble + ) + where + +import Control.Monad (forM) +import Data.List () +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Solver.Mios.Types (VectorFamily(..)) + +-- | Mutable unboxed Double Vector +type VecDouble = UV.IOVector Double + +instance VectorFamily VecDouble Double where + clear _ = error "VecDouble.clear" + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + +-- | returns a new 'VecDouble' +newVecDouble :: Int -> Double -> IO VecDouble +newVecDouble n 0 = UV.new n +newVecDouble n x = do + v <- UV.new n + UV.set v x + return v + +-- | returns the nth value in 'VecDouble' +{-# INLINE getNthDouble #-} +getNthDouble :: Int -> VecDouble -> IO Double +getNthDouble !n v = UV.unsafeRead v n + +-- | sets the nth value +{-# INLINE setNthDouble #-} +setNthDouble :: Int -> VecDouble -> Double -> IO () +setNthDouble !n v !x = UV.unsafeWrite v n x + +-- | updates the nth value +{-# INLINE modifyNthDouble #-} +modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO () +modifyNthDouble !n v !f = UV.unsafeModify v f n diff --git a/SAT/Solver/Mios/Glucose.hs b/SAT/Solver/Mios/Glucose.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Glucose.hs @@ -0,0 +1,72 @@ +-- | This is a part of MIOS +{-# LANGUAGE + BangPatterns + , RecordWildCards + , ScopedTypeVariables + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Solver.Mios.Glucose + ( + computeLBD + , lbdOf + , setLBD + , updateLBD + , nextReduction + ) + where + +import Control.Monad (when) +import SAT.Solver.Mios.Types +import SAT.Solver.Mios.Clause +import SAT.Solver.Mios.Solver + +-- | returns the LBD vaule for 'Vec[1 ..]' +computeLBD :: Solver -> Vec -> IO Int +computeLBD Solver{..} vec = do + key <- (1 +) <$> getInt lbd'key + setInt lbd'key key + nv <- getNth vec 0 + let + loop :: Int -> Int -> IO Int + loop ((<= nv) -> False) n = return n + loop !i !n = do + l <- getNth level . lit2var =<< getNth vec i + seen <- if l == 0 then return True else (key ==) <$> getNth lbd'seen l + if seen + then loop (i + 1) n + else setNth lbd'seen l key >> loop (i + 1) (n + 1) + loop 1 0 + +-- | returns the LBD value of 'Clause' +{-# INLINE lbdOf #-} +lbdOf :: Solver -> Clause -> IO Int +lbdOf s (lits -> v) = computeLBD s v + +-- | update the LBD field in 'Clause' +{-# INLINE setLBD #-} +setLBD :: Solver -> Clause -> IO () +setLBD s c = setInt (lbd c) =<< lbdOf s c + +-- | update the lbd field of /c/ +{-# INLINE updateLBD #-} +updateLBD :: Solver -> Clause -> IO () +updateLBD _ NullClause = error "LBD71" +updateLBD _ (learnt -> False) = return () +updateLBD s c@Clause{..} = setInt lbd =<< lbdOf s c + +-- | 0 based +-- +-- >>> nextReduction 0 +-- 20000 +-- >>> nextReduction 1 +-- 40000 + 200 = 20000 + 20000 + 200 +-- >>> nextReduction 2 +-- 6000 + 600 = 20000 + 20200 + 20000 + 400 +-- >>> nextReduction 3 +-- 80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600 +-- +nextReduction :: Int -> Int -> Int +-- nextReduction _ n = 30000 + 10000 * n +nextReduction b n = b + 300 * n diff --git a/SAT/Solver/Mios/Internal.hs b/SAT/Solver/Mios/Internal.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Internal.hs @@ -0,0 +1,34 @@ +-- | Internal Settings +module SAT.Solver.Mios.Internal + ( + versionId + , MiosConfiguration (..) + , defaultConfiguration + , module Plumbing + ) + where +import SAT.Solver.Mios.Data.VecBool as Plumbing +import SAT.Solver.Mios.Data.VecDouble as Plumbing +import SAT.Solver.Mios.Data.Stack as Plumbing + +-- | version name +versionId :: String +versionId = "mios 1.2 " -- blocking literal + lbd + phase-saving + +-- | solver's parameters; random decision rate was dropped. +data MiosConfiguration = MiosConfiguration + { + variableDecayRate :: Double -- ^ decay rate for variable activity + , clauseDecayRate :: Double -- ^ decay rate for clause activity + , collectStats :: Bool -- ^ whether collect and report statistics + } + +-- | dafault configuration +-- +-- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@. +-- * Minisat-2.20 uses @(0.95, 0.999, 0)@. +-- * Gulcose-4.0 uses @(0.8 , 0.999, 0)@. +-- * Mios-1.2 uses @(0.95, 0.999, 0)@. +-- +defaultConfiguration :: MiosConfiguration +defaultConfiguration = MiosConfiguration 0.95 0.999 {- 0 -} False diff --git a/SAT/Solver/Mios/M114.hs b/SAT/Solver/Mios/M114.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/M114.hs @@ -0,0 +1,816 @@ +-- | This is a part of MIOS +{-# LANGUAGE + BangPatterns + , RecordWildCards + , ScopedTypeVariables + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Solver.Mios.M114 + ( + simplifyDB + , solve + ) + where + +import Control.Monad (forM_, unless, void, when) +import Data.Bits +import Data.Foldable (foldrM) +import SAT.Solver.Mios.Types +import SAT.Solver.Mios.Internal +import SAT.Solver.Mios.Clause +import SAT.Solver.Mios.ClauseManager +import SAT.Solver.Mios.Solver +import SAT.Solver.Mios.Glucose + +-- | #114: __RemoveWatch__ +{-# INLINABLE removeWatch #-} +removeWatch :: Solver -> Clause -> IO () +removeWatch Solver{..} c = do + let lvec = asVec c + l1 <- negateLit <$> getNth lvec 0 + markClause (getNthWatcher watches l1) c + l2 <- negateLit <$> getNth lvec 1 + markClause (getNthWatcher watches l2) c + +-------------------------------------------------------------------------------- +-- Operations on 'Clause' +-------------------------------------------------------------------------------- + +-- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists +-- This is a strippped-down version of 'newClause' in Solver +{-# INLINABLE newLearntClause #-} +newLearntClause :: Solver -> Vec -> IO () +newLearntClause s@Solver{..} ps = do + good <- getBool ok + when good $ do + -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals + -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause' + k <- getNth ps 0 + case k of + 1 -> do + l <- getNth ps 1 + unsafeEnqueue s l NullClause + _ -> do + -- allocate clause: + c <- newClauseFromVec True ps + let vec = asVec c + -- Pick a second literal to watch: + let + findMax :: Int -> Int -> Int -> IO Int + findMax ((< k) -> False) j _ = return j + findMax i j val = do + v' <- lit2var <$> getNth vec i + a <- getNth assigns v' + b <- getNth level v' + if (a /= lBottom) && (val < b) + then findMax (i + 1) i b + else findMax (i + 1) j val + swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level + -- Bump, enqueue, store clause: + claBumpActivity s c -- newly learnt clauses should be considered active + -- Add clause to all managers + pushClause learnts c + l <- getNth vec 0 + pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0 + l1 <- negateLit <$> getNth vec 1 + pushClauseWithKey (getNthWatcher watches l1) c 0 + -- update the solver state by @l@ + unsafeEnqueue s l c + -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue + setLBD s c + +-- | __Simplify.__ At the top-level, a constraint may be given the opportunity to +-- simplify its representation (returns @False@) or state that the constraint is +-- satisfied under the current assignment and can be removed (returns @True@). +-- A constraint must /not/ be simplifiable to produce unit information or to be +-- conflicting; in that case the propagation has not been correctly defined. +-- +-- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy. +{-# INLINABLE simplify #-} +simplify :: Solver -> Clause -> IO Bool +simplify s c = do + n <- sizeOfClause c + let + lvec = asVec c + loop ::Int -> IO Bool + loop ((< n) -> False) = return False + loop i = do + v <- valueLit s =<< getNth lvec i + if v == 1 then return True else loop (i + 1) + loop 0 + +-------------------------------------------------------------------------------- +-- MIOS NOTE on Minor methods: +-- +-- * no (meaningful) 'newVar' in mios +-- * 'assume' is defined in 'Solver' +-- * `cancelUntil` is defined in 'Solver' + +-------------------------------------------------------------------------------- +-- Major methods + +-- | M114: __Fig. 10. (p.15)__ +-- +-- analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel :: int&) -> [void] +-- +-- __Description:_- +-- Analzye confilct and produce a reason clause. +-- +-- __Pre-conditions:__ +-- * 'out_learnt' is assumed to be cleared. +-- * Corrent decision level must be greater than root level. +-- +-- __Post-conditions:__ +-- * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +-- * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +-- rest of literals. There may be others from the same level though. +-- +-- @analyze@ is invoked from @search@ +-- {-# INLINEABLE analyze #-} +analyze :: Solver -> Clause -> IO Int +analyze s@Solver{..} confl = do + -- litvec + clearStack litsLearnt + pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal + dl <- decisionLevel s + let + litsVec = asVec litsLearnt + trailVec = asVec trail + loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int + loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level + when (learnt c) $ do + claBumpActivity s c + -- update LBD like #Glucose4.0 + d <- getInt (lbd c) + when (2 < d) $ do + nblevels <- lbdOf s c + when (nblevels + 1 < d) $ do -- improve the LBD + when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause` + -- seems to be interesting: keep it fro the next round + setInt (lbd c) nblevels -- Update it + sc <- sizeOfClause c + let + lvec = asVec c + loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int) + loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC + loopOnLiterals j b pc = do + (q :: Lit) <- getNth lvec j + let v = lit2var q + sn <- getNth an'seen v + l <- getNth level v + if sn == 0 && 0 < l + then do + varBumpActivity s v + setNth an'seen v 1 + if dl <= l -- cancelUntil doesn't clear level of cancelled literals + then do + -- glucose heuristics + r <- getNthClause reason v + when (r /= NullClause && learnt r) $ pushToStack lastDL q + -- end of glucose heuristics + loopOnLiterals (j + 1) b (pc + 1) + else pushToStack litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc + else loopOnLiterals (j + 1) b pc + (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC + let + -- select next clause to look at + nextPickedUpLit :: Int -> IO Int + nextPickedUpLit i = do + x <- getNth an'seen . lit2var =<< getNth trailVec i + if x == 0 then nextPickedUpLit $ i - 1 else return i + ti' <- nextPickedUpLit ti + nextP <- getNth trailVec ti' + let nextV = lit2var nextP + confl' <- getNthClause reason nextV + setNth an'seen nextV 0 + if 1 < pathC' + then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1) + else setNth litsVec 0 (negateLit nextP) >> return b' + ti <- subtract 1 <$> sizeOfStack trail + levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0 + -- Simplify phase (implemented only @expensive_ccmin@ path) + n <- sizeOfStack litsLearnt + clearStack an'stack -- analyze_stack.clear(); + clearStack an'toClear -- out_learnt.copyTo(analyze_toclear); + pushToStack an'toClear =<< getNth litsVec 0 + let + merger :: Int -> Int -> IO Int + merger ((< n) -> False) b = return b + merger i b = do + l <- getNth litsVec i + pushToStack an'toClear l + -- restrict the search depth (range) to 32 + merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l) + levels <- merger 1 0 + let + loopOnLits :: Int -> Int -> IO () + loopOnLits ((< n) -> False) n' = shrinkStack litsLearnt $ n - n' + loopOnLits i j = do + l <- getNth litsVec i + c1 <- (NullClause ==) <$> getNthClause reason (lit2var l) + if c1 + then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) + else do + c2 <- not <$> analyzeRemovable s l levels + if c2 + then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) + else loopOnLits (i + 1) j + loopOnLits 1 1 -- the first literal is specail + -- glucose heuristics + nld <- sizeOfStack lastDL + lbd' <- computeLBD s $ asSizedVec litsLearnt -- this is not the right value + let + vec = asVec lastDL + loopOnLastDL :: Int -> IO () + loopOnLastDL ((< nld) -> False) = return () + loopOnLastDL i = do + v <- lit2var <$> getNth vec i + d' <- getInt . lbd =<< getNthClause reason v + when (lbd' < d') $ varBumpActivity s v + loopOnLastDL $ i + 1 + loopOnLastDL 0 + clearStack lastDL + -- Clear seen + k <- sizeOfStack an'toClear + let + vec' = asVec an'toClear + cleaner :: Int -> IO () + cleaner ((< k) -> False) = return () + cleaner i = do + v <- lit2var <$> getNth vec' i + setNth an'seen v 0 + cleaner $ i + 1 + cleaner 0 + return levelToReturn + +-- | #M114 +-- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is +-- visiting literals at levels that cannot be removed later. +-- +-- Implementation memo: +-- +-- * @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt'). +-- This is used only in this function and @analyze@. +-- +{-# INLINEABLE analyzeRemovable #-} +analyzeRemovable :: Solver -> Lit -> Int -> IO Bool +analyzeRemovable Solver{..} p minLevel = do + -- assert (reason[var(p)]!= NullCaulse); + clearStack an'stack -- analyze_stack.clear() + pushToStack an'stack p -- analyze_stack.push(p); + top <- sizeOfStack an'toClear + let + loopOnStack :: IO Bool + loopOnStack = do + k <- sizeOfStack an'stack -- int top = analyze_toclear.size(); + if 0 == k + then return True + else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL); + sl <- lastOfStack an'stack + popFromStack an'stack -- analyze_stack.pop(); + c <- getNthClause reason (lit2var sl) -- getRoot sl + nl <- sizeOfClause c + let + cvec = asVec c + loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){ + loopOnLit ((< nl) -> False) = loopOnStack + loopOnLit i = do + p' <- getNth cvec i -- valid range is [0 .. nl - 1] + let v' = lit2var p' + l' <- getNth level v' + c1 <- (1 /=) <$> getNth an'seen v' + if c1 && (0 /= l') -- if (!analyze_seen[var(p)] && level[var(p)] != 0){ + then do + c3 <- (NullClause /=) <$> getNthClause reason v' + if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){ + then do + setNth an'seen v' 1 -- analyze_seen[var(p)] = 1; + pushToStack an'stack p' -- analyze_stack.push(p); + pushToStack an'toClear p' -- analyze_toclear.push(p); + loopOnLit $ i + 1 + else do + -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0; + top' <- sizeOfStack an'toClear + let vec = asVec an'toClear + forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0 + -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop + shrinkStack an'toClear $ top' - top + return False + else loopOnLit $ i + 1 + loopOnLit 1 + loopOnStack + +-- | #114 +-- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void] +-- +-- __Description:__ +-- Specialized analysis proceduce to express the final conflict in terms of assumptions. +-- 'root_level' is allowed to point beyond end of trace (useful if called after conflict while +-- making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed +-- if conflict arose before search even started). +-- +analyzeFinal :: Solver -> Clause -> Bool -> IO () +analyzeFinal Solver{..} confl skipFirst = do + clearStack conflict + rl <- getInt rootLevel + unless (rl == 0) $ do + n <- sizeOfClause confl + let + lvec = asVec confl + loopOnConfl :: Int -> IO () + loopOnConfl ((< n) -> False) = return () + loopOnConfl i = do + (x :: Var) <- lit2var <$> getNth lvec i + lvl <- getNth level x + when (0 < lvl) $ setNth an'seen x 1 + loopOnConfl $ i + 1 + loopOnConfl $ if skipFirst then 1 else 0 + tls <- sizeOfStack trailLim + trs <- sizeOfStack trail + tlz <- getNth (asVec trailLim) 0 + let + trailVec = asVec trail + loopOnTrail :: Int -> IO () + loopOnTrail ((tlz <=) -> False) = return () + loopOnTrail i = do + (l :: Lit) <- getNth trailVec i + let (x :: Var) = lit2var l + saw <- getNth an'seen x + when (saw == 1) $ do + (r :: Clause) <- getNthClause reason x + if r == NullClause + then pushToStack conflict (negateLit l) + else do + k <- sizeOfClause r + let + cvec = asVec r + loopOnLits :: Int -> IO () + loopOnLits ((< k) -> False) = return () + loopOnLits j = do + (v :: Var) <- lit2var <$> getNth cvec j + lv <- getNth level v + when (0 < lv) $ setNth an'seen v 1 + loopOnLits $ i + 1 + loopOnLits 1 + setNth an'seen x 0 + loopOnTrail $ i - 1 + loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asVec trailLim) rl + +-- | M114: +-- propagate : [void] -> [Clause+] +-- +-- __Description:__ +-- Porpagates all enqueued facts. If a conflict arises, the cornflicting clause is returned. +-- otherwise CRef_undef. +-- +-- __Post-conditions:__ +-- * the propagation queue is empty, even if there was a conflict. +-- +-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve` +{-# INLINABLE propagate #-} +propagate :: Solver -> IO Clause +propagate s@Solver{..} = do + -- myVal <- getNth stats (fromEnum NumOfBackjump) + let +{- + myVal = 0 + bumpAllVar :: IO () -- not in use + bumpAllVar = do + let + loop :: Int -> IO () + loop ((<= nVars) -> False) = return () + loop i = do + c <- getNth pr'seen i + when (c == myVal) $ varBumpActivity s i + loop $ i + 1 + loop 1 +-} + trailVec = asVec trail + while :: Clause -> Bool -> IO Clause + while confl False = {- bumpAllVar >> -} return confl + while confl True = do + (p :: Lit) <- getNth trailVec =<< getInt qHead + modifyInt qHead (+ 1) + let (ws :: ClauseExtManager) = getNthWatcher watches p + end <- numberOfClauses ws + cvec <- getClauseVector ws + bvec <- getKeyVector ws +-- rc <- getNthClause reason $ lit2var p +-- byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False + let +{- + checkAllLiteralsIn :: Clause -> IO () -- not in use + checkAllLiteralsIn c = do + nc <- sizeOfClause c + let + vec = asVec c + loop :: Int -> IO () + loop((< nc) -> False) = return () + loop i = do + (v :: Var) <- lit2var <$> getNth vec i + setNth pr'seen v myVal + loop $ i + 1 + loop 0 +-} + forClause :: Clause -> Int -> Int -> IO Clause + forClause confl i@((< end) -> False) j = do + shrinkManager ws (i - j) + while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail) + forClause confl i j = do + (l :: Lit) <- getNth bvec i + bv <- if l == 0 then return lFalse else valueLit s l + if bv == lTrue + then do + unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec! + (c :: Clause) <- getNthClause cvec i + setNthClause cvec j c + setNth bvec j l + forClause confl (i + 1) (j + 1) + else do + -- checkAllLiteralsIn c + (c :: Clause) <- getNthClause cvec i + let + lits = asVec c + falseLit = negateLit p + -- Make sure the false literal is data[1] + ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1) + -- if 0th watch is true, then clause is already satisfied. + (first :: Lit) <- getNth lits 0 + val <- valueLit s first + if val == lTrue + then setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1) + else do + -- Look for new watch + cs <- sizeOfClause c + let + forLit :: Int -> IO Clause + forLit ((< cs) -> False) = do + -- Did not find watch; clause is unit under assignment: + setNthClause cvec j c + setNth bvec j 0 + result <- enqueue s first c + if not result + then do + ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False) + setInt qHead =<< sizeOfStack trail + -- Copy the remaining watches: + let + copy i'@((< end) -> False) j' = forClause c i' j' + copy i' j' = do + setNthClause cvec j' =<< getNthClause cvec i' + setNth bvec j' =<< getNth bvec i' + copy (i' + 1) (j' + 1) + copy (i + 1) (j + 1) + else forClause confl (i + 1) (j + 1) + forLit k = do + (l :: Lit) <- getNth lits k + lv <- valueLit s l + if lv /= lFalse + then do + swapBetween lits 1 k + pushClauseWithKey (getNthWatcher watches (negateLit l)) c l + forClause confl (i + 1) j + else forLit $ k + 1 + forLit 2 + forClause confl 0 0 + while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail) + +-- | #M22 +-- reduceDB: () -> [void] +-- +-- __Description:__ +-- Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked +-- clauses are clauses that are reason to some assignment. Binary clauses are never removed. +{-# INLINABLE reduceDB #-} +reduceDB :: Solver -> IO () +reduceDB s@Solver{..} = do + n <- nLearnts s + vec <- getClauseVector learnts + let + loop :: Int -> IO () + loop ((< n) -> False) = return () + loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1) + k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged + loop k -- CAVEAT: `vec` is a zero-based vector + garbageCollect watches + shrinkManager learnts (n - k) + +-- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses. +-- this function uses the same metrix as reduceDB_lt in glucose 4.0: +-- 1. binary clause +-- 2. smaller lbd +-- 3. larger activity defined in MiniSat +-- , where smaller value is better. +-- +-- they are coded into an Int as the following layout: +-- +-- * 14 bit: LBD or 0 for preserved clauses +-- * 19 bit: converted activity +-- * remain: clauseVector index +-- +(lbdWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1)) + where + w = finiteBitSize (0:: Int) + (l, a) = case () of + _ | 64 <= w -> (16, 19) -- 28 bit => 256M clauses + _ | 60 <= w -> (14, 19) -- 26 bit => 32M clauses + _ | 32 <= w -> ( 7, 6) -- 18 bit => 256K clauses + _ | 29 <= w -> ( 6, 5) -- 17 bit => 128K clauses + _ -> error "Int on your CPU doesn't have sufficient bit width." + +{-# INLINABLE sortClauses #-} +sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int +sortClauses s cm nneeds = do + -- constants + let + lbdMax :: Int + lbdMax = 2 ^ lbdWidth - 1 + activityMax :: Int + activityMax = 2 ^ activityWidth - 1 + activityScale :: Double + activityScale = fromIntegral activityMax + indexMax :: Int + indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26 + n <- numberOfClauses cm + when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity" + vec <- getClauseVector cm + keys <- getKeyVector cm + -- 1: assign keys + let + assignKey :: Int -> Int -> IO Int + assignKey ((< n) -> False) m = return m + assignKey i m = do + c <- getNthClause vec i + k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c + case k of + 1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1) + 2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) + _ -> do + l <- locked s c -- this is expensive + if l + then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) + else do + d <- getInt $ lbd c + b <- floor . (activityScale *) . (1 -) . logBase 1e100 . max 1 <$> getDouble (activity c) + setNth keys i $ shiftL (min lbdMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i + assignKey (i + 1) m + limit <- min n . (+ nneeds) <$> assignKey 0 0 + -- 2: sort keyVector + let + sortOnRange :: Int -> Int -> IO () + sortOnRange left right + | limit < left = return () + | left >= right = return () + | left + 1 == right = do + a <- getNth keys left + b <- getNth keys right + unless (a < b) $ swapBetween keys left right + | otherwise = do + let p = div (left + right) 2 + pivot <- getNth keys p + swapBetween keys p left -- set a sentinel for r' + let + nextL :: Int -> IO Int + nextL i@((<= right) -> False) = return i + nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i + nextR :: Int -> IO Int + -- nextR i@((left <=) -> False) = return i + nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i + divide :: Int -> Int -> IO Int + divide l r = do + l' <- nextL l + r' <- nextR r + if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r' + m <- divide (left + 1) right + swapBetween keys left m + sortOnRange left (m - 1) + sortOnRange (m + 1) right + sortOnRange 0 (n - 1) + -- 3: place clauses + let + seek :: Int -> IO () + seek ((< limit) -> False) = return () + seek i = do + bits <- getNth keys i + when (indexMax < bits) $ do + c <- getNthClause vec i + let + sweep k = do + k' <- (indexMax .&.) <$> getNth keys k + setNth keys k k + if k' == i + then setNthClause vec k c + else getNthClause vec k' >>= setNthClause vec k >> sweep k' + sweep i + seek $ i + 1 + seek 0 + return limit + +-- | #M22 +-- +-- simplify : [void] -> [bool] +-- +-- __Description:__ +-- Simplify the clause database according to the current top-level assigment. Currently, the only +-- thing done here is the removal of satisfied clauses, but more things can be put here. +-- +{-# INLINABLE simplifyDB #-} +simplifyDB :: Solver -> IO Bool +simplifyDB s@Solver{..} = do + good <- getBool ok + if good + then do + p <- propagate s + if p /= NullClause + then setBool ok False >> return False + else do + -- Clear watcher lists: + n <- sizeOfStack trail + let + vec = asVec trail + loopOnLit ((< n) -> False) = return () + loopOnLit i = do + l <- getNth vec i + clearManager . getNthWatcher watches $ l + clearManager . getNthWatcher watches $ negateLit l + loopOnLit $ i + 1 + loopOnLit 0 + -- Remove satisfied clauses: + let + for :: Int -> IO Bool + for ((< 2) -> False) = return True + for t = do + let ptr = if t == 0 then learnts else clauses + vec' <- getClauseVector ptr + n' <- numberOfClauses ptr + let + loopOnVector :: Int -> Int -> IO Bool + loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True + loopOnVector i j = do + c <- getNthClause vec' i + l <- locked s c + r <- simplify s c + if not l && r + then removeWatch s c >> loopOnVector (i + 1) j + else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1) + loopOnVector 0 0 + ret <- for 0 + garbageCollect watches + return ret + else return False + +-- | #M22 +-- +-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] +-- +-- __Description:__ +-- Search for a model the specified number of conflicts. +-- NOTE: Use negative value for 'nof_conflicts' indicate infinity. +-- +-- __Output:__ +-- 'l_True' if a partial assigment that is consistent with respect to the clause set is found. If +-- all variables are decision variables, that means that the clause set is satisfiable. 'l_False' +-- if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +{-# INLINABLE search #-} +search :: Solver -> Int -> Int -> IO LiftedBool +search s@Solver{..} nOfConflicts nOfLearnts = do + -- clear model + let + loop :: Int -> IO LiftedBool + loop conflictC = do + !confl <- propagate s + d <- decisionLevel s + if confl /= NullClause + then do + -- CONFLICT + incrementStat s NumOfBackjump 1 + r <- getInt rootLevel + if d == r + then do + -- Contradiction found: + analyzeFinal s confl False + return LFalse + else do +-- u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump) +-- when u $ do +-- d <- getDouble varDecay +-- when (d < 0.95) $ modifyDouble varDecay (+ 0.01) + backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself + (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel + newLearntClause s $ asSizedVec litsLearnt + k <- sizeOfStack litsLearnt + when (k == 1) $ do + (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0 + setNth level v 0 + varDecayActivity s + claDecayActivity s + loop $ conflictC + 1 + else do -- NO CONFLICT + -- Simplify the set of problem clauses: + when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here + k1 <- numberOfClauses learnts + k2 <- nAssigns s + when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses + case () of + _ | k2 == nVars -> do + -- Model found: + forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1) + return LTrue + _ | conflictC >= nOfConflicts -> do + -- Reached bound on number of conflicts + (s `cancelUntil`) =<< getInt rootLevel -- force a restart + incrementStat s NumOfRestart 1 + return Bottom + _ -> do + -- New variable decision: + v <- select s -- many have heuristic for polarity here + -- << #phasesaving + oldVal <- getNth phases v + unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@ + -- >> #phasesaving + loop conflictC + good <- getBool ok + if good then loop 0 else return LFalse + +-- | __Fig. 16. (p.20)__ +-- Main solve method. +-- +-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be +-- called right before using this method. If not, a top-level conflict (resulting in a +-- non-usable internal state) cannot be distinguished from a conflict under assumptions. +solve :: (Foldable t) => Solver -> t Lit -> IO Bool +solve s@Solver{..} assumps = do + -- PUSH INCREMENTAL ASSUMPTIONS: + let + injector :: Lit -> Bool -> IO Bool + injector _ False = return False + injector a True = do + b <- assume s a + if not b + then do -- conflict analyze + (confl :: Clause) <- getNthClause reason (lit2var a) + analyzeFinal s confl True + pushToStack conflict (negateLit a) + cancelUntil s 0 + return False + else do + confl <- propagate s + if confl /= NullClause + then do + analyzeFinal s confl True + cancelUntil s 0 + return False + else return True + good <- simplifyDB s + x <- if good then foldrM injector True assumps else return False + if not x + then return False + else do + setInt rootLevel =<< decisionLevel s + -- SOLVE: + nc <- fromIntegral <$> nClauses s + let + while :: Double -> Double -> IO Bool + while nOfConflicts nOfLearnts = do + status <- search s (floor nOfConflicts) (floor nOfLearnts) + if status == Bottom + then while (1.5 * nOfConflicts) (1.1 * nOfLearnts) + else cancelUntil s 0 >> return (status == LTrue) + while 100 (nc / 3.0) + + +-- +-- 'enqueue' is defined in 'Solver'; functions in M114 use 'unsafeEnqueue' +-- +{-# INLINABLE unsafeEnqueue #-} +unsafeEnqueue :: Solver -> Lit -> Clause -> IO () +unsafeEnqueue s@Solver{..} p from = do + let v = lit2var p + setNth assigns v $! if positiveLit p then lTrue else lFalse + setNth level v =<< decisionLevel s + setNthClause reason v from -- NOTE: @from@ might be NULL! + pushToStack trail p + +-- __Pre-condition:__ propagation queue is empty +{-# INLINE unsafeAssume #-} +unsafeAssume :: Solver -> Lit -> IO () +unsafeAssume s@Solver{..} p = do + pushToStack trailLim =<< sizeOfStack trail + unsafeEnqueue s p NullClause + +{- +-- | for debug +fromAssigns :: Vec -> IO [Int] +fromAssigns as = zipWith f [1 .. ] . tail <$> asList as + where + f n x + | x == lTrue = n + | x == lFalse = negate n + | otherwise = 0 + +-- | for debug +dumpAssignment :: String -> Vec -> IO String +dumpAssignment mes v = (mes ++) . show <$> fromAssigns v +-} diff --git a/SAT/Solver/Mios/OptionParser.hs b/SAT/Solver/Mios/OptionParser.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/OptionParser.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE Safe #-} +-- | command line option parser for mios +module SAT.Solver.Mios.OptionParser + ( + MiosConfiguration (..) + , defaultConfiguration + , MiosProgramOption (..) + , miosDefaultOption + , miosOptions + , miosUsage + , miosParseOptions + , miosParseOptionsFromArgs + , toMiosConf + ) + where + +import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) +import System.Environment (getArgs) +import SAT.Solver.Mios.Internal (MiosConfiguration (..), defaultConfiguration) + +-- | configuration swithces +data MiosProgramOption = MiosProgramOption + { + _targetFile :: Maybe String + , _outputFile :: Maybe String + , _confVariableDecayRate :: Double + , _confClauseDecayRate :: Double +-- , _confRandomDecisionRate :: Int + , _confCheckAnswer :: Bool + , _confVerbose :: Bool + , _confTimeProbe :: Bool + , _confStatProbe :: Bool + , _confNoAnswer :: Bool + , _validateAssignment :: Bool + , _displayHelp :: Bool + , _displayVersion :: Bool + } + +-- | default option settings +miosDefaultOption :: MiosProgramOption +miosDefaultOption = MiosProgramOption + { + _targetFile = Just "" + , _outputFile = Nothing + , _confVariableDecayRate = variableDecayRate defaultConfiguration + , _confClauseDecayRate = clauseDecayRate defaultConfiguration +-- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration + , _confCheckAnswer = False + , _confVerbose = False + , _confTimeProbe = False + , _confStatProbe = collectStats defaultConfiguration + , _confNoAnswer = False + , _validateAssignment = False + , _displayHelp = False + , _displayVersion = False + } + +-- | definition of mios option +miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)] +miosOptions = + [ + Option ['d'] ["variable-decay-rate"] + (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption))) + "[solver] variable activity decay rate (0.0 - 1.0)" + , Option ['c'] ["clause-decay-rate"] + (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption))) + "[solver] clause activity decay rate (0.0 - 1.0)" +-- , Option ['r'] ["random-decision-rate"] +-- (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption))) +-- "[solver] random selection rate (0 - 1000)" + , Option [':'] ["validate-assignment"] + (NoArg (\c -> c { _validateAssignment = True })) + "[solver] read an assignment from STDIN and validate it" + , Option [] ["validate"] + (NoArg (\c -> c { _confCheckAnswer = True })) + "[solver] self-check the (satisfied) answer" + , Option ['o'] ["output"] + (ReqArg (\v c -> c { _outputFile = Just v })"file") + "[option] filename to store the result" +{- + , Option [] ["stdin"] + (NoArg (\c -> c { _targetFile = Nothing })) + "[option] read a CNF from STDIN instead of a file" +-} + , Option ['v'] ["verbose"] + (NoArg (\c -> c { _confVerbose = True })) + "[option] display misc information" + , Option ['X'] ["hide-solution"] + (NoArg (\c -> c { _confNoAnswer = True })) + "[option] hide the solution" + , Option [] ["time"] + (NoArg (\c -> c { _confTimeProbe = True })) + "[option] display execution time" + , Option [] ["stat"] + (NoArg (\c -> c { _confStatProbe = True })) + "[option] display statistics information" + , Option ['h'] ["help"] + (NoArg (\c -> c { _displayHelp = True })) + "[misc] display this help message" + , Option [] ["version"] + (NoArg (\c -> c { _displayVersion = True })) + "[misc] display program ID" + ] + +-- | generates help message +miosUsage :: String -> String +miosUsage mes = usageInfo mes miosOptions + +-- | builds "MiosProgramOption" from string given as command option +miosParseOptions :: String -> [String] -> IO MiosProgramOption +miosParseOptions mes argv = + case getOpt Permute miosOptions argv of + (o, [], []) -> do + return $ foldl (flip id) miosDefaultOption o + (o, (n:_), []) -> do + let conf = foldl (flip id) miosDefaultOption o + return $ conf { _targetFile = Just n } + (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes)) + +-- | builds "MiosProgramOption" from a String +miosParseOptionsFromArgs :: String -> IO MiosProgramOption +miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs + +-- | converts "MiosProgramOption" into "SIHConfiguration" +toMiosConf :: MiosProgramOption -> MiosConfiguration +toMiosConf opts = MiosConfiguration + { + variableDecayRate = _confVariableDecayRate opts + , clauseDecayRate = _confClauseDecayRate opts +-- , randomDecisionRate = _confRandomDecisionRate opts + , collectStats = _confStatProbe opts + } diff --git a/SAT/Solver/Mios/Solver.hs b/SAT/Solver/Mios/Solver.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Solver.hs @@ -0,0 +1,554 @@ +-- | This is a part of MIOS +{-# LANGUAGE + BangPatterns + , RecordWildCards + , ScopedTypeVariables + , TupleSections + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Solver.Mios.Solver + ( + -- * Solver + Solver (..) + , newSolver + -- * Misc Accessors + , nAssigns + , nClauses + , nLearnts + , decisionLevel + , valueVar + , valueLit + , locked + , VarHeap + -- * State Modifiers + , addClause + , enqueue + , assume + , cancelUntil + , getModel + -- * Activities + , claBumpActivity + , claDecayActivity + , varBumpActivity + , varDecayActivity + -- * Stats + , StatIndex (..) + , incrementStat + , getStats + ) + where + +import Control.Monad ((<=<), forM_, unless, when) +import SAT.Solver.Mios.Types +import SAT.Solver.Mios.Internal +import SAT.Solver.Mios.Clause +import SAT.Solver.Mios.ClauseManager + +-- | __Fig. 2.(p.9)__ Internal State of the solver +data Solver = Solver + { + -- Public Interface + model :: !VecBool -- ^ If found, this vector has the model + , conflict :: !Stack -- ^ set of literals in the case of conflicts + -- Clause Database + , clauses :: !ClauseExtManager -- ^ List of problem constraints. + , learnts :: !ClauseExtManager -- ^ List of learnt clauses. + , watches :: !WatcherList -- ^ a list of constraint wathing 'p', literal-indexed + -- Assignment Management + , assigns :: !Vec -- ^ The current assignments indexed on variables; var-indexed + , phases :: !Vec -- ^ The last assignments indexed on variables; var-indexed + , trail :: !Stack -- ^ List of assignments in chronological order; var-indexed + , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'. + , qHead :: !IntSingleton -- ^ 'trail' is divided at qHead; assignments and queue + , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value; var-indexed + , level :: !Vec -- ^ For each variable, the decision level it was assigned; var-indexed + -- Variable Order + , activities :: !VecDouble -- ^ Heuristic measurement of the activity of a variable; var-indexed + , order :: !VarHeap -- ^ Keeps track of the dynamic variable order. + -- Configuration + , config :: !MiosConfiguration -- ^ search paramerters + , nVars :: !Int -- ^ number of variables + , claInc :: !DoubleSingleton -- ^ Clause activity increment amount to bump with. +-- , varDecay :: !DoubleSingleton -- ^ used to set 'varInc' + , varInc :: !DoubleSingleton -- ^ Variable activity increment amount to bump with. + , rootLevel :: !IntSingleton -- ^ Separates incremental and search assumptions. + -- Working Memory + , ok :: !BoolSingleton -- ^ return value holder + , an'seen :: !Vec -- ^ scratch var for 'analyze'; var-indexed + , an'toClear :: !Stack -- ^ ditto + , an'stack :: !Stack -- ^ ditto + , pr'seen :: !Vec -- ^ used in propagate + , lbd'seen :: !Vec -- ^ used in lbd computation + , lbd'key :: !IntSingleton -- ^ used in lbd computation + , litsLearnt :: !Stack -- ^ used to create a learnt clause + , lastDL :: !Stack -- ^ last decision level used in analyze + , stats :: !Vec -- ^ statistics information holder + } + +-- | returns an everything-is-initialized solver from the arguments +newSolver :: MiosConfiguration -> CNFDescription -> IO Solver +newSolver conf (CNFDescription nv nc _) = do + Solver + -- Public Interface + <$> newVecBool nv False -- model + <*> newStack nv -- coflict + -- Clause Database + <*> newManager nc -- clauses + <*> newManager nc -- learnts + <*> newWatcherList nv 2 -- watches + -- Assignment Management + <*> newVecWith (nv + 1) lBottom -- assigns + <*> newVecWith (nv + 1) lBottom -- phases + <*> newStack nv -- trail + <*> newStack nv -- trailLim + <*> newInt 0 -- qHead + <*> newClauseVector (nv + 1) -- reason + <*> newVecWith (nv + 1) (-1) -- level + -- Variable Order + <*> newVecDouble (nv + 1) 0 -- activities + <*> newVarHeap nv -- order + -- Configuration + <*> return conf -- config + <*> return nv -- nVars + <*> newDouble 1.0 -- claInc +-- <*> newDouble (variableDecayRate conf) -- varDecay + <*> newDouble 1.0 -- varInc + <*> newInt 0 -- rootLevel + -- Working Memory + <*> newBool True -- ok + <*> newVec (nv + 1) -- an'seen + <*> newStack nv -- an'toClear + <*> newStack nv -- an'stack + <*> newVecWith (nv + 1) (-1) -- pr'seen + <*> newVec nv -- lbd'seen + <*> newInt 0 -- lbd'key + <*> newStack nv -- litsLearnt + <*> newStack nv -- lastDL + <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats + +-------------------------------------------------------------------------------- +-- Accessors + +-- | returns the number of current assigments +{-# INLINE nAssigns #-} +nAssigns :: Solver -> IO Int +nAssigns = sizeOfStack . trail + +-- | returns the number of constraints (clauses) +{-# INLINE nClauses #-} +nClauses :: Solver -> IO Int +nClauses = numberOfClauses . clauses + +-- | returns the number of learnt clauses +{-# INLINE nLearnts #-} +nLearnts :: Solver -> IO Int +nLearnts = numberOfClauses . learnts + +-- | return the model as a list of literal +getModel :: Solver -> IO [Int] +getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s) + +-- | returns the current decision level +{-# INLINE decisionLevel #-} +decisionLevel :: Solver -> IO Int +decisionLevel Solver{..} = sizeOfStack trailLim + +-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var' +{-# INLINE valueVar #-} +valueVar :: Solver -> Var -> IO Int +valueVar s !x = getNth (assigns s) x + +-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' +{-# INLINE valueLit #-} +valueLit :: Solver -> Lit -> IO Int -- FIXME: LiftedBool +valueLit Solver{..} !p = if positiveLit p then getNth assigns (lit2var p) else negate <$> getNth assigns (lit2var p) + +-- | __Fig. 7. (p.11)__ +-- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__ +{-# INLINE locked #-} +locked :: Solver -> Clause -> IO Bool +locked Solver{..} c@Clause{..} = (c ==) <$> (getNthClause reason . lit2var =<< getNth lits 1) + +-- | stats +data StatIndex = + NumOfBackjump + | NumOfRestart + deriving (Bounded, Enum, Eq, Ord, Read, Show) + +-- | increments a stat data corresponding to 'StatIndex' +incrementStat :: Solver -> StatIndex -> Int -> IO () +incrementStat (config -> collectStats -> False) _ _ = return () +incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i + +-- | returns the statistics as list +getStats :: Solver -> IO [(StatIndex, Int)] +getStats (config -> collectStats -> False) = return [] +getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex] + +-------------------------------------------------------------------------------- State Modifiers + +-- | returns @False@ if a conflict has occured. +-- This function is called only before the solving phase to register the given clauses. +{-# INLINABLE addClause #-} +addClause :: Solver -> Vec -> IO Bool +addClause s@Solver{..} vecLits = do + result <- clauseNew s vecLits False + case result of + (False, _) -> return False -- Conflict occured + (True, c) -> do + unless (c == NullClause) $ pushClause clauses c + return True -- No conflict + +-- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists +-- Constructor function for clauses. Returns @False@ if top-level conflict is determined. +-- @outClause@ may be set to Null if the new clause is already satisfied under the current +-- top-level assignment. +-- +-- __Post-condition:__ @ps@ is cleared. For learnt clauses, all +-- literals will be false except @lits[0]@ (this by design of the 'analyze' method). +-- For the propagation to work, the second watch must be put on the literal which will +-- first be unbound by backtracking. (Note that none of the learnt-clause specific things +-- needs to done for a user defined contraint type.) +{-# INLINABLE clauseNew #-} +clauseNew :: Solver -> Vec -> Bool -> IO (Bool, Clause) +clauseNew s@Solver{..} ps isLearnt = do + -- now ps[0] is the number of living literals + exit <- do + let + handle :: Int -> Int -> Int -> IO Bool + handle j l n -- removes duplicates, but returns @True@ if this clause is satisfied + | j > n = return False + | otherwise = do + y <- getNth ps j + case () of + _ | y == l -> do -- finds a duplicate + swapBetween ps j n + modifyNth ps (subtract 1) 0 + handle j l (n - 1) + _ | - y == l -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps + _ -> handle (j + 1) l n + loopForLearnt :: Int -> IO Bool + loopForLearnt i = do + n <- getNth ps 0 + if n < i + then return False + else do + l <- getNth ps i + sat <- handle (i + 1) l n + if sat + then return True + else loopForLearnt $ i + 1 + loop :: Int -> IO Bool + loop i = do + n <- getNth ps 0 + if n < i + then return False + else do + l <- getNth ps i -- check the i-th literal's satisfiability + sat <- valueLit s l -- any literal in ps is true + case sat of + 1 -> setNth ps 0 0 >> return True + -1 -> do + swapBetween ps i n + modifyNth ps (subtract 1) 0 + loop i + _ -> do + sat' <- handle (i + 1) l n + if sat' + then return True + else loop $ i + 1 + if isLearnt then loopForLearnt 1 else loop 1 + k <- getNth ps 0 + case k of + 0 -> return (exit, NullClause) + 1 -> do + l <- getNth ps 1 + (, NullClause) <$> enqueue s l NullClause + _ -> do + -- allocate clause: + c <- newClauseFromVec isLearnt ps + let vec = asVec c + when isLearnt $ do + -- Pick a second literal to watch: + let + findMax :: Int -> Int -> Int -> IO Int + findMax ((< k) -> False) j _ = return j + findMax i j val = do + v' <- lit2var <$> getNth vec i + a <- getNth assigns v' + b <- getNth level v' + if (a /= lBottom) && (val < b) + then findMax (i + 1) i b + else findMax (i + 1) j val + -- Let @max_i@ be the index of the literal with highest decision level + max_i <- findMax 0 0 0 + swapBetween vec 1 max_i + -- check literals occurences + -- x <- asList c + -- unless (length x == length (nub x)) $ error "new clause contains a element doubly" + -- Bumping: + claBumpActivity s c -- newly learnt clauses should be considered active + forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped + -- Add clause to watcher lists: + l0 <- negateLit <$> getNth vec 0 + pushClauseWithKey (getNthWatcher watches l0) c 0 + l1 <- negateLit <$> getNth vec 1 + pushClauseWithKey (getNthWatcher watches l1) c 0 + return (True, c) + +-- | __Fig. 9 (p.14)__ +-- Puts a new fact on the propagation queue, as well as immediately updating the variable's value +-- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is +-- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was +-- propagated (defaults to @Nothing@ if omitted). +{-# INLINABLE enqueue #-} +enqueue :: Solver -> Lit -> Clause -> IO Bool +enqueue s@Solver{..} p from = do + -- putStrLn . ("ssigns " ++) . show . map lit2int =<< asList trail + -- putStrLn =<< dump ("enqueue " ++ show (lit2int p) ++ " ") from + let signumP = if positiveLit p then lTrue else lFalse + let v = lit2var p + val <- valueVar s v + if val /= lBottom + then do -- Existing consistent assignment -- don't enqueue + return $ val == signumP + else do + -- New fact, store it + setNth assigns v $! signumP + setNth level v =<< decisionLevel s + setNthClause reason v from -- NOTE: @from@ might be NULL! + pushToStack trail p + return True + +-- | __Fig. 12 (p.17)__ +-- returns @False@ if immediate conflict. +-- +-- __Pre-condition:__ propagation queue is empty +{-# INLINE assume #-} +assume :: Solver -> Lit -> IO Bool +assume s@Solver{..} p = do + pushToStack trailLim =<< sizeOfStack trail + enqueue s p NullClause + +-- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond). +{-# INLINABLE cancelUntil #-} +cancelUntil :: Solver -> Int -> IO () +cancelUntil s@Solver{..} lvl = do + dl <- decisionLevel s + when (lvl < dl) $ do + let tr = asVec trail + let tl = asVec trailLim + lim <- getNth tl lvl + ts <- sizeOfStack trail + ls <- sizeOfStack trailLim + let + loopOnTrail :: Int -> IO () + loopOnTrail ((lim <=) -> False) = return () + loopOnTrail c = do + x <- lit2var <$> getNth tr c + setNth phases x =<< getNth assigns x + setNth assigns x lBottom + -- #reason to set reason Null + -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked. + -- This means we can't reduce it from clause DB and affects the performance. + setNthClause reason x NullClause -- 'analyze` uses reason without checking assigns + -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212 + undo s x + -- insertHeap s x -- insertVerOrder + loopOnTrail $ c - 1 + loopOnTrail $ ts - 1 + shrinkStack trail (ts - lim) + shrinkStack trailLim (ls - lvl) + setInt qHead =<< sizeOfStack trail + +-------------------------------------------------------------------------------- VarOrder + +-- | Interfate to select a decision var based on variable activity. +instance VarOrder Solver where + -- | __Fig. 6. (p.10)__ + -- Creates a new SAT variable in the solver. + newVar _ = return 0 + -- i <- nVars s + -- Version 0.4:: push watches =<< newVec -- push' + -- Version 0.4:: push watches =<< newVec -- push' + -- push undos =<< newVec -- push' + -- push reason NullClause -- push' + -- push assigns lBottom + -- push level (-1) + -- push activities (0.0 :: Double) + -- newVar order + -- growQueueSized (i + 1) propQ + -- return i + {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-} + update = increaseHeap + {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-} + undo s v = inHeap s v >>= (`unless` insertHeap s v) + {-# SPECIALIZE INLINE select :: Solver -> IO Var #-} + select s = do + let + asg = assigns s + -- | returns the most active var (heap-based implementation) + loop :: IO Var + loop = do + n <- numElementsInHeap s + if n == 0 + then return 0 + else do + v <- getHeapRoot s + x <- getNth asg v + if x == lBottom then return v else loop + loop + +-------------------------------------------------------------------------------- Activities + +-- | __Fig. 14 (p.19)__ Bumping of clause activity +{-# INLINE varBumpActivity #-} +varBumpActivity :: Solver -> Var -> IO () +varBumpActivity s@Solver{..} !x = do + !a <- (+) <$> getNthDouble x activities <*> getDouble varInc + if 1e100 < a + then varRescaleActivity s + else setNthDouble x activities a + update s x + +-- | __Fig. 14 (p.19)__ +{-# INLINE varDecayActivity #-} +varDecayActivity :: Solver -> IO () +varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config) +-- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay + +-- | __Fig. 14 (p.19)__ +{-# INLINE varRescaleActivity #-} +varRescaleActivity :: Solver -> IO () +varRescaleActivity Solver{..} = do + forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (* 1e-100) + modifyDouble varInc (* 1e-100) + +-- | __Fig. 14 (p.19)__ +{-# INLINE claBumpActivity #-} +claBumpActivity :: Solver -> Clause -> IO () +claBumpActivity s@Solver{..} Clause{..} = do + a <- (+) <$> getDouble activity <*> getDouble claInc + if 1e100 < a + then claRescaleActivity s + else setDouble activity a + +-- | __Fig. 14 (p.19)__ +{-# INLINE claDecayActivity #-} +claDecayActivity :: Solver -> IO () +claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config) + +-- | __Fig. 14 (p.19)__ +{-# INLINE claRescaleActivity #-} +claRescaleActivity :: Solver -> IO () +claRescaleActivity Solver{..} = do + vec <- getClauseVector learnts + n <- numberOfClauses learnts + let + loopOnVector :: Int -> IO () + loopOnVector ((< n) -> False) = return () + loopOnVector i = do + c <- getNthClause vec i + modifyDouble (activity c) (* 1e-20) -- not 1e-100 + loopOnVector $ i + 1 + loopOnVector 0 + modifyDouble claInc (* 1e-20) -- not 1e-100 + +-------------------------------------------------------------------------------- VarHeap + +-- | 'VarHeap' is a heap tree built from two 'Vec' +-- This implementation is identical wtih that in Minisat-1.14 +-- Note: the zero-th element of @heap@ is used for holding the number of elements +-- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver +data VarHeap = VarHeap + { + heap :: Vec -- order to var + , idxs :: Vec -- var to order (index) + } + +newVarHeap :: Int -> IO VarHeap +newVarHeap n = VarHeap <$> newSizedVecIntFromList lst <*> newSizedVecIntFromList lst + where + lst = [1 .. n] + +{-# INLINE numElementsInHeap #-} +numElementsInHeap :: Solver -> IO Int +numElementsInHeap (order -> heap -> h) = getNth h 0 + +{-# INLINE inHeap #-} +inHeap :: Solver -> Var -> IO Bool +inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n + +{-# INLINE increaseHeap #-} +increaseHeap :: Solver -> Int -> IO () +increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n)) + +{-# INLINABLE percolateUp #-} +percolateUp :: Solver -> Int -> IO () +percolateUp Solver{..} start = do + let VarHeap to at = order + v <- getNth to start + ac <- getNthDouble v activities + let + loop :: Int -> IO () + loop i = do + let iP = div i 2 -- parent + if iP == 0 + then setNth to i v >> setNth at v i -- end + else do + v' <- getNth to iP + acP <- getNthDouble v' activities + if ac > acP + then setNth to i v' >> setNth at v' i >> loop iP -- loop + else setNth to i v >> setNth at v i -- end + loop start + +{-# INLINABLE percolateDown #-} +percolateDown :: Solver -> Int -> IO () +percolateDown Solver{..} start = do + let (VarHeap to at) = order + n <- getNth to 0 + v <- getNth to start + ac <- getNthDouble v activities + let + loop :: Int -> IO () + loop i = do + let iL = 2 * i -- left + if iL <= n + then do + let iR = iL + 1 -- right + l <- getNth to iL + r <- getNth to iR + acL <- getNthDouble l activities + acR <- getNthDouble r activities + let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL) + if ac' > ac + then setNth to i child >> setNth at child i >> loop ci + else setNth to i v >> setNth at v i -- end + else setNth to i v >> setNth at v i -- end + loop start + +{-# INLINE insertHeap #-} +insertHeap :: Solver -> Var -> IO () +insertHeap s@(order -> VarHeap to at) v = do + n <- (1 +) <$> getNth to 0 + setNth at v n + setNth to n v + setNth to 0 n + percolateUp s n + +-- | renamed from 'getmin' +{-# INLINE getHeapRoot #-} +getHeapRoot :: Solver -> IO Int +getHeapRoot s@(order -> VarHeap to at) = do + r <- getNth to 1 + l <- getNth to =<< getNth to 0 -- the last element's value + setNth to 1 l + setNth at l 1 + setNth at r 0 + modifyNth to (subtract 1) 0 -- pop + n <- getNth to 0 + when (1 < n) $ percolateDown s 1 + return r diff --git a/SAT/Solver/Mios/Types.hs b/SAT/Solver/Mios/Types.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Types.hs @@ -0,0 +1,269 @@ +-- | Basic data types used throughout mios. +{-# LANGUAGE + BangPatterns + , FlexibleContexts + , FlexibleInstances + , FunctionalDependencies + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Solver.Mios.Types + ( + -- Singleton + module SAT.Solver.Mios.Data.Singleton + -- Fixed Unboxed Mutable Int Vector + , module SAT.Solver.Mios.Data.Vec + -- Abstract interfaces + , VectorFamily (..) + -- * Variable + , Var + , bottomVar + , int2var + -- * Internal encoded Literal + , Lit + , lit2int + , int2lit + , bottomLit + , newLit + , positiveLit + , lit2var + , var2lit + , negateLit + -- * Assignment + , LiftedBool (..) + , lbool + , lFalse + , lTrue + , lBottom + , VarOrder (..) + -- * CNF + , CNFDescription (..) + ) + where + +import Control.Monad (forM) +import Data.Bits +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Solver.Mios.Data.Singleton +import SAT.Solver.Mios.Data.Vec + +-- | Public interface as /Container/ +class VectorFamily s t | s -> t where + -- * Size operations + -- | erases all elements in it + clear :: s -> IO () + clear = error "no default method for clear" + -- * Debug + -- | dump the contents + dump :: Show t => String -> s -> IO String + dump msg _ = error $ msg ++ ": no defalut method for dump" + -- | get a raw data + asVec :: s -> UV.IOVector Int + asVec = error "asVector undefined" + -- | converts into a list + asList :: s -> IO [t] + asList = error "asList undefined" + {-# MINIMAL dump #-} + +-- | provides 'clear' and 'size' +instance VectorFamily Vec Int where + clear = error "Vec.clear" + {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-} + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-} + asVec = id + +-- | represents "Var" +type Var = Int + +-- | Special constant in 'Var' (p.7) +bottomVar :: Var +bottomVar = 0 + +-- | converts a usual Int as literal to an internal 'Var' presentation +-- +-- >>> int2var 1 +-- 1 -- the first literal is the first variable +-- >>> int2var 2 +-- 2 -- literal @2@ is variable 2 +-- >>> int2var (-2) +-- 2 -- literal @-2@ is corresponding to variable 2 +-- +{-# INLINE int2var #-} +int2var = abs + +-- | The literal data has an 'index' method which converts the literal to +-- a "small" integer suitable for array indexing. The 'var' method returns +-- the underlying variable of the literal, and the 'sign' method if the literal +-- is signed (False for /x/ and True for /-x/). +type Lit = Int + +-- | Special constant in 'Lit' (p.7) +bottomLit :: Lit +bottomLit = 0 + +-- | converts "Var" into 'Lit' +newLit :: Var -> Lit +newLit = error "newLit undefined" + +-- | returns @True@ if the literal is positive +{-# INLINE positiveLit #-} +positiveLit :: Lit -> Bool +positiveLit = even + +-- | negates literal +-- +-- >>> negateLit 2 +-- 3 +-- >>> negateLit 3 +-- 2 +-- >>> negateLit 4 +-- 5 +-- >>> negateLit 5 +-- 4 +{-# INLINE negateLit #-} +negateLit :: Lit -> Lit +negateLit !l = complementBit l 0 -- if even l then l + 1 else l - 1 + +---------------------------------------- +----------------- Var +---------------------------------------- + +-- | converts 'Lit' into 'Var' +-- +-- >>> lit2var 2 +-- 1 +-- >>> lit2var 3 +-- 1 +-- >>> lit2var 4 +-- 2 +-- >>> lit2var 5 +-- 2 +{-# INLINE lit2var #-} +lit2var :: Lit -> Var +lit2var !n = shiftR n 1 + +-- | converts a 'Var' to the corresponing literal +-- +-- >>> var2lit 1 True +-- 2 +-- >>> var2lit 1 False +-- 3 +-- >>> var2lit 2 True +-- 4 +-- >>> var2lit 2 False +-- 5 +{-# INLINE var2lit #-} +var2lit :: Var -> Bool -> Lit +var2lit !v True = shiftL v 1 +var2lit !v _ = shiftL v 1 + 1 + +---------------------------------------- +----------------- Int +---------------------------------------- + +-- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@ +-- +-- >>> int2lit 1 +-- 2 +-- >>> int2lit (-1) +-- 3 +-- >>> int2lit 2 +-- 4 +-- >>> int2lit (-2) +-- 5 +-- +{-# INLINE int2lit #-} +int2lit :: Int -> Lit +int2lit n + | 0 < n = 2 * n + | otherwise = -2 * n + 1 + +-- | converts `Lit' into 'Int' as @int2lit . lit2int == id@ +-- +-- >>> lit2int 2 +-- 1 +-- >>> lit2int 3 +-- -1 +-- >>> lit2int 4 +-- 2 +-- >>> lit2int 5 +-- -2 +{-# INLINE lit2int #-} +lit2int :: Lit -> Int +lit2int l = case divMod l 2 of + (i, 0) -> i + (i, _) -> - i + +-- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/ +-- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2. +data LiftedBool = Bottom | LFalse | LTrue + deriving (Bounded, Eq, Ord, Read, Show) + +instance Enum LiftedBool where + {-# SPECIALIZE INLINE toEnum :: Int -> LiftedBool #-} + toEnum 1 = LTrue + toEnum (-1) = LFalse + toEnum _ = Bottom + {-# SPECIALIZE INLINE fromEnum :: LiftedBool -> Int #-} + fromEnum Bottom = 0 + fromEnum LFalse = 1 + fromEnum LTrue = 2 + +-- | converts 'Bool' into 'LBool' +{-# INLINE lbool #-} +lbool :: Bool -> LiftedBool +lbool True = LTrue +lbool False = LFalse + +-- | A contant representing False +lFalse:: Int +lFalse = -1 + +-- | A constant representing True +lTrue :: Int +lTrue = 1 + +-- | A constant for "undefined" +lBottom :: Int +lBottom = 0 + +-- | Assisting ADT for the dynamic variable ordering of the solver. +-- The constructor takes references to the assignment vector and the activity +-- vector of the solver. The method 'select' will return the unassigned variable +-- with the highest activity. +class VarOrder o where + -- | constructor + newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o + newVarOrder _ _ = error "newVarOrder undefined" + + -- | Called when a new variable is created. + newVar :: o -> IO Var + newVar = error "newVar undefined" + + -- | Called when variable has increased in activity. + update :: o -> Var -> IO () + update _ = error "update undefined" + + -- | Called when all variables have been assigned new activities. + updateAll :: o -> IO () + updateAll = error "updateAll undefined" + + -- | Called when variable is unbound (may be selected again). + undo :: o -> Var -> IO () + undo _ _ = error "undo undefined" + + -- | Called to select a new, unassigned variable. + select :: o -> IO Var + select = error "select undefined" + +-- | misc information on CNF +data CNFDescription = CNFDescription + { + _numberOfVariables :: !Int -- ^ number of variables + , _numberOfClauses :: !Int -- ^ number of clauses + , _pathname :: Maybe FilePath -- ^ given filename + } + deriving (Eq, Ord, Show) diff --git a/SAT/Solver/Mios/Validator.hs b/SAT/Solver/Mios/Validator.hs new file mode 100644 --- /dev/null +++ b/SAT/Solver/Mios/Validator.hs @@ -0,0 +1,47 @@ +-- | validate an assignment +{-# LANGUAGE + ViewPatterns + #-} +{-# LANGUAGE Safe #-} +module SAT.Solver.Mios.Validator + ( + validate + ) + where + +import Data.Foldable (toList) +import SAT.Solver.Mios.Types +import SAT.Solver.Mios.Clause +import SAT.Solver.Mios.ClauseManager +import SAT.Solver.Mios.Solver + +-- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here. +validate :: Traversable t => Solver -> t Int -> IO Bool +validate s (toList -> map int2lit -> lst) = do + assignment <- newVec $ 1 + nVars s + vec <- getClauseVector (clauses s) + nc <- numberOfClauses (clauses s) + let + inject :: Lit -> IO () + inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse + -- return True if the literal is satisfied under the assignment + satisfied :: Lit -> IO Bool + satisfied l + | positiveLit l = (lTrue ==) <$> getNth assignment (lit2var l) + | otherwise = (lFalse ==) <$> getNth assignment (lit2var l) + -- return True is any literal in the given list + satAny :: [Lit] -> IO Bool + satAny [] = return False + satAny (l:ls) = do + sat' <- satisfied l + if sat' then return True else satAny ls + -- traverse all clauses in 'clauses' + loopOnVector :: Int -> IO Bool + loopOnVector ((< nc) -> False) = return True + loopOnVector i = do + c <- getNthClause vec i + sat' <- satAny =<< asList c + if sat' then loopOnVector (i + 1) else return False + if null lst + then error "validator got an empty assignment." + else mapM_ inject lst >> loopOnVector 0 diff --git a/SAT/Util/BoolExp.hs b/SAT/Util/BoolExp.hs new file mode 100644 --- /dev/null +++ b/SAT/Util/BoolExp.hs @@ -0,0 +1,244 @@ +{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-} +{-# LANGUAGE Safe #-} + +-- | Boolean Expression module to build CNF from arbitrary expressions +-- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation +module SAT.Util.BoolExp + ( + -- * Class & Type + BoolComponent (..) + , BoolForm (..) + -- * Expression contructors + , (-|-) + , (-&-) + , (-=-) + , (-!-) + , (->-) + , neg + -- * List Operation + , disjunctionOf + , (-|||-) + , conjunctionOf + , (-&&&-) + -- * Convert function + , asList + , asList_ + , asLatex + , asLatex_ + , numberOfVariables + , numberOfClauses + , tseitinBase + ) + where + +import Data.List (foldl', intercalate) + +-- | the start index for the generated variables by Tseitin encoding +tseitinBase :: Int +tseitinBase = 1600000 + +data L = L Int + +-- | class of objects that can be interpeted as a bool expression +class BoolComponent a where + toBF :: a -> BoolForm -- lift to BoolForm + +-- | CNF expression +data BoolForm = Cnf (Int, Int) [[Int]] + deriving (Eq, Show) + +instance BoolComponent Int where + toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent L where + toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent [Char] where + toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent BoolForm where + toBF = id + +-- | returns the number of variables in the 'BoolForm' +numberOfVariables :: BoolForm -> Int +numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase + +-- | returns the number of clauses in the 'BoolForm' +numberOfClauses :: BoolForm -> Int +numberOfClauses (Cnf _ l) = length l + +boolFormTrue = Cnf (-1, 1) [] +boolFormFalse = Cnf (-1, -1) [] + +instance BoolComponent Bool where + toBF True = boolFormTrue + toBF False = boolFormFalse + +isTrue :: BoolForm -> Bool +isTrue = (== boolFormTrue) + +isFalse :: BoolForm -> Bool +isFalse = (== boolFormFalse) + +-- | return a 'clause' list only if it contains some real clause (not a literal) +clausesOf :: BoolForm -> [[Int]] +clausesOf cnf@(Cnf _ [[]]) = [] +clausesOf cnf@(Cnf _ [[x]]) = [] +clausesOf cnf@(Cnf _ l) = l + +maxRank :: BoolForm -> Int +maxRank (Cnf (n, _) _) = n + +-- | returns the number of valiable used as the output of this expression. +-- and returns itself it the expression is a literal. +-- Otherwise the number is a integer larger than 'tseitinBase'. +-- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future. +tseitinNumber :: BoolForm -> Int +tseitinNumber (Cnf (m, n) [[x]]) = x +tseitinNumber (Cnf (_, n) _) = n + +renumber :: Int -> BoolForm -> (BoolForm, Int) +renumber base (Cnf (m, n) l) + | l == [] = (Cnf (m, n) l, 0) + | tseitinBase < base = (Cnf (m, n') l', n') + | otherwise = (Cnf (n', tseitinBase) l', n') + where + l' = map (map f) l + n' = maximum $ map maximum l' + offset = base - tseitinBase - 1 + f x = if abs x < tseitinBase then x else signum x * (abs x + offset) + +instance Ord BoolForm where + compare (Cnf _ a) (Cnf _ b) = compare a b + +-- | disjunction constructor +-- +-- >>> asList $ "3" -|- "4" +-- [[3,4,-5],[-3,5],[-4,5]] +-- +-- >>> asList (("3" -|- "4") -|- "-1") +-- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]] +-- +(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -|- (toBF -> e2') + | isTrue e1 || isTrue e2' = boolFormTrue + | isFalse e1 && isFalse e2' = boolFormFalse + | isFalse e1 = e2' + | isFalse e2' = e1 + | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]] + where + a = tseitinNumber e1 + (e2, b) = renumber (1 + max tseitinBase a) e2' + m = max (maxRank e1) (maxRank e2) + c = 1 + max tseitinBase (max a b) + +-- | conjunction constructor +-- +-- >>> asList $ "3" -&- "-2" +-- [[-3,2,4],[3,-4],[-2,-4]] +-- +-- >>> asList $ "3" -|- ("1" -&- "2") +-- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]] +-- +(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -&- (toBF -> e2') + | isTrue e1 && isTrue e2' = boolFormTrue + | isFalse e1 || isFalse e2' = boolFormFalse + | isTrue e1 = e2' + | isTrue e2' = e1 + | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]] + where + a = tseitinNumber e1 + (e2, b) = renumber (1 + max tseitinBase a) e2' + m = max (maxRank e1) (maxRank e2) + c = 1 + max tseitinBase (max a b) + +-- | negate a form +-- +-- >>> asList $ neg ("1" -|- "2") +-- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]] +neg :: (BoolComponent a) => a -> BoolForm +neg (toBF -> e) = + Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]] + where + a = tseitinNumber e + m = maxRank e + c = 1 + max tseitinBase a + +-- | equal on BoolForm +(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2) + +-- | negation on BoolForm +(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2) + +-- | implication as a short cut +-- +-- >>> asList ("1" ->- "2") +-- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]] +(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> a) ->- (toBF -> b) = (neg a) -|- b + +-- | merge [BoolForm] by '(-|-)' +disjunctionOf :: [BoolForm] -> BoolForm +disjunctionOf [] = boolFormFalse +disjunctionOf (x:l) = foldl' (-|-) x l + +-- | an alias of 'disjunctionOf' +(-|||-) = disjunctionOf + +-- | merge [BoolForm] by '(-&-)' +conjunctionOf :: [BoolForm] -> BoolForm +conjunctionOf [] = boolFormTrue +conjunctionOf (x:l) = foldl' (-&-) x l + +-- | an alias of 'conjunctionOf' +(-&&&-) = conjunctionOf + +-- | converts a BoolForm to "[[Int]]" +asList_ :: BoolForm -> [[Int]] +asList_ cnf@(Cnf (m,_) _) + | isTrue cnf = [] + | isFalse cnf = [[]] + | otherwise = l' + where + (Cnf _ l', _) = renumber (m + 1) cnf + +-- | converts a *satisfied* BoolForm to "[[Int]]" +asList :: BoolForm -> [[Int]] +asList cnf@(Cnf (m,n) l) + | isTrue cnf = [] + | isFalse cnf = [[]] + | n <= tseitinBase = l + | otherwise = [m'] : l' + where + (Cnf (m', _) l', _) = renumber (m + 1) cnf + +-- | make latex string from CNF, using 'asList_' +-- +-- >>> asLatex $ "3" -|- "4" +-- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n" +-- +asLatex_ :: BoolForm -> String +asLatex_ b = beg ++ s ++ end + where + beg = "\\begin{displaymath}\n" + end = "\n\\end{displaymath}\n" + s = intercalate " \\wedge " [ makeClause c | c <- asList_ b] + makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" + makeLiteral l + | 0 < l = " x_{" ++ show l ++ "} " + | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " + +-- | make latex string from CNF, using 'asList' +asLatex :: BoolForm -> String +asLatex b = beg ++ s ++ end + where + beg = "\\begin{displaymath}\n" + end = "\n\\end{displaymath}\n" + s = intercalate " \\wedge " [ makeClause c | c <- asList b] + makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" + makeLiteral l + | 0 < l = " x_{" ++ show l ++ "} " + | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " diff --git a/SAT/Util/CNFIO.hs b/SAT/Util/CNFIO.hs new file mode 100644 --- /dev/null +++ b/SAT/Util/CNFIO.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE Safe #-} + +-- | Read/Write a CNF file only with ghc standard libraries +module SAT.Util.CNFIO + ( + -- * Input + fromFile + , clauseListFromFile + , fromMinisatOutput + , clauseListFromMinisatOutput + -- * Output + , toFile + , toCNFString + , asCNFString + , asCNFString_ + -- * Bool Operation + , module SAT.Util.BoolExp + ) + where +import SAT.Util.CNFIO.Reader +import SAT.Util.CNFIO.Writer +import SAT.Util.CNFIO.MinisatReader +import SAT.Util.BoolExp + +-- | String from BoolFrom +asCNFString :: BoolForm -> String +asCNFString = toCNFString . asList + +-- | String from BoolFrom +asCNFString_ :: BoolForm -> String +asCNFString_ = toCNFString . asList_ diff --git a/SAT/Util/CNFIO/MinisatReader.hs b/SAT/Util/CNFIO/MinisatReader.hs new file mode 100644 --- /dev/null +++ b/SAT/Util/CNFIO/MinisatReader.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE Safe #-} + +-- | Read an output file of minisat +module SAT.Util.CNFIO.MinisatReader + ( + -- * Interface + fromMinisatOutput + , clauseListFromMinisatOutput + ) + where +-- import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +-- |parse a non-signed integer +{-# INLINE pint #-} +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int = mint <++ pint + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums = do + skipSpaces + x <- int + skipSpaces + if (x == 0) then return [] else (x :) <$> seqNums + +-- |top level interface for parsing CNF +{-# INLINE parseMinisatOutput #-} +parseMinisatOutput :: ReadP ((Int, Int), [Int]) +parseMinisatOutput = do + string "SAT" + skipSpaces + l <- seqNums + return ((length l,0), l) + +-- |read a minisat output: +-- ((numbefOfVariables, 0), [Literal]) +-- +-- >>> fromFile "result" +-- ((3, 0), [1, -2, 3]) +-- +{-# INLINE fromMinisatOutput #-} +fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) +fromMinisatOutput f = do + c <- readFile f + case readP_to_S parseMinisatOutput c of + [(a, _)] -> return $ Just a + _ -> return Nothing + +-- | return clauses as [[Int]] from 'file' +-- +-- >>> clauseListFromMinisatOutput "result" +-- [1,-2,3] +-- +clauseListFromMinisatOutput :: FilePath -> IO [Int] +clauseListFromMinisatOutput l = do + res <- fromMinisatOutput l + case res of + Just p -> return (snd p) + _ -> return [] diff --git a/SAT/Util/CNFIO/Reader.hs b/SAT/Util/CNFIO/Reader.hs new file mode 100644 --- /dev/null +++ b/SAT/Util/CNFIO/Reader.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE Safe #-} + +-- | Read a CNF file without haskell-platform +module SAT.Util.CNFIO.Reader + ( + -- * Interface + fromFile + , clauseListFromFile + ) + where +import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +{-# INLINE newline #-} +newline = char '\n' + +{-# INLINE digit #-} +digit = satisfy isDigit + +{-# INLINE spaces #-} +spaces = munch (`elem` " \t") + +{-# INLINE noneOf #-} +noneOf s = satisfy (`notElem` s) + +-- |parse a non-signed integer +{-# INLINE pint #-} +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int = mint <++ pint + +-- |Parse something like: p FORMAT VARIABLES CLAUSES +{-# INLINE problemLine #-} +problemLine = do + char 'p' + skipSpaces + (string "cnf" <++ string "CNF") + skipSpaces + vars <- pint + skipSpaces + clas <- pint + spaces + newline + return (vars, clas) + +-- |Parse something like: c This in an example of a comment line. +{-# INLINE commentLines #-} +commentLines = do + l <- look + if (head l) == 'c' + then do + munch ('\n' /=) + newline + commentLines + else return () + +_commentLines = do + char 'c' + munch ('\n' /=) + newline + l <- look + if (head l) == 'c' then commentLines else return () + +-- |Parse the preamble part +{-# INLINE preambleCNF #-} +preambleCNF = do + commentLines + problemLine + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums = do + skipSpaces + x <- int + skipSpaces + if (x == 0) then return [] else (x :) <$> seqNums + +-- |Parse something like: 1 -2 0 4 0 -3 0 +{-# INLINE parseClauses #-} +parseClauses :: Int -> ReadP [[Int]] +parseClauses n = count n seqNums + +-- |top level interface for parsing CNF +{-# INLINE parseCNF #-} +parseCNF :: ReadP ((Int, Int), [[Int]]) +parseCNF = do + a <- preambleCNF + b <- parseClauses (snd a) + return (a, b) + +-- |driver:: String -> Either ParseError Int +driver input = readP_to_S (parseClauses 1) input + +-- |read a CNF file and return: +-- ((numbefOfVariables, numberOfClauses), [Literal]) +-- +-- >>> fromFile "acnf" +-- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]] +-- +{-# INLINE fromFile #-} +fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) +fromFile f = do + c <- readFile f + case readP_to_S parseCNF c of + [(a, _)] -> return $ Just a + _ -> return Nothing + +-- | return clauses as [[Int]] from 'file' +-- +-- >>> clauseListFromFile "a.cnf" +-- [[1, 2], [-2, 3], [-1, 2, -3], [3]] +-- +clauseListFromFile :: FilePath -> IO [[Int]] +clauseListFromFile l = do + res <- fromFile l + case res of + Just (_, l) -> return l + _ -> return [] diff --git a/SAT/Util/CNFIO/Writer.hs b/SAT/Util/CNFIO/Writer.hs new file mode 100644 --- /dev/null +++ b/SAT/Util/CNFIO/Writer.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE Safe #-} + +-- | Write SAT data to CNF file +module SAT.Util.CNFIO.Writer + ( + -- * Interface + toFile + , toCNFString + , toString + , toLatexString + ) + where +import Data.List (intercalate, nub, sort) +import System.IO + +-- | Write the CNF to file 'f', using 'toCNFString' +toFile :: FilePath -> [[Int]] -> IO () +toFile f l = writeFile f $ toCNFString l + +-- | Convert [Clause] to String, where Clause is [Int] +-- +-- >>> toCNFString [] +-- "p cnf 0 0\n" +-- +-- >>> toCNFString [[-1, 2], [-3, -4]] +-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n" +-- +-- >>> toCNFString [[1], [-2], [-3, -4], [1,2,3,4]] +-- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n" +-- +toCNFString :: [[Int]] -> String +toCNFString l = hdr ++ str + where + hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n" + numC = length l + numV = last $ nub $ sort $ map abs $ concat l + str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l] + +-- | converts @[[Int]]@ to a String +toString :: [[Int]] -> String -> String -> String +toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] + where + lit x + | 0 <= x = "X" ++ show x + | otherwise = "-X" ++ show (abs x) + a = pad and' + o = pad or' + pad s = " " ++ s ++ " " + +-- | converts @[[Int]]@ to a LaTeX expression +toLatexString :: [[Int]] -> String +toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}" + where + lit x + | 0 <= x = "X_{" ++ show x ++ "}" + | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}" + a = " \n\\wedge " + o = " \\vee " diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/mios.hs b/app/mios.hs new file mode 100644 --- /dev/null +++ b/app/mios.hs @@ -0,0 +1,20 @@ +-- | Executable of 'Minisat Implementation and Optimization Study' +module Main + ( + main + ) + where + +import SAT.Solver.Mios + +-- | main +main :: IO () +main = do + opts <- miosParseOptionsFromArgs versionId + case () of + _ | _displayVersion opts -> putStrLn versionId + _ | _displayHelp opts -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" + _ | _targetFile opts == Just "" -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" + _ | _validateAssignment opts -> executeValidator opts + _ | otherwise -> executeSolver opts + diff --git a/mios.cabal b/mios.cabal new file mode 100644 --- /dev/null +++ b/mios.cabal @@ -0,0 +1,89 @@ +-- Initial mios.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/ + +name: mios +version: 1.2.1 +synopsis: A Minisat-based SAT solver in Haskell +description: + + A modern and fast SAT solver written in Haskell, based on Minisat-1.14 and 2.2. + By using CDCL, watch literals, VSIDS, restart, blocking-literals, LBD and so on, + the current version is only 1.8 time slower than Minisat-1.14. + "Mios" is an abbreviation of /Minisat-based Implementation and Optimization Study on SAT solver/. + . + +homepage: https://github.com/shnarazk/mios +license: GPL-3 +license-file: LICENSE +author: Shuji Narazaki +maintainer: Shuji Narazaki +category: Artificial Intelligence, Constraint Solver +build-type: Simple +cabal-version: >=1.16 + +Flag llvm + Description: Compile with llvm + Default: False + +library + buildable: True + default-language: Haskell2010 + default-extensions: Strict + exposed-modules: + SAT.Solver.Mios + SAT.Solver.Mios.Clause + SAT.Solver.Mios.ClauseManager + SAT.Solver.Mios.Data.VecBool + SAT.Solver.Mios.Data.VecDouble + SAT.Solver.Mios.Data.Vec + SAT.Solver.Mios.Data.Singleton + SAT.Solver.Mios.Data.Stack + SAT.Solver.Mios.Internal + SAT.Solver.Mios.Glucose + SAT.Solver.Mios.M114 + SAT.Solver.Mios.OptionParser + SAT.Solver.Mios.Solver + SAT.Solver.Mios.Types + SAT.Solver.Mios.Validator + SAT.Util.CNFIO + SAT.Util.CNFIO.MinisatReader + SAT.Util.CNFIO.Reader + SAT.Util.CNFIO.Writer + SAT.Util.BoolExp + build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6 + if flag(llvm) + ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + else + ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2 + +executable mios + main-is: app/mios.hs + buildable: True + default-language: Haskell2010 + default-extensions: Strict + build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6 + if flag(llvm) + ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + else + ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2 + other-modules: + SAT.Solver.Mios + SAT.Solver.Mios.Clause + SAT.Solver.Mios.ClauseManager + SAT.Solver.Mios.Data.VecBool + SAT.Solver.Mios.Data.VecDouble + SAT.Solver.Mios.Data.Vec + SAT.Solver.Mios.Data.Singleton + SAT.Solver.Mios.Data.Stack + SAT.Solver.Mios.Internal + SAT.Solver.Mios.Glucose + SAT.Solver.Mios.M114 + SAT.Solver.Mios.OptionParser + SAT.Solver.Mios.Solver + SAT.Solver.Mios.Types + SAT.Solver.Mios.Validator + SAT.Util.CNFIO + SAT.Util.CNFIO.MinisatReader + SAT.Util.CNFIO.Reader + SAT.Util.CNFIO.Writer + SAT.Util.BoolExp