From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id D2F97139694 for ; Fri, 2 Jun 2017 15:19:33 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id EE070E0E0F; Fri, 2 Jun 2017 15:19:24 +0000 (UTC) Received: from mail-wr0-x242.google.com (mail-wr0-x242.google.com [IPv6:2a00:1450:400c:c0c::242]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 8667AE0DE9 for ; Fri, 2 Jun 2017 15:19:24 +0000 (UTC) Received: by mail-wr0-x242.google.com with SMTP id v104so1532467wrb.0 for ; Fri, 02 Jun 2017 08:19:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=date:from:to:subject:message-id:in-reply-to:references:mime-version :content-transfer-encoding; bh=qJZAO89OyA3MW8bvfPIFZTV706Kt1o0EUm8Dmy9vcG0=; b=oO9Bsterlps4Iu9igFW4NcY3xinx+OZX4pa0nhnnbh4Ghw6OKkMpBlxBB4305py+Ua grqnYVvBzfr0ELprcF68SzlM4nDBhJZ4AYSoir6SlZk69hXxWBQV6aiWWfbwpcqfYzuu vgfeTL8UdewjlUzXGjXdjkc6PidI07CCUy+ZBaV7Gb1e0WC5KS3wKs18HYGZtF3PDvte zrqNp6k3PWrC7TFcWs9Q4J+lu1YrP7ShoDaqt/omQnf6i5dk4elDQ6kNkcUF+8CeC3du ncMMzB6zp3+uNo8SyLapKg6WLnzsKWAnK0FKPAIjG7WGvP9AgsVjFQEawwSLXApZ47cv 7Esg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:subject:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=qJZAO89OyA3MW8bvfPIFZTV706Kt1o0EUm8Dmy9vcG0=; b=nHCVLjPF6yU/sBq0F6o+SEF32wqJfwTKTNej+jGGEVBZVe9gf3vC/4P3qBpUJiNkEk s5RfXjv93Hcm6tuchKgaXeW7R5s9jcAeiUBIr1GqZBC5Qw6KN0273RP0iMUihoVG3AkO v7owdPx/uORJVCZOEPCf7tlOK3etgUQztx1NZQLVYIlL6WeAvZgnhkzxH8pJ/9ByNzoQ cvROv9duF/ITmRI4pIQa3qhmBXMVqVBncOOL+AHxTCMVoEJdDs+/fmnkffKlqcGrVHhY XpQahYJW9sOmDAnJRc/qZGrOzVXtRrhjKHrRQntldVn4imEw4TfI3gOV/tBbe1g3sAQa FHTg== X-Gm-Message-State: AODbwcC8DSGrCK2ssBhP0xSa21Nyug3H2WQYMqZq8TJ92cBH5vzGwLmv RqTg6ATWTumrQK3c X-Received: by 10.223.143.35 with SMTP id p32mr5209147wrb.120.1496416762809; Fri, 02 Jun 2017 08:19:22 -0700 (PDT) Received: from snowblower (cpc4-broo7-2-0-cust35.14-2.cable.virginm.net. [82.8.215.36]) by smtp.gmail.com with ESMTPSA id t8sm12951131wrc.28.2017.06.02.08.19.22 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Fri, 02 Jun 2017 08:19:22 -0700 (PDT) Date: Fri, 2 Jun 2017 16:19:19 +0100 From: Ciaran McCreesh To: gentoo-dev@lists.gentoo.org Subject: Re: [gentoo-dev] Re: [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE) Message-ID: <20170602161919.68d0b80b@snowblower> In-Reply-To: References: <1496071993.31087.1.camel@gentoo.org> <20170529200037.2559f80a@gentoo.org> <1496093035.12795.3.camel@gentoo.org> <20170530094245.40e1cf64@gentoo.org> <20170530092245.681d4aeb@snowblower> <20170530104654.31b89e10@gentoo.org> <20170530095607.1adbc0b8@snowblower> <20170530112518.65b4f9e9@gentoo.org> <22829.24276.295.969060@a1i15.kph.uni-mainz.de> <1496154812.1238.5.camel@gentoo.org> <20170530173340.0b575526@gentoo.org> <1496167898.1335.1.camel@gentoo.org> <20170530204614.61e8e42c@gentoo.org> <1496213717.1164.1.camel@gentoo.org> <20170531093257.23b66f88@gentoo.org> <1496217792.1164.5.camel@gentoo.org> <20170531103819.417c2420@gentoo.org> <1496235892.25038.1.camel@gentoo.org> <20170531193922.477245bb@gentoo.org> <1496257344.25758.1.camel@gentoo.org> <20170601105523.08a9234e@gentoo.org> <1496352685.30502.4.camel@gentoo.org> <20170602141618.68a1e3e4@gentoo.org> X-Mailer: Claws Mail 3.13.0 (GTK+ 2.24.31; x86_64-pc-linux-gnu) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-dev@lists.gentoo.org Reply-to: gentoo-dev@lists.gentoo.org MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Archives-Salt: 0f22d1e5-d18b-4465-a5a8-2f9f7f5b3819 X-Archives-Hash: dfb7691d6b128f8c32da5c8bcd88afb3 On Fri, 2 Jun 2017 14:56:42 +0000 (UTC) Martin Vaeth wrote: > Most examples mentioned earlier were actually 2SAT, i.e., > they are only of the form foo? ( bar ) (possibly with negations) > or can be easily reduced to that. E.g. > ^^ ( foo bar ) > foo? ( !bar graulty bazola ) > can be rewritten as 2 or 3 2SAT-clauses as above, respectively. > > For 2SAT, there are linear time algorithms. You're getting the encoding wrong. "foo? ( bar )" does not encode as "( !foo \/ bar )", because that would permit the solver to turn on bar even if there is no need to do so. Good luck figuring out how to encode grounding in SAT... -- Ciaran McCreesh